从 A 到 Z 的建模/建模原则/A 代表 Alloy 分析器
Alloy 是一种 形式语言，其根源深厚地扎根于 Z[1]。它由目前在 MIT 工作的 Daniel Jackson 开发。Daniel 是 Michael Jackson 的儿子，以其对计算的贡献而闻名。
Alloy 分析器 是由目前在 MIT 工作的 Felix Chang[2] 开发的约束分析器。
让我们以 地址簿[3] 的经典示例为例，并将其转换为数字艺术画廊目录的形式等效模型。在这里，我们考虑的是画作名称[4]。实物画作只位于一个地方。但是该画作的数字形式（我们将称为数字图像）可能位于许多不同的地方。此类数字图像将受到控制，以确保质量、版权等。为了激发工作，我们将重点关注一个现实世界的示例：数字艺术展。
但首先让我们从地址簿开始。在当今世界，我们可能想到姓名和网址、姓名和电子邮件地址等。潜力巨大。让我们保持保守并享受一些乐趣？这是一个简单的旧式地址簿
| 姓名 | 地址 |
|---|---|
| Harry Knooall | Black Rock，Big Peak 县 |
| Martha Underwude | Black Rock，Big Peak 县 |
| Charlie Bigfoot | 在路上 |
| Mary Wethervain | White Rock，Big Peak 县 |
构建模型需要投入时间和精力。开发有意义的模型有助于理解模型构建过程。这会让人对模型产生一种所有权感。人们可以尝试上面这个简单模型。例如，如果对监狱系统感兴趣，可以将“Black Rock”更改为“Black Rock 监狱”或“Black Rock 拘留所”，并将“在路上”更改为“在逃”。
让我们以 Jackson 在他的书[5] 中使用的第一个示例为例
module addressbook
sig Name, Addr {}
sig Book {
addr: Name -> lone Addr
}
特殊关键字 lone 需要解释。它表明每个姓名最多映射到一个地址。有人可能没有地址。在我们的简单模型中，“Charlie Bigfoot” 通常没有地址。所以，只是为了好玩，我们给了他[6] 一种特殊的地址“在路上”。
我们可以了解我们简单模型的图片。
|
|
| addressBook 简单模型的结构 | addressBook 简单模型的结构 使用 Magic 布局 |
左侧的图像是 Alloy 分析器中的默认布局；右侧的图像是“Magic 布局”。
我们的下一步是生成一些典型的地址簿。我们特别想看看是否可以生成一个与我们开始使用的旧式地址簿相对应的示例。
pred show () {}
run show for 4 but 1 Book
紧随 Jackson 开发模式，添加谓词 show 以在每个签名中获得最多 4 个对象：Name 和 Addr，但只有一个 Book 对象。
所以！我们可以认为“Harry Knooall” 拥有 Name1，“Martha Underwude” 拥有 Name0，“Black Rock，Big Peak 县” 由 Addr2 表示，依此类推。换句话说，我们确实有一个适合我们心中地址簿类型的良好工作模型。现在我们该怎么办？
让我们从简单的对应开始。地址簿将姓名与地址相关联。展览目录将数字图像（画作或其他作品）名称与网址相关联。
我们直接用模块名称跳入
module exhibitionCatalog
下一步是引入一个抽象签名，我们将称为 Xpoint[7]。Xpoint 背后的理念是指示 XML 命名空间中的某个端点。
abstract sig Xpoint {}
现在我们可以准确地定义数字图像（画作或其他作品）的网址。
sig WebAddr extends Xpoint {}
我们也考虑名称组的可能性。该组的目的是涵盖艺术主题的概念，例如印象派、立体主义等等。让我们尝试使用 ArtTheme 来表示此类组？
类似地，别名是另一个名称的名称。很多情况下，一件艺术作品会有一些名称，例如《母子》。也可能出现这种情况，即编目者会使用别名，例如“芝加哥圣母”，指代完全相同的艺术作品。使用 Alias 用于此目的似乎很方便。但是，为了避免此新（同构）模型与原始 Jackson 模型之间的混淆，我们将使用 OtherName。ArtTheme 和 OtherName 都是名称类型，用于识别单词。但 Name 用于原始 Jackson 模型中。让我们改用 Identity 这个词。就像 Xpoint 位于 XML 空间中一样，为什么不考虑 Identity 作为 Xpoint 的一种类型呢？
abstract sig Identity extends Xpoint {}
现在我们可以将 ArtTheme 和 OtherName 定义为 Identity 的扩展
sig ArtTheme extends Identity {}
sig OtherName extends Identity {}
为了方便起见，人们可能希望在一行中将前面两个定义包装起来
sig ArtTheme, OtherName extends Identity {}
最后，ArtExhibitionCatalog 通过在 Identity（艺术作品的）和 Xpoint（其所在的位置）之间建立关系来确定。
sig ArtExhibitionCatalog {webAddr: Identity —> Xpoint}
现在我们将所有内容整合在一起
module exhibitionCatalog
abstract sig Xpoint {}
sig WebAddr extends Xpoint {}
abstract sig Identity extends Xpoint {}
sig ArtTheme, OtherName extends Identity {}
sig ArtExhibitionCatalog {webAddr: Identity -> Xpoint}
首先要做的是展示元模型结构的图片
在学习模型的剩余部分时，打印或绘制此图片可能是个好主意。
现在我们准备好玩玩我们的简单模型了。在我们开始之前，倾听 Daniel Jackson 对此主题的见解非常值得
«使用分析器逐步构建模型，边模拟边检查，这与单独使用纸笔有很大的不同。最开始的反应往往是惊讶：当您获得即时、直观的反馈时，建模会变得更加有趣。当您模拟部分模型时，您可以立即看到示例，这些示例建议添加新的约束。»[8]
展示正在发生情况的最基本方法是使用谓词 show。这里，我们想展示与我们的 ArtExhibitionCatalog 相关联的 一些 可能的 webAddress
pred show (aec: ArtExhibitionCatalog) {some aec.webAddr}
我们希望将模型的探索范围限制在每个签名中最多 3 个对象，除了 *ArtExhibitionCatalog* 限制为 1 个对象。
run show for 3 but 1 ArtExhibitionCatalog
最后，为了了解*ArtExhibitionCatalog*的状况，我们对其进行投影。也就是说，我们知道只有一个。让我们把它放在背景中，看看剩下的画面是什么样的。这是一个这样的结果。
消除身份循环
[edit | edit source]我们必须回去修正模型。具体来说，可以添加这样一个事实：对于任何 *ArtExhibitionCatalog*，都没有 Identity 存在于可以从该 Identity 访问的一组 Xpoints 中。换句话说，循环（即绕圈）是不可取的！
我们将其表述为
fact {
all aec: ArtExhibitionCatalog | no id: Identity | id in id.^(aec.webAddr)
}
从 OtherNames 到 Xpoints
[edit | edit source]现在让我们考虑以下结果
pred show (ace: ArtExhibitionCatalog) some OtherName.(ace.webaddress)}
从 addressBook 到 vCard
[edit | edit source]从简单的地址簿开始，我们可以朝着 vCard 的方向前进。任务是找到一种简单的方法，逐步构建 vCard 模型。为什么不从维基百科文章中给出的示例开始呢？
BEGIN:VCARD VERSION:2.1 N:Gump;Forrest FN:Forrest Gump ORG:Bubba Gump Shrimp Co. TITLE:Shrimp Man TEL;WORK;VOICE:(111) 555-1212 TEL;HOME;VOICE:(404) 555-1212 ADR;WORK:;;100 Waters Edge;Baytown;LA;30314;United States of America LABEL;WORK;ENCODING=QUOTED-PRINTABLE:100 Waters Edge=0D=0ABaytown, LA 30314=0D=0AUnited States of America ADR;HOME:;;42 Plantation St.;Baytown;LA;30314;United States of America LABEL;HOME;ENCODING=QUOTED-PRINTABLE:42 Plantation St.=0D=0ABaytown, LA 30314=0D=0AUnited States of America EMAIL;PREF;INTERNET:[email protected] REV:20080424T195243Z END:VCARD
我们的首要任务是确定“关键词”的含义，这些关键词显然是大写的。我们识别出 TITLE、WORK、VOICE、HOME 等等。但 N、FN、REV 究竟是什么？这些“关键词”被称为属性。属性的基本列表是 FN、N、NICKNAME、PHOTO、BDAY、ADR、LABEL、TEL、EMAIL、MAILER、TZ、GEO、TITLE、ROLE、LOGO、AGENT、ORG、CATEGORIES、NOTE、PRODID、REV、SORT-STRING、SOUND、URL、UID、VERSION、CLASS、KEY。让我们首先将这些属性组织成一个表格。现在我们不会填写所有细节。
| key | meaning | example | comment |
|---|---|---|---|
| FN | 格式化的名称 | Mr. Harry Knooall jnr | "这是名称的显示方式"[9] |
| N | 名称 | KNOOALL;Harry;Mr.;Jnr | "对人、地点或事物的名称的结构化表示"[10] |
| PHOTO | 照片 | • | "此属性指定与 vCard 关联的个人的图像或照片。"[11] |
| JPEG | 照片格式类型 | • | "此属性参数用于指定照片属性值的图形格式。属性参数包括..."[12] |
| BDAY | |||
| ADR | |||
| LABEL | |||
| TEL | |||
| ADR |
http://www.imc.org/pdi/pdiproddev.html
Notes
[edit | edit source]- ↑ "就像 Z 一样，它用最少的数学概念工具集描述了所有（时空）结构，" Jackson 2006，第 xii 页
- ↑ e-Links 中提供了关于 Felix Chang 的一些简要信息。
- ↑ 我们使用 addressBook2 作为从 Daniel Jackson 的著作《软件抽象》第 17 页摘取的关键示例
- ↑ 在实际工作中，我们将使用数字照片作为我们展览中的数字图像。这些数字照片将在通常的 Creative Commons 许可下免费提供。
- ↑ 我们对 Jackson 的模型进行了一些简化。他的模块（第 6 页）有一个更长的标题“tour/addressBook1”。
- ↑ 重要的是要对名字的可能含义持开放态度。我说的是*他*。我也可以说*她*。如果我们想对性别进行具体说明，那么我们必须对它进行建模：例如，*女性*、*男性*、*其他*。
- ↑ Jackson 使用了 Target 这个名字，第 17 页。很难想象一个人如何会想出这种特殊的方式。换句话说，从如此抽象的签名开始似乎需要先前的知识。这种先前的知识似乎需要大量的复杂性或直觉。
- ↑ Jackson 2006，第 xiii 页
- ↑ vCard 版本 2.1 规范
- ↑ vCard 版本 2.1 规范
- ↑ vCard 版本 2.1 规范
- ↑ vCard 版本 2.1 规范
阅读链接
[edit | edit source]- Jackson, Daniel (2006). 软件抽象：逻辑、语言和分析. 肯布里奇，马萨诸塞州：麻省理工学院出版社. ISBN 978-0262101149.
{{cite book}}: Check|isbn=value: checksum (help); Cite has empty unknown parameter:|coauthors=(help)
e-Links
[edit | edit source]- Felix Chang 最后访问时间 {2008-08-15}
vCard
[edit | edit source]- 在 RDF/XML 中表示 vCard 对象
- vCard, 电子名片，版本 2.1. versit 联盟规范，1996 年 9 月 18 日