No.1
プログラムを証明するには？
レス数: 26
概要: どうしたらいい？
No.2
No.3
No.4
No.5
No.6
No.7
No.8
No.9
入力が固定なら、出力を正解と差分比較すればいいが
No.10
No.11
No.12
No.13
No.14
自然数が
・3の倍数だが5の倍数ではない
・5の倍数だが3の倍数ではない
・3の倍数かつ5の倍数
・それ以外
の無縁和に分かれることの証明を表現する
それぞれのケースに対する関数を定義する
FizzBuzzの上限と下限を決める
このようになっていれば形式的に証明できると思う
No.15
No.16
作られてるかな❓
て、ゆうか、FizzBuzzの仕様書？の方が意味不明
プログラミング言語の記述の方が分かりやすい
てか、
if (n%15) console.log(FizzBuzz);
else if (n%3) console.log(Fizz);
ホゲホゲ
てプログラミング結果と一致するか
ま、nが1〜300位までチェックすりゃ大丈夫だろ
て、ゆぅかっ、1,2,3,5,15,16 の６通りで
いいぢゃーーーん。
てか、予算は幾らあるの❓
そりゃさ、自然数は可算∞個あるのだから
可算無限個とおりチェックしなさーーーい
ま、ポクは、６通りチェックするだけで
非可算無限チェックしたのと同じ
位、それがバッチリか検証できる超能力を
有するウチュ〰人だよぉーーー
No.17
console.log("FizzBuzz"); だろ
ちみは、15の倍数とか、任意の自然数のとき、
定義されてませーーーんとか答えると
正確なのか？。ちゃんと検証してから投稿しなさーーーい
by 自分へ返答、変答、変な解答、怪解でした。(;_;)/~~~
No.18
よ。チミは、昨日の自分ぢゃーん
そもそも、
15の倍数⇒3の倍数∧5の倍数 だから
15とか30とか45とかは、
FIZZ も BUZZ もドッチも正解だぁ
FIZZ、BUZZが正解でも正解たけどさ、
FIZZ でも 正解にしてあげて、
てか、国語なら必要条件さえ答えれば
💯なのに、数学は零点になるよな❓
てか、地球人のルールの解説ヤバイ
No.19
部品は高尚な概念なんだよ
部品はブリコラージュ（器用仕事）の上位互換
エントロピー、オキシトシン、アルファ波などを組み込むと機械という高尚な概念になる
大部分は唯物論の実証や数学から来ているがシャノンエントロピーなんて例外もある
41 poem 225/03/11(火) 12:10:33.57
シャノンエントロピーと調べたら
2進数情報量？
10進数情報量が
ハートレーエントロピーと言ったり？
42 poem 225/03/11(火) 12:14:35.95
念の為に言うけど
同じ5MBの情報量でも
情報の入れ子具合で
機能の水準が違うからね
1,0の入れ子(括弧で括り)無しだと単なるバイナリで情報表現は1次元紐の水準しかなく
入れ子ありだと2次元3次元n次元以上の情報表現になる
だから2進数情報量だけでは機能水準を表していない
43 poem 225/03/11(火) 12:15:49.05
単なるエントロピーつまり乱雑さに
入れ子とかあるのかは知らない
44 poem 225/03/11(火) 12:16:18.57
熱力学のエントロピーの方ね
No.20
全体は部分の総和という理論
メソッド理論の観点から見た心理学の実証
心理学は神経科学により実証される
神経科学（オキシトシン）や脳科学（アルファ波）がメソッド主義であり
数的関係を持つ部品になる
この部品こそ研鑽の集大成でありタイプ理論などは机上の空論であり部品たり得ない
全体は部分（部品）の総和であるべきである
https:
No.21
FIZZ BUZZのルールの地球人よる説明も
カナリ、あれだけどさ、
地球人が発明した閏年の説明も
カナリ。あれだな。
西暦年が4で割切れるは、閏年。でも
西暦年が100で割切れるは、平年。でも
西暦年が400で割切れるは、閏年。
としてるよう、ぢゃ。ぢゃから
地球人は、おそらく、絶対
400の倍数は、100の倍数ぢゃない、かつ
100の倍数は、4の倍数ぢゃない。
と、理解してるのか❓
全く数学というか算数すらもダメな地球人
てか、西暦2000年は、閏年でバグちゃう
バグが、発生しちゃったようだぜ。
by 👾の感想文でした。(^.^)/~~~
No.22
「西暦は、４で割り切れるは、閏年」
なんてしてるロジックは、西暦2000年問題は、クリア
🐴🦌な奴が開発したロジックがバグらんって
地球の自転速度てか公転速度を決めた神サマは、
カナリ、チョー天才だな。by 👾
No.23
No.24
任意のプログラムコードをHaskellに変換する。
Haskellコードを数学に置き換えて証明する（ここは手動。HaskellからTeXへの変換手段があれば自動化できそう）
No.25
プログラムが何かの証明を記述しているのだろうと思えば
>>23
プログラムの正しさを証明したいのだとすればホーアロジック
etc
No.26
その場合、バグとは証明すべき定理を取り違えたことで生じる（笑）
