【Alloy】形式言語による仕様記述【VDM】at TECH【Alloy】形式言語による仕様記述【VDM】 - 暇つぶし2ch■コピペモード□スレを通常表示□オプションモード□このｽﾚｯﾄﾞのURL■項目テキスト281:デフォルトの名無しさん 15/04/30 07:58:46.50 B1QV8IC2.net うん、その違いだよ。 抽象度の高いモデルで正しさを証明できたとして、それをもって現実のプログラムの 正しさの証明とするにはギャップは小さいほうがいいと思うが。 書き換えの段階で間違いが入ったらそもそも意味がないし。 ギャップが大きいほどいいとする理由は？ 282:デフォルトの名無しさん 15/04/30 08:47:12.46 YRFCj/Kr.net えー！ 極端な場合で考えてみなよ ギャップ＝０ということはモデルの意味がないということだ 283:デフォルトの名無しさん 15/04/30 09:07:52.87 B1QV8IC2.net モデルの意味って何ぞ？ >>277の言う現実のプロジェクトではモデルを構築することそれ自体が目的じゃなくて 実際のシステムに誤りがないことを保証したいわけだろう。 モデルはそのための道具でしかない。 284:デフォルトの名無しさん 15/04/30 10:01:13.28 YRFCj/Kr.net モデルがなぜそのための道具になりえるとしたら、それはモデルが何だからか考えてみな 次ページ最新レス表示レスジャンプ類似スレ一覧スレッドの検索話題のニュースおまかせリストオプションしおりを挟むスレッドに書込スレッドの一覧暇つぶし2ch