Alloyは、論理学の力で限定的に世界を記述し、その記述された世界を満たすような状態があるかどうか、あるとすればどのような状況か、を示してくれる、一種のプログラム的なものです。このような方法で状態や制約無矛盾性を探る手法を、形式手法と呼びます。 プログラム的なものなので、プログラミングをしたことがない人にとっては少し「とっつきにくい」ところがあるかもしれません。 それではプログラマには簡単なのかと言われると、プログラム的であるにもかかわらず、これまでのプログラミング言語とはかけ離れた考え方をしないといけないところもあって、そのへんが普通のプログラマから見ても「とっつきにくい」印象を与えているように思えます。既存の言語では「SQL」が割と近い、と言えば、分かる人には分かってもらえるかもしれません。SQLはすでに存在するテーブル上のレコードに対して条件を満たすレコードを抜き出してきますが、Al
