プログラムを証明するには？

**１３２人目の素数さん** · 2025/03/08(土) 00:48:27.93

どうしたらいい？

**１３２人目の素数さん** · 2025/03/08(土) 01:10:04.22

表示的意味論

**１３２人目の素数さん** · 2025/03/08(土) 01:26:12.12

依存型

**１３２人目の素数さん** · 2025/03/08(土) 05:54:27.61

働けウンコ製造機

**１３２人目の素数さん** · 2025/03/08(土) 05:55:24.93

「数学」をプログラミングするには2 @ぷ板

**１３２人目の素数さん** · 2025/03/08(土) 08:32:34.22

プログラムとは？

**１３２人目の素数さん** · 2025/03/08(土) 08:32:54.99

証明とは？

**１３２人目の素数さん** · 2025/03/08(土) 08:33:14.12

思い付きとは？

**１３２人目の素数さん** · 2025/03/08(土) 10:19:37.00

たとえばFizzBuzzのプログラムが「正しい」ことはどうやって証明するのか
入力が固定なら、出力を正解と差分比較すればいいが

**１３２人目の素数さん** · 2025/03/08(土) 10:32:47.02

プログラムが仕様通り作られていることを形式的に証明する、のか

**１３２人目の素数さん** · 2025/03/08(土) 10:33:31.33

ホーア論理

**１３２人目の素数さん** · 2025/03/08(土) 10:34:11.32

ダイクストラのプログラム検証法

**１３２人目の素数さん** · 2025/03/08(土) 10:36:11.90

coq

**１３２人目の素数さん** · 2025/03/08(土) 12:20:00.49

>>9
自然数が

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

の無縁和に分かれることの証明を表現する
それぞれのケースに対する関数を定義する
FizzBuzzの上限と下限を決める

このようになっていれば形式的に証明できると思う

**poem** · 2025/03/09(日) 18:57:21.39

https://rio2016.5ch.net/test/read.cgi/math/1739087008/44-46/

**１３２人目の素数さん** · 2025/03/10(月) 06:51:19.10

そもそもね、仕様書がプログラミング通り
作られてるかな❓
て、ゆうか、FizzBuzzの仕様書？の方が意味不明
プログラミング言語の記述の方が分かりやすい
てか、
if (n%15) console.log(FizzBuzz);
else if (n%3) console.log(Fizz);
ホゲホゲ
てプログラミング結果と一致するか
ま、nが1〜300位までチェックすりゃ大丈夫だろ
て、ゆぅかっ、1,2,3,5,15,16 の６通りで
いいぢゃーーーん。
てか、予算は幾らあるの❓
そりゃさ、自然数は可算∞個あるのだから
可算無限個とおりチェックしなさーーーい

ま、ポクは、６通りチェックするだけで
非可算無限チェックしたのと同じ
位、それがバッチリか検証できる超能力を
有するウチュ〰人だよぉーーー

**16 怪しい呟き** · 2025/03/10(月) 06:56:50.93

console.log(FizzBuzz);　🐴🦌だねぇー
console.log("FizzBuzz");　だろ
ちみは、15の倍数とか、任意の自然数のとき、
定義されてませーーーんとか答えると
正確なのか？。ちゃんと検証してから投稿しなさーーーい

by 自分へ返答、変答、変な解答、怪解でした。(;_;)/~~~

**16は、知能は、ヤバイ(自演)** · 2025/03/11(火) 10:57:04.40

>>16 よ。チミは、昨日の自分ぢゃーん
そもそも、
15の倍数⇒3の倍数∧5の倍数　だから
15とか30とか45とかは、
FIZZ も BUZZ もドッチも正解だぁ
FIZZ、BUZZが正解でも正解たけどさ、
FIZZ でも正解にしてあげて、

てか、国語なら必要条件さえ答えれば
💯なのに、数学は零点になるよな❓
てか、地球人のルールの解説ヤバイ

**poem** · 2025/03/11(火) 12:22:09.43

39 ご冗談でしょう？名無しさん 225/03/11(火) 10:33:16.84
部品は高尚な概念なんだよ
部品はブリコラージュ（器用仕事）の上位互換
エントロピー、オキシトシン、アルファ波などを組み込むと機械という高尚な概念になる
大部分は唯物論の実証や数学から来ているがシャノンエントロピーなんて例外もある

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
熱力学のエントロピーの方ね

**１３２人目の素数さん** · 2025/03/11(火) 17:06:43.45

哲学で実証の証明をやってる
全体は部分の総和という理論

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

心理学は神経科学により実証される
神経科学（オキシトシン）や脳科学（アルファ波）がメソッド主義であり
数的関係を持つ部品になる
この部品こそ研鑽の集大成でありタイプ理論などは机上の空論であり部品たり得ない
全体は部分（部品）の総和であるべきである
https://lavender.5ch.net/test/read.cgi/psycho/1741093674/21

16 · 2025/03/13(木) 04:08:42.01

３日前の自分、壱拾六へ

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

西暦年が4で割切れるは、閏年。でも
西暦年が100で割切れるは、平年。でも
西暦年が400で割切れるは、閏年。
としてるよう、ぢゃ。ぢゃから

地球人は、おそらく、絶対
400の倍数は、100の倍数ぢゃない、かつ
100の倍数は、4の倍数ぢゃない。
と、理解してるのか❓
全く数学というか算数すらもダメな地球人

てか、西暦2000年は、閏年でバグちゃう
バグが、発生しちゃったようだぜ。

by 👾の感想文でした。(^.^)/~~~

16 · 2025/03/13(木) 04:16:37.06

でもさ、ちょう安易に、
「西暦は、４で割り切れるは、閏年」
なんてしてるロジックは、西暦2000年問題は、クリア
🐴🦌な奴が開発したロジックがバグらんって
地球の自転速度てか公転速度を決めた神サマは、
カナリ、チョー天才だな。by 👾

**１３２人目の素数さん** · 2025/03/26(水) 10:12:32.43

むしろプログラムこそが証明なんだが

**１３２人目の素数さん** · 2025/09/28(日) 21:25:49.58

>>1
任意のプログラムコードをHaskellに変換する。
Haskellコードを数学に置き換えて証明する（ここは手動。HaskellからTeXへの変換手段があれば自動化できそう）

**１３２人目の素数さん** · 2025/10/19(日) 14:15:30.82

プログラムのいったい何を証明したいのか意味不明

プログラムが何かの証明を記述しているのだろうと思えば>>23
プログラムの正しさを証明したいのだとすればホーアロジック
etc

**１３２人目の素数さん** · 2025/10/19(日) 14:56:09.71

>>23
その場合、バグとは証明すべき定理を取り違えたことで生じる（笑）