• atwiki
  • 教えて!アロイ人!

教えて!アロイ人!

最終更新:

pleasealloy

- view
メンバー限定 登録/ログイン

教えて!アロイ人!~ Alloyにパズルの答えを教えてもらおう ~


Alloyって何?

Alloyは、論理学の力で限定的に世界を記述し、その記述された世界を満たすような状態があるかどうか、あるとすればどのような状況か、を示してくれる、一種のプログラム的なものです。このような方法で状態や制約無矛盾性を探る手法を、形式手法と呼びます。
プログラム的なものなので、プログラミングをしたことがない人にとっては少し「とっつきにくい」ところがあるかもしれません。

Alloyはプログラミング言語?

それではプログラマには簡単なのかと言われると、プログラム的であるにもかかわらず、これまでのプログラミング言語とはかけ離れた考え方をしないといけないところもあって、そのへんが普通のプログラマから見ても「とっつきにくい」印象を与えているように思えます。既存の言語では「SQL」が割と近い、と言えば、分かる人には分かってもらえるかもしれません。SQLはすでに存在するテーブル上のレコードに対して条件を満たすレコードを抜き出してきますが、Alloyはそのテーブル自身を条件に応じて自動生成して、条件を満たす組み合わせをその中から選ぶ感じです。内部的にはSATソルバという仕組みが動いています。

Alloyで何ができる?

Alloyは、プログラムの設計が正しいかどうかを検証する道具として、近年そちらの業界から注目をされていますが、「論理で世界を記述し、その条件を満たす解を探してくれる」ことが、実はパズルを解く際にとても強力な武器となることが知られています。

ここでは何をするの?

というわけで、このWikiでは、Alloyを使って簡単なパズルをどのように解いていくかを考えていくことにします。古典的な問題や、市販のクイズ本から問題をいくつか引用して、それをAlloyに解かせてみるのです。

そんなことして楽しいんですか?

パズルをわざわざコンピュータに解かせて楽しいかといわれると、そりゃぁ自分で解いたほうが楽しいに決まっています。僕もコンピュータにかける前に一度紙と鉛筆で解いてからコンピュータに向かいます。パズルはそのために生まれてきていますし。
しかし考えてください。パズルには、解があることが保証されていますし、紙と鉛筆で解いていく過程自体が楽しめるようにデザインされているものです。解が一つあるにしても、苦痛なほど総当りで条件チェックをしないと解けないようなパズルは出来がいいとはいえません。
ところが、現実に我々が直面している問題は、解がある保証もありませんし、解を見つける過程に紙と鉛筆で生きている時間にたどり着けるかどうかもわかりません。それでも我々は、そんな考えたくもないような問題に取り組まなければならないのです。こんなとき、Alloyが使えるならそれを使って解を探したほうがいいに決まっています。
「これはAlloyを使ったほうがいいぞ」と思えるような状況に遭遇したとき、すぐに取り組めるように、また、日常の問題に「これはAlloyで解ける」と気づくことができるようなセンスを養っておくために、日ごろからパズルを使ってトレーニングを積んでおくのです。
一番悪いのは、考えもせず、道具も使わないで「たぶん大丈夫」という結論を出すことです!!

入手とインストールの方法は?

おなじ@WikiのAlloy Analyzer で形式仕様記述を見ていただくのが一番かと思います。
こちらは少し「仕事」寄りですが、今日本語で読める貴重なAlloyの資料の一つです。

で?あなたは?

Alloyの勉強を始めたばかりのものです。Alloyは先日日本語の最初の本が出たばかりで、インターネット上にもまだまだ情報が多いとは言えない状況ですが、そんな中で、勉強の過程でわかったことを少しでも発信していければ、と思っているものです。そんな訳なので、「こんな風に書いたほうがいい」とか「こんな書き方は普通しない」というようなご意見があれば、ありがたく頂戴します。

(文責:片山 功士)


今日: -
昨日: -
トータル: -
目安箱バナー