合金初心者です。
私は、Alloy で制約を作成し、モデルが制約に従って有効であることをアナライザーにチェックさせるのが本当に好きです。
しかし、「これらの制約の定義は単なる頭の体操ですか? それとも、より良いソフトウェアの構築に役立つでしょうか?」</p>
具体例を挙げてみましょう。電子メール クライアントのアドレス帳のモデルでは、アドレス帳に新しいエントリを追加するために次の制約を定義できます。
新しいブック b' のアドレス マッピングは、古いブック b のアドレス マッピングと同じですが、名前からアドレスへのリンクが追加されています。この制約は Alloy では次のように表されます: b'.addr = b.addr + n->a
それは美しいです。
しかし、追加操作がコードに実装されている場合、その関連性を確認するのに苦労しています。たとえば、Common Lisp でadd操作を実装しました。
(defun add (b n a)
"Add a new entry, (n a), to address book b"
(adjoin (list n a) b :key #'first))
つまり、「これはaddという名前の関数の定義で、3 つのパラメーターb、n、およびa (本、名前、住所) を持ちます。Common Lisp の set 関数adjoinを使用して、リスト ( na ) をbに追加します。"</p>
その関数は、単純な追加関数を正しく実装しているようです。Alloy で定義した拘束はどうすればよいですか? 制約を表現する追加のコードを作成する必要がありますか? 擬似コード: [1]
(defun add (b n a)
"Add a new entry, (n a), to address book b"
(adjoin (list n a) b :key #'first)
Check that nothing has changed in the
address book except that it now has
a n->a mapping)
このようなコードを書くのは大変な作業のように思えますが、明らかなメリットはありません。
私の質問は次のとおりです: コードで Alloy モデルを実装する場合、Alloy で定義されている制約をどうすればよいですか?
また、Alloy モデルをコードに変換する方法を説明するチュートリアルはありますか? コードで Alloy 制約定義がどのように使用されるかの説明が含まれていますか?
ありがとうございました。
[1] 注: Common Lisp には Screamer という制約プログラミング用の言語拡張があることを認識しています。