從 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:forrestgump@walladalla.com 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 日