私はしばらくの間、形式的な方法に興味を持っていました。私は、私が取り組んできたいくつかのプロジェクトのいくつかの非常に具体的なサブエリアについて、形式的な方法を使用して推論しました。正式な方法でドメイン全体を指定するどころか、他のチーム メンバーに同じことを試みるよう説得することはできませんでした。
私が特に興味深いと思った 1 つの方法は、Alloyです。概念的にも表記的にも実際のプログラミング言語に非常に近いため、プロジェクト全体の基盤としてより「スケーリング」できると思います。さらに、ツールは非常に堅牢であるため、モデル検証の利点をすぐに利用できます。
皆さんのプロジェクトで Alloy を使用した実際の経験についてお聞きしたいと思います。より良いドメイン モデルの設計に役立ったと思いますか? 検証中にドメイン モデルにエラーが見つかりましたか? また利用しますか？
私はいくつかのプロジェクトで Alloy を使用しましたが、それが役立つことがわかりました。これらのプロジェクトのすべてではありませんが、一部のプロジェクトでは、関係者に Alloy を使用するように、または少なくとも私が書いた Alloy モデルを使用するように説得することができました。これらのプロジェクトは、「現実世界」のプロジェクトを求める際にあなたが念頭に置いているものかもしれませんし、そうでないかもしれませんが、それらは確かに私が働いている現実世界の一部で行われました.
2006 年と 2007 年に、当時最新の W3C XProc 仕様のドラフト用に部分的な Alloy モデルを作成しました。私が知る限り、ワーキング グループのほとんどのメンバーは、私が書いた論文 ( http://www.w3.org/XML/XProc/2006/12/alloy-models/models.html ) を読んだことがありません。彼らは、「ああ、仕様のその部分を先週変更したので、モデルが言っていることはもはや関係ありません」と言いました. しかし、この論文は、仕様の最初のドラフトで説明されている抽象的な「コンポーネント」レベルがひどく指定不足であり、完全に指定するか削除する必要があることを仕様の編集者に納得させることができました. 彼はそれを落とし、仕様の読みやすさと使いやすさの点で (私が思うに) 良い結果をもたらしました。
2010 年にXPath 1.0 データ モデルの Alloy モデルを作成し、仕様のいくつかの不具合を明らかにしました。残念ながら、ほとんどの関係者 (XPath 1.0 仕様の保守を担当する W3C ワーキング グループを含む) の反応は、心強いものではありませんでした。
私が関与している研究プロジェクトでは、Alloy を使用して MLCD オーバーラップ コーパスをモデル化しました。これは、作成中のサンプル ドキュメントと関連情報のコレクションです (SO の主張によりハイパーリンクは省略されています)。Alloy モデルは、コーパス カタログの最初の設計でいくつかのエラーを発見したため、努力する価値が十分にありました。
また、Alloy を使用して、転写の性質と、タイプ/トークンの区別をドキュメント構造に拡張するために行ったモデリング作業を形式化しました (私たちの論文については、2010 年の Balisage: The Markup Conference の議事録を参照してください)。これは、ソフトウェア設計とは何の関係もないため、Alloy の通常のアプリケーション領域から少し外れていますが、モデルの整合性をチェックしてインスタンスを生成する Alloy の機能は、これまたはその可能性のある公理の論理的な結果のいくつかを示す上で非常に貴重です。私たちのモデルのために。
特定の質問に答えるには: はい、Alloy はよりクリーンなドメイン モデルを指定するのに役立ちました。また、エラーや不具合が見つかりました。Daniel Jackson が彼の著書Software Abstractionsで説明している理由により、それらはしばしば小さいものでした: まず、設計中にモデルを使用すると、すべてがまだ小さいうちにエラーを早期に発見できます。そして、2 番目に (ジャクソンの言葉で)、「後から考えると、ほとんどのソフトウェア設計の問題は些細なことです。」
彼は次のように続けています。私の経験はこれを十分に確認しています。そのような問題を早期に回避する方がはるかに良い. はい、また合金を使用します。
はい、私は合金を使用しました、そしてそれは工業的にいとこです。Alloyは、私のモデルがひどく間違っていなかったことを私に納得させるのに最も役立ちました---むしろ、どこが間違っていて、ばかげた結果をもたらしたかを私に示しました。SongのAthenaやGuttman、RamsdellのCPSAなど、他のより具体的なツールは、より狭い領域でより有用になっています。これ以上何について聞きたいですか？
遅ればせながらこのスレッドに追加します... Eunsuk Kang は最近、一部の新興企業の Web API のセキュリティ分析を実行するために Alloy を適用しました (Apurvaによる OAuth の分析や Barth らによるブラウザベースのセキュリティメカニズムの分析など、セキュリティにおける多くの Alloy の適用に続きます)。 CSRFなど); Pamela Zave は、ピア ツー ピア ストレージ システムである Chordの印象的な分析に取り組んでおり、最近、元のアルゴリズムの修正を書きました。