プログラムを証明するには? (24レス)
1-

1
(1): 03/08(土)00:48 ID:YjtwmC1M(1) AAS
どうしたらいい?
2: 03/08(土)01:10 ID:0PDxRvmg(1) AAS
表示的意味論
3: 03/08(土)01:26 ID:+BBHA5Hy(1) AAS
依存型
4: 03/08(土)05:54 ID:3yKaxuFZ(1/9) AAS
働けウンコ製造機
5: 03/08(土)05:55 ID:3yKaxuFZ(2/9) AAS
「数学」をプログラミングするには2 @ぷ板
6: 03/08(土)08:32 ID:3yKaxuFZ(3/9) AAS
プログラムとは?
7: 03/08(土)08:32 ID:3yKaxuFZ(4/9) AAS
証明とは?
8: 03/08(土)08:33 ID:3yKaxuFZ(5/9) AAS
思い付きとは?
9
(1): 03/08(土)10:19 ID:lUzSDHir(1) AAS
たとえばFizzBuzzのプログラムが「正しい」ことはどうやって証明するのか
入力が固定なら、出力を正解と差分比較すればいいが
10: 03/08(土)10:32 ID:3yKaxuFZ(6/9) AAS
プログラムが仕様通り作られていることを形式的に証明する、のか
11: 03/08(土)10:33 ID:3yKaxuFZ(7/9) AAS
ホーア論理
12: 03/08(土)10:34 ID:3yKaxuFZ(8/9) AAS
ダイクストラのプログラム検証法
13: 03/08(土)10:36 ID:3yKaxuFZ(9/9) AAS
coq
14: 03/08(土)12:20 ID:0f9oMeD6(1) AAS
>>9
自然数が

・3の倍数だが5の倍数ではない
・5の倍数だが3の倍数ではない
・3の倍数かつ5の倍数
・それ以外

の無縁和に分かれることの証明を表現する
省3
15: poem 03/09(日)18:57 ID:HM1Gkwqb(1) AAS
2chスレ:math
16
(3): 03/10(月)06:51 ID:9N9g1qmV(1/2) AAS
そもそもね、仕様書がプログラミング通り
作られてるかな❓
て、ゆうか、FizzBuzzの仕様書?の方が意味不明
プログラミング言語の記述の方が分かりやすい
てか、
if (n%15) console.log(FizzBuzz);
else if (n%3) console.log(Fizz);
省12
17: 16 怪しい呟き 03/10(月)06:56 ID:9N9g1qmV(2/2) AAS
console.log(FizzBuzz); 🐴🦌だねぇー
console.log("FizzBuzz"); だろ
ちみは、15の倍数とか、任意の自然数のとき、
定義されてませーーーんとか答えると
正確なのか?。ちゃんと検証してから投稿しなさーーーい

by 自分へ返答、変答、変な解答、怪解でした。(;_;)/~~~
18: 16は、知能は、ヤバイ(自演) 03/11(火)10:57 ID:3Bh/sPXv(1) AAS
>>16 よ。チミは、昨日の自分ぢゃーん
そもそも、
15の倍数⇒3の倍数∧5の倍数 だから
15とか30とか45とかは、
FIZZ も BUZZ もドッチも正解だぁ
FIZZ、BUZZが正解でも正解たけどさ、
FIZZ でも 正解にしてあげて、
省3
19: poem 03/11(火)12:22 ID:7G9/jMlG(1) AAS
39 ご冗談でしょう?名無しさん 225/03/11(火) 10:33:16.84
部品は高尚な概念なんだよ
部品はブリコラージュ(器用仕事)の上位互換
エントロピー、オキシトシン、アルファ波などを組み込むと機械という高尚な概念になる
大部分は唯物論の実証や数学から来ているがシャノンエントロピーなんて例外もある

41 poem 225/03/11(火) 12:10:33.57
シャノンエントロピーと調べたら
省16
20: 03/11(火)17:06 ID:LeJDstie(1) AAS
哲学で実証の証明をやってる
全体は部分の総和という理論

メソッド理論の観点から見た心理学の実証

心理学は神経科学により実証される
神経科学(オキシトシン)や脳科学(アルファ波)がメソッド主義であり
数的関係を持つ部品になる
この部品こそ研鑽の集大成でありタイプ理論などは机上の空論であり部品たり得ない
省2
21: 16 03/13(木)04:08 ID:1QPgiK/Y(1/2) AAS
3日前の自分、壱拾六へ

FIZZ BUZZのルールの地球人よる説明も
カナリ、あれだけどさ、
地球人が発明した閏年の説明も
カナリ。あれだな。

西暦年が4で割切れるは、閏年。でも
西暦年が100で割切れるは、平年。でも
省10
22: 16 03/13(木)04:16 ID:1QPgiK/Y(2/2) AAS
でもさ、ちょう安易に、
「西暦は、4で割り切れるは、閏年」
なんてしてるロジックは、西暦2000年問題は、クリア
🐴🦌な奴が開発したロジックがバグらんって
地球の自転速度てか公転速度を決めた神サマは、
カナリ、チョー天才だな。by 👾
23: 03/26(水)10:12 ID:RyqxVhEy(1) AAS
むしろプログラムこそが証明なんだが
24: 09/28(日)21:25 ID:ukWFqdUB(1) AAS
>>1
任意のプログラムコードをHaskellに変換する。
Haskellコードを数学に置き換えて証明する(ここは手動。HaskellからTeXへの変換手段があれば自動化できそう)
1-
スレ情報 赤レス抽出 画像レス抽出 歴の未読スレ AAサムネイル

ぬこの手 ぬこTOP 1.133s*