このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

Alloyを理屈っぽく考えてみようと思う

Alloy本=『抽象によるソフトウェア設計』が出版された直後、しばらく僕はAlloyで遊んでました。「『抽象によるソフトウェア設計』とAlloy、第一印象報告」あたりからいくつかAlloy関係の記事を書いています。でも、2,3週間で「ちょっと飽きたかなー」と。サンプルの人生モデリングも途中までで、続編は西尾さんにお任せ(「お願いした続編です: Alloyで人生モデリング」)。

このとき僕は、Alloy本をソフトウェアのマニュアルとして読んでいて、Alloyアナライザーを使うために必要な箇所を拾い読みしただけです(著者、翻訳者の皆さん、ゴメンナサイ)。最近になって、頭から(でも第2章はスキップ)読んでます。Alloyアナライザーの背後にある理屈のほうを読み取ろうと思っています。

キッカケはスピヴァックの関手データモデルです。「デイヴィッド・スピヴァックはデータベース界の革命児か -- 関手的データモデル」のコメント欄でid:bonotakeさんとのやり取り(http://d.hatena.ne.jp/m-hiyama/20130128#c1359936671 )で、

AlloyモデルとRDBが似てる、とかじゃなくて、まったく同じ概念を具現化しているとなれば、Alloyでデータベース設計やプロトタイピングがすごく実際的になる気がします。

関手データモデルとAlloyは、かなり親和性が高いんじゃないか、と感じるのです。以前から、Alloy圏論的に解釈できないか?とは考えていて、「Alloyの矢印記法と、モノイド閉圏としての関係圏」、「Alloy、コンパクト論理、関係圏」なんて話も書きました。また、関手データモデルを理解する道具としてAlloyが役に立つとも言えます。

と、そんな事情で、Alloy本=『抽象によるソフトウェア設計』を読み直しながら、Alloyを理屈っぽく考えてみようと思っている次第です。

抽象によるソフトウェア設計−Alloyではじめる形式手法−

抽象によるソフトウェア設計−Alloyではじめる形式手法−