首页 > 解决方案 > 在 Alloy 中“运行”一个函数是什么意思?

问题描述

我的理解是合金中的函数返回一个值。但是,我注意到您可以像使用谓词run一样使用命令运行函数。run运行一个函数是什么意思,这个函数在 Alloy 中是如何使用的?

标签: alloy

解决方案


在这方面,您可以将函数视为就像一个谓词:它是一个约束,当您运行它时,Alloy 会找到一个使约束为真的实例。在这种情况下,它将是函数的参数、签名和字段的值以及函数结果的集合。

运行一个函数,就像运行一个谓词一样,通过向您展示示例执行来让您更好地理解。把它想象成运行测试用例,但不必编写测试:-)


推荐阅读