前回の続き．
Chapter. 2
ファイルシステムを記述した例をもとに説明を行う．
// A file system object in the file system
sig FSObject { parent: lone Dir }// A directory in the file system
sig Dir extends FSObject { contents: set FSObject }// A file in the file system
sig File extends FSObject { }// A directory is the parent of its contents
fact { all d: Dir, o: d.contents | o.parent = d }// All file system objects are either files or directories
fact { File + Dir = FSObject }// There exists a root
one sig Root extends Dir { } { no parent }// File system is connected
fact { FSObject in Root.*contents }// The contents path is acyclic
assert acyclic { no d: Dir | d in d.^contents }// Now check it for a scope of 5
check acyclic for 5// File system has one root
assert oneRoot { one d: Dir | no d.parent }// Now check it for a scope of 5
check oneRoot for 5// Every fs object is in at most one directory
assert oneLocation { all o: FSObject | lone d: Dir | o in d.contents }// Now check it for a scope of 5
check oneLocation for 5
上記の記述に関する段階的説明がなされる．
// A file system object in the file system
sig FSObject { parent: lone Dir }
「//」はコメントアウト．
sig はシグネチャ（sigunature）の略で，集合を表す．
この FSObject は高々一つ（0 個または 1 個）の parent という Dir の要素をもつ（Dir の定義はこのあと）．
// A directory in the file system
sig Dir extends FSObject { contents: set FSObject }// A file in the file system
sig File extends FSObject { }
Dir という集合は FSObject の部分集合（extends）で，その要素の contents は FSObject の部分集合である．
同様に，File という集合も FSObject の部分集合．
Dir も File も FSObject の部分集合で，別々に定義されているので共通部分を持たない部分集合とみなされるっぽい．
extends というのがかなりオブジェクト指向っぽいし，実際そうみなせる．
// A directory is the parent of its contents
fact { all d: Dir, o: d.contents | o.parent = d }
fact は「必ず成り立つべき」「成り立つことを前提とする」という制約条件を記述するためのもの．
ここでは，「Dir のどの要素 d および d のどの contents o も，d が o の親」，言い換えると，「d の contents o の親は必ず d」といっている．
Alloy では，記載した内容の具体例を探すとき， fact を満たさない例を切り捨てるようである．
// All file system objects are either files or directories
fact { File + Dir = FSObject }
演算子「*」は非交和（disjoint union）を表す．ここでは，File と Dir は非交和で，FSObject の要素はこのどちらかに限ると制約している．
// There exists a root
one sig Root extends Dir { } { no parent }
ファイルシステムにはルートディレクトリが存在する（Linux では "/" ）．
修飾子 one は「ちょうど一つ」であり，要素を持たない．{} が二つあるが，二つ目は追加の制約条件であり，Root は親を持たないと制約している．以下のように書いてもいいらしい：
sig Root extends Dir { }
fact { one Root }
fact { no Root.parent }
次いきます．
// File system is connected
fact { FSObject in Root.*contents }
"in" は部分集合を表すので，FSObject は "Root.*contents" の部分集合である．
また，"*" は「反射的で推移的な閉包（？）」で，Root，Root.contents，Root.contents.contents, ... の和を表す．正確には，三つ目は Root.contents の各元の contents の和集合，のはず．以下同様．
つまり，FSObject の元は Root からたどっていけるということを表していて，言い換えると，連結な有向グラフの構造を持っていることをファイルシステムに課している．
// The contents path is acyclic
assert acyclic { no d: Dir | d in d.^contents }// Now check it for a scope of 5\
check acyclic for 5
assert は成り立つかどうかをチェックしたい条件式を記述するためのもので，ここでは "acyclic（非輪体）" ，つまり循環を持たないグラフであることをチェックしようとしている．
"^" はさっきの "*" とは違って，0 回の推移を許さない．つまり，d.^contents は d.*contents - d を表している，はず．
check acyclic は acyclic が成り立つかを調べる（凡例を探す）ということで，ここでは 5 個オブジェクトを含む場合について調べようとしている．
// File system has one root
assert oneRoot { one d: Dir | no d.parent }
親を持たないようなディレクトリ d がちょうど一つ存在する．
// Every fs object is in at most one directory
assert oneLocation { all o: FSObject | lone d: Dir | o in d.contents }
どの FSObject o に対しても，たかだか一つのディレクトリ d が存在して，o は d の contents の元である．
縦棒 | は such that の略記かなと思ったけど，この文ではそう解釈できないので，区切り程度の意味なのかなと思う．詳しくは，別途本を読んでいきたい．
チュートリアルにかかれていることの解説に終止してしまいました．
自分用の文法まとめを作っていければと思います．
コメント