PFI の社内セミナーで Alloy Analyzer について発表してきました。
なんか ust でストリーミング放送された上、録画・保存されてしまっているらしいので、観てやろうという酔狂な方は下からご覧になったらいいんじゃないでしょうか。
なんだか台本とか特に考えずに書いたので、早口かつしどろもどろと云うか何か何云ってるのか良くわからない感じになっちゃってますね……反省。
補足
日本語をソースで使うには、4.2RC を使う必要があります。
さて。訳者の一人でいらっしゃる id:bonotake さんやさかいさんから幾つか補足がありましたので紹介します。
- 発表では「有界モデル検査器」と紹介しましたが、公式には「有界モデル発見器」と呼ぶそうです。
- 発表では assert を「不変条件」と表現していましたが、より広い概念なので「表明」とか「アサーション」と表現する方が適当でした。
- 矛盾したファクトを判別する方法がありました。
- MiniSAT が使える環境では、MiniSat with Unsat Core を SAT Solver に指定すると、矛盾する箇所をハイライト出来ます
- Options Menu の Unsat Core Minimization Strategy で矛盾箇所の粒度/速度を指定出来ます
