【Alloyの概要説明】

本実験で用いるAlloyの概要について説明します．
現時点で本ページの内容を完全に理解する必要はありません．課題に取り組む際に必要に応じて本ページを参照しながら進めるようにください．

形式的仕様記述言語とは？

Alloyは代表的な形式的仕様記述言語の一つです．
形式的仕様記述言語とは，仕様を自然言語ではなく，論理式のような数学的に厳密に意味が定義された形式で記述する方法で，

といった特長を持っています．
コンピュータによる解析としては，仕様レベルで不具合が存在しないかを網羅的に調べたり，セキュリティホールが存在しないことを確認することなどが挙げられます．
形式的仕様記述言語による記述は，通常のプログラミング言語におけるソースコードの記述とはかなり異なっております．そのため，最初に形式的な仕様記述を見ると少々戸惑うかもしれません．
一般的に形式的仕様記述言語の表現能力はプログラミング言語よりも低く，表現能力が低くなればなるほど複雑な振る舞いが記述できなくなる一方で，強力な解析ができるといった関係が成り立っています．

Alloyとは？

Alloyは形式的仕様記述言語の一つで，比較的表現能力が高いため完全に網羅的な解析はできませんが，実用性を大きく損なわない範囲で網羅性を制限した解析を行うことができるといった特長があります．
本実験では，Alloyによる仕様記述と仕様の仮想実行に着目しており，Alloyによる解析は行いません．そのため，AlloyのツールをPCにダウンロードして操作していただく必要はありません．

Alloyによる仕様記述

Alloyでは，集合と関係を中心に仕様を記述していきます．また，その記述は宣言的な形式で行われます．
宣言的記述の対義語は手続き的記述です．我々が通常用いるプログラミング言語では手続き的な記述が用いられています．手続き的な記述ではプログラムは基本的に一番上の行から順番に一行ずつ記述された順に実行されていきます．
一方宣言的な記述では，記述の順序は関係ありません．すべての行が同時に成り立っていると考えます．連立方程式を考えてみると解りやすいと思います．連立方程式では，すべての式が同時に成り立っているため，式の記述順に関係なく同じ解が得られます．
そのため，宣言的記述には時間の経過がありません．実行の初期状態から最終状態までのすべての状態が同時に存在していることになります．概念的な説明はこれくらいにして，Alloyの具体的な記述を見ていきましょう．