スタートAlloyに参加してきた日記
- 「試行錯誤の過程が一番面白い」全く同意
- 「形式手法と一言で言っても定理証明系とモデル検査と形式仕様記述言語とは中身が全然違う」
- フィールドの宣言で X one -> one Y みたいに多重度を指定できる
- runで指定するpredicateが引数を持っていてもよい。存在量化子みたいに働く。
- predの定義のところで角カッコを使っても良い
- そうか「追加して削除したら元に戻る」を検証する上で全順序の時間を導入する必要性はないのか
- assertを回帰テストみたいに使う。使うために残しておくこと推奨。
- Execute allを使うとよい
- 自分の書いたコードが正しいかどうか不安→避けがたい。同じ事を違う書き方で書いてみて、それが同値であることを検証してちょっと安心する
- Alloyの公式サイトのチュートリアル用のスライドを見る: Everything's a relation
- Visualizerの四角はドラッグで移動できる
- Visualizerで出力したXMLをOpenできる
- r: A->B->CからBを取るにはやっぱA.r.Cが正解らしい。
- ペアモデリングは興味深かった。でも初対面の人とのペアプロは疲れる。社内勉強会とかAlloy温泉とかやればいいのかな。
