如何表示顺序操作模式[Z表示法]

Question

我有一个操作模式C，它由两个顺序操作模式A和B组成。A必须在B之前执行。我不知道如何表示模式激活的顺序。

我可以使用模式连接吗，例如C == A∧B？或者，有没有办法从A中“调用”模式B？

我是Z-notation的新手，任何帮助都将不胜感激！

Answer 1

模式只是包装一大块数学的一种方式。

有一种相当标准的方式将该数学解释为描述ADT。一个模式表示状态变量和它们之间的约束，一个模式表示初始化，以及与ADT接口中的操作一样多的模式表示操作。

您可能正在寻找向前模式组合，C == A⨟B。

Answer 2

有关大型Z规范的示例，我建议您使用最近上载的项目：https://github.com/vinahradau/finma

以下模式连接在CZT中有效。在这里，C不是从B调用的，而是在B之后调用的。

─
  A == B ∧ C 
└