我有一个操作模式 C，它由两个顺序操作模式 A 和 B 组成。必须在 B 之前执行 A。我被困在如何表示模式激活的顺序上。
我可以使用模式连词，即 C == A ∧ B 吗？或者有没有办法从A“调用”模式B？
我是 Z 表示法的新手，任何帮助将不胜感激！
问问题
117 次
2 回答
1
模式只是包装一大块数学的一种方式。
有一种相当标准的方法可以将该数学解释为描述 ADT。一种模式表示状态变量和它们之间的约束，一种模式表示初始化，并且表示操作的模式与 ADT 接口中的操作一样多。
您可能正在寻找前向模式组合，C == A ⨟ B。
于 2019-08-16T12:21:16.597 回答
0
举个大 Z 规范的例子，我推荐这个最近上传的项目：https ://github.com/vinahradau/finma
以下模式连接在 CZT 中有效。这里，C 不是从 B 调用的，而是在 B 之后调用的。
─
A == B ∧ C
└
于 2020-05-03T19:16:23.263 回答