別讓 Alloy 的 fact 讓你的規格淪為虛構
原文由 Hillel Wayne 于 發布，訂閱此部落格
最近我做了不少 Alloy 相關的工作，讓我開始思考一個常見的規格陷阱。本文主文的所有內容都適用於所有的形式化規格，而下拉選單裡的內容則是給有經驗的 Alloy 使用者看的。
來考慮一個簡單的依賴樹模型。我們的程式有一組頂層依賴，而這些依賴本身又有各自的依賴，以此類推。我們可以在 Alloy 中這樣建模：
sig Package {
, depends_on: set Package
}
run {some depends_on}顯示 Alloy 小技巧
接下來的範例我會使用稍微不同的模型：
abstract sig Package {
, depends_on: set Package
}
lone sig A, B extends Package {}
run {some depends_on}我這樣做是因為視覺化時會顯示 A 和 B，而不是 Package$0 和 Package$1。Alloy 有內建的 enum，但它們跟語言的其他部分不太相容（你無法繼承它們，也無法為它們加上欄位）。
如果我們瀏覽一下產生的範例，會發現一件奇怪的事：套件竟然可以依賴自己！
在描述規格時，這種不合理的狀況經常出現，原因是我們心裡對系統應該是什麼樣子有個預期，卻沒有明確地把它寫進規格裡。遇到這種情況，我們就需要加上額外的限制來避免它。為此，Alloy 有一個特殊的關鍵字「fact」：1
fact no_self_deps {
all p: Package {
p not in p.depends_on
}
}顯示 Alloy 小技巧
你也可以完全用關聯式的方式來寫同一個 fact：
fact {
no depends_on & iden
}一般來說，模型檢查器評估純關聯式運算式的速度遠比帶量詞的運算式快得多。在大型模型中，這會有很大的差別！
Alloy 不會產生任何違反 fact 的模型，也不會在那些模型中去尋找不變性違規。它是「現實中的事實」，完全不需要去探索。
fact 的陷阱
「禁止自我依賴」是 fact 的一個很典型的範例。同時，它也是個非常糟糕的 fact 範例。新手經常會犯這種錯誤：用 fact 來建模系統，而這很快就會導致問題。
先別管規格，想一下真實的系統。套件管理器的依賴是從哪裡來的？通常是像 package.json 或 Cargo.toml 這樣的純文字檔。如果有人手動在那個檔案裡加入自我依賴呢？想必你會希望套件管理器能偵測到這個自我依賴，並將其當作錯誤拒絕輸入。你要怎麼知道錯誤處理是有效的？就是讓檢查器去驗證它能接受合法的 manifest，並拒絕帶有自我循環的 manifest。
但它現在沒辦法測試這種拒絕行為，因為我們已經告訴它不要產生任何自我依賴。我們的 fact 讓自我依賴變得無法被表示。
通常在程式語言中，「讓不合法的狀態無法被表示」（MISU）是一件好事（1 2 3 4）。但規格涵蓋的不只是你正在撰寫的軟體，還包括軟體所處的環境，也就是機器與世界。如果你無法表示不合法的狀態，就無法表示世界產生了需要你的軟體去處理的不合法狀態。
顯示 Alloy 小技巧
有一種技巧可以讓不合法的狀態在世界中可被表示、但在機器中不可被表示：精化（refinement）。連結指向的是 TLA+ 的說明，但同樣的原則在 Alloy 中也適用：寫一個不使用 MISU 的抽象規格，再寫一個使用 MISU 的實作規格，然後證明實作精化了抽象規格。不過你會用 signature 和 predicate 來做這件事，而不是用 fact。
與其用 fact，你應該使用 predicate。這樣你就可以測試 predicate 為真的情況，或檢查它是達成其他性質的必要條件。讓限制變得明確，而不是隱含的。
// instead of
fact no_self_deps {/*body*/}
run {some_case}
check {some_property}
// do
pred no_cycles {/*body*/}
run {
no_cycles and some_case
}
check {no_cycles implies some_property}Predicate 還有一個額外的好處是它是「區域性作用域」的：如果你有三個 fact，想用其中兩個來檢查模型，就得把第三個 fact 註解掉。
什麼時候該用 fact
那麼，我們到底該在什麼地方使用 fact？在什麼情況下，全面性地強制施加限制才是合理的，即使這麼做可能會弱化我們的模型？
第一，fact 適合用來限縮問題的範圍。如果我們只是在描述套件安裝器的行為，而驗證 manifest 的工作是由其他部分負責，那麼「禁止自我依賴」就是一個完全合理的 fact。把它寫成 fact，能清楚地讓讀者知道我們不負責驗證 manifest。這也意味著，如果這個假設不成立，我們就不提供任何保證。
第二，fact 可以用來排除根本不值得關注的情況。假設我在對鏈結串列建模：
sig Node {
next: lone Node //lone: 0 or 1
}這會產生一般的串列和帶有循環的串列，這兩種對我來說都是值得關注的。我不想把其中任何一種限制掉。但它同時也會產生包含兩個互不相連串列的模型。如果我只關心單一鏈結串列，就可以用一個 fact 來排除多餘的串列：
fact one_list {
some root: Node | root.*next = Node
}顯示 Alloy 小技巧
one_list 同時也會排除「兩個鏈結串列合併成一個」的情況。如果那是你想保留的情況，請使用 graph 模組：
open util/graph[Node]
fact {
weaklyConnected[next]
}同樣地，你也可以用 fact 來消除多餘的細節。例如我在對使用者與群組建模時，我不想要任何空的群組。我會加上像 Users.groups = Group 這樣的 fact。
第三，你可以用限制來最佳化執行緩慢的模型。這通常是透過對稱性破壞（symmetry breaking）來達成。
最後，你可以用 fact 來定義 Alloy 原生無法表達的必要關聯。在我參與的專案中，我們的圖裡有紅色和藍色的節點。紅色節點至少有一條邊連到其他節點，藍色節點則至多有一條。我們本來是這樣寫的：
abstract sig Node {
}
sig Red extends Node {
edge: some Node
}
sig Blue extends Node {
edge: lone Node
}但這樣一來，我們就無法針對節點寫使用 edge 的通用 predicate，因為 Alloy 會將其視為型別錯誤。因此我們改用 fact 來寫：
abstract sig Node {
edge: set Node
}
sig Blue, Red extends Node {}
fact {
all r: Red | some r.edge
all r: Blue | lone r.edge
}顯示 Alloy 小技巧
好吧，還有一個（相當小眾的）使用情境。假設你有一個時序模型，以及一個代表系統行為的標準 spec predicate。那麼你的許多 assertion 看起來會像這樣：
module main
// spec
check {spec => always (prop1)}
check {spec => always (prop2)}
// etc你可以把所有性質匯出到 properties.als，並改寫成這樣來大幅簡化：
open main
fact {spec}
check {always (prop1)}
check {always (prop2)}
// etc結論
限制是危險的，因為你需要錯誤狀態，才能檢查你的程式是否能避開錯誤狀態。
如果你想進一步了解 Alloy，這裡有一本不錯的書，而我也有維護一些參考文件。我目前也在籌備一個新的 Alloy 工作坊。上個月我剛進行了 alpha 測試，預計今年夏天稍晚會進行 beta 測試。歡迎訂閱我的電子報來掌握最新消息！
感謝 Jay Parlar 與 Lorin Hochstein 提供的回饋。如果你喜歡這篇文章，歡迎加入我的電子報！我每週都會在那裡發表新的文章。
我為企業提供形式化方法的培訓，讓軟體開發更快速、更便宜、更安全。歡迎在這裡了解更多。
留言
登入後參與討論