2011-06-07から1日間の記事一覧
最終章「プログラムの論証」の後半です。「コンパイラーの正しさ」として少し長い例題が提示されているので写経しました。 加算を扱う式(Expr)をスタックマシンのコード(Code)に変換する関数 comp の正しさを検証 exec (comp e) [] = [eval e] を証明すれば…
最終章「プログラムの論証」の後半です。「コンパイラーの正しさ」として少し長い例題が提示されているので写経しました。 加算を扱う式(Expr)をスタックマシンのコード(Code)に変換する関数 comp の正しさを検証 exec (comp e) [] = [eval e] を証明すれば…