Alloyでパックマン - keigoiの日記
Alloyを使ってみた。 数年前に使ったときはなんでこんなの使うのと思っていたけど考えが変わったのだ。 ちょっとした規模のプログラムを書くには設計が必要だ。 コードを書く前に、問題の本質的な部分を知っておこう。 本質がわかっていれば、 適切な部分にモジュール分割したり、適切なライブラリを選択したり、アルゴリズムを書いたりできるはずだ。 もちろんお絵描きツールでもいいのだけど、動いたりチェックしたりできれば、設計で得られる知見はより多くなるはず。 述語論理で書くけれど、モデルが絵になるのが直感的でよい サクサク設計するために Alloy が使えないか ? Alloyについて Alloy は 一階述語論理でモデルを書く。 だから概念は Prolog に近いかもしれない。 いわゆる公理的意味論というやつだ。 が書ける述語はホーン節に限らず自由である。 モデルと制約を自由に書ける。 そのかわり？
CafeOBJ 入門
このディレクトリで提供しているドキュメントは、CafeOBJ の初学者への手引きである。主に自然数の仕様を例題として用い、仕様記述から証明までの流れを体験してもらうことを主眼に置いている。 このドキュメントは、次のように構成されている: CafeOBJ 処理系の使い方 CafeOBJ 処理系の起動と終了方法 仕様の記述法 仕様を CafeOBJ 処理系に読み込ませる CafeOBJ の基本的な文法などの仕様の記述法 コメント モジュール ソート 輸入 オペレータ 等式 変数 定義済みモジュールの表示 項の構文解析 項の簡約 証明譜を用いた証明法 証明譜とは 組み込み述語 = 結合律の証明 交換律の証明 補足 トラブル発生時 内蔵モジュール 識別子で日本語を使う 練習問題 改訂履歴 2008-02-06 「識別子に日本語を使う」を追加した。 2007-09-25 「証明譜とは」の証明ログのダ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
らくがきえんじん