从 Alloy 角度与 UML 角度解释图表

Question

Software Abstractions 一书有一个对大量网络进程进行建模的示例。每个进程都连接到另一个进程。为了描述这一点，我在一张纸上画了这张图：

我将该图解释为：每个进程都有一个后续进程。

但后来我开始思考：这是不对的。如果它是 UML 模型，那么它是正确的，但它不是合金模型的正确描述。

经过一番思考，我得出了这样的描述：进程有一组（原子）值；每个值代表网络中的一个进程。 succ 有一组对，每对代表从一个进程到另一个进程的连接。 Process 中的每个值都与 Process 中的一个值配对。

你同意这个描述吗？您是否同意上图在 Alloy 中与 UML 中的表现截然不同？

也许上图更适合UML，下图更适合Alloy：

那会是更合适的合金图吗？

Answer 1

如果您将语义赋予 UML 类图作为抽象数据模型（而不是代码草图），那么您给出的解释似乎是合理的——您给出的合金版本只是相同的形式化解释。你给的第二张图是一种实例图，我会用它作为给第一张图语义的一种方式：也就是说，类图的含义是一组可能的实例图。