在教程的第二部分中，为什么Alloy可以用父元素组成根

Question

在Alloy教程的文件系统第二课中，描述了以下模型：

// A file system object in the file system
abstract sig FSObject { }
// File system objects must be either directories or files.
sig File, Dir extends FSObject { }
// A File System
sig FileSystem {
root: Dir,
live: set FSObject,
contents: Dir lone-> FSObject,
parent: FSObject ->lone Dir
}{
// root has no parent
no root.parent
// live objects are reachable from the root
live in root.*contents
// parent is the inverse of contents
parent = ~contents
}

注意no root.parent事实。

问题是：既然根是Dir，而Dir没有父关系，为什么Alloy可以将根与父组成？(只有FileSystem具有父关系(

Answer 1

通过将parent定义为FileSystem的字段，它得到类型

FileSystem -> FSObject -> Dir

在签名事实中，有一个隐含的this，所以root.parent是(this.root).(this.parent)的缩写，这意味着我们加入了类型Dir和FSObject -> Dir。由于FSObject包括Dir，所以该联接不是冗余的，并且产生类型为Dir的集合。