+ 本実験で用いるAlloyの概要について説明します．
+ 現時点で本ページの内容を完全に理解する必要はありません．課題に取り組む際に必要に応じて本ページを参照しながら進めるようにください．
+
+ Alloyは代表的な形式的仕様記述言語の一つです．
+ 形式的仕様記述言語とは，仕様を自然言語ではなく，論理式のような数学的に厳密に意味が定義された形式で記述する方法で，
+
+ Alloyは形式的仕様記述言語の一つで，比較的表現能力が高いため完全に網羅的な解析はできませんが，実用性を大きく損なわない範囲で網羅性を制限した解析を行うことができるといった特長があります．
+ 本実験では，Alloyによる仕様記述と仕様の仮想実行に着目しており，Alloyによる解析は行いません．そのため，AlloyのツールをPCにダウンロードして操作していただく必要はありません．
+
+ Alloyでは，集合と関係を中心に仕様を記述していきます．また，その記述は宣言的な形式で行われます．
+ 宣言的記述の対義語は手続き的記述です．我々が通常用いるプログラミング言語では手続き的な記述が用いられています．手続き的な記述ではプログラムは基本的に一番上の行から順番に一行ずつ記述された順に実行されていきます．
+ 一方宣言的な記述では，記述の順序は関係ありません．すべての行が同時に成り立っていると考えます．連立方程式を考えてみると解りやすいと思います．連立方程式では，すべての式が同時に成り立っているため，式の記述順に関係なく同じ解が得られます．
+ そのため，宣言的記述には時間の経過がありません．実行の初期状態から最終状態までのすべての状態が同時に存在していることになります．概念的な説明はこれくらいにして，Alloyの具体的な記述を見ていきましょう．
+