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