重寫合金中的對象

Question

我一直在努力讓自己的項目更具動感，所以我決定編寫一個添加函數，我從合金網站上的這個例子中得到靈感：

pred add [b, b': Book, n: Name, t: Target] { 
    b'.addr = b.addr + n->t 
} 

但我想要做的是重寫兩個對象「b」和「b」（如我想添加到同一個對象），但我似乎無法找到辦法如何做到這一點。

如果任何人有一個想法，我會感謝

Answer 1

您不會錯過任何東西。你找不到「添加到同一個對象」的方法的原因是你不能。合金沒有突變;您不能更改模型中的任何對象。

在您的示例中，涉及突變的應用程序通常建模爲add：使用兩個參數顯示前置狀態和後置狀態。在這樣的模型中，任何兩個Book對象B1，B2將顯示相同的可變Book對象的不同狀態在應用領域，當且僅當存在一些Ñ，噸使得添加[B1， b2，n，t]成立。