22/04/30 21:22:50.15 .net
>>829
＞（証明を）プログラムに例えると
＞ 1）プログラムの設計と書き方
＞ 2）プログラムの検証
＞ 3）プログラムの可読性
＞ に分けて考えることが出来る
ほんまけ？
＞・「プログラムの設計と書き方」は、
＞ C言語を使うとか、サブルーチンと本体プログラムとの関係とか
＞ 「プログラムの検証」は、論文の査読に相当する
＞ 「プログラムの可読性」は、メンテナンスも考えると、
＞ 作者と別の人が読めるように、どの言語を使ったとか、
＞ フローチャートを作るとか、コメントを入れて
＞ 変数の意味づけやサブルーチンの意図を書いておくとか
下げマス システム設計したこと全然ないやろｗ
「プログラムの検証」とはプログラムが仕様を満たすことの証明
ここで仕様は当然論理式で記述する
プログラムの各ステートメントは
実行前の事前条件と事後条件の組で
意味が明確に記載できる（ホーア論理）
URLﾘﾝｸ(ja.wikipedia.org)
ホーア論理に従って、プログラム全体の仕様が
証明できれば検証できたことになる
つまり「ま、いいんじゃね」とかいう
気分的なチェックは検証でもなんでもないのよ
FesenkoもSaidiもカトブンもまったく
IUT論文を検証できてないってこと
そんなん「査読」とかいってるなら数学は死んでるねｗ
＞・そうすると、「プログラムの検証」と
＞「プログラムの可読性」とは分けることが出来る
なんか下げマスはくだらぬ言い訳ばっかりしてるけど
そもそもＩＵＴ論文は検証すら全然できてないのが問題
「ホーア論理」にあたるのが形式的証明による検証
そもそも証明＝プログラムであるから別におかしくはない
＞ある読み手にとっては「プログラムの可読性」が悪くても、
＞別の人で「プログラムの検証」はちゃんと出来ているってことが
＞あってもおかしくない
そもそもできてない
検証できてるなら可読性なんか完璧にできる
ま、論理の基本も分かってない論盲の下げマスみたいな
人間失格のニホンザルは別だがなｗｗｗ