tmiyaさんが出している問題に触発されました。 http://study-func-prog.blogspot.com/2010/07/coq-coq-99-part-1.html数をこなせば自然と出来るようになるのではないか。 Section FoundationOfSoftwareScience. Lemma e_1_23 : forall A B C : Prop, (A -> B…

連載：モデリング技術の新しい動向 第3回 形式手法とモデリング - Alloy Analyzerを中心にという記事が掲載された。 http://thinkit.co.jp/story/2010/09/22/1766今回はFormal Methods Forumのみなさんの力を借りられなかったのが心残り。最低限の査読は入っ…

Alloy Analyzerはアジャイルモデリングをサポートできるツールだと 思っているわけですが、現時点では識別子に日本語が使えません。 このままだと分析モデリングに使えない(と、会社の人が文句を言ってきた)。コードを調べてみたら何のことはなかったので、…

ASDF(Another System Definition Facility)というのはCommon Lisp版パッケージ管理ライブラリ(http://www.cliki.net/asdf)。Windowsではどうにも動いてくれないなーと思っていたが。 http://f34.aaa.livedoor.jp/~kumadasu/pukiwiki/index.php?Maxima#w69d91…

http://alloy.mit.edu/community/node/506 に、LaTeXでAlloyのリストを表示するサンプルがあったので試す。 \documentclass{jarticle} \usepackage{amsmath} \usepackage{listings,jlisting} \lstdefinelanguage{Alloy} {morekeywords={abstract, all, and, …