问将check命令作为合金中的完整模型
EN

Stack Overflow用户

提问于 2014-12-04 23:59:45

回答 1查看 55关注 0票数 1

在第132页的合金书(软件摘要)中，有人说以下命令是一个完整的合金模型：

check {all p,q: univ -> univ, s: set S | (p.s).q = p.(s.q)}

我将其放入合金工具并执行，但是合金抱怨S。这是书中的错误吗？

回答已采纳

发布于 2014-12-05 00:48:10

看起来确实很像。如果用'univ‘替换'S’，表达式就有意义了，Analyzer接受模型。

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/27306504

复制

相似问题

问将check命令作为合金中的完整模型EN