我正在创建 iCalendar 数据格式的合金模型。
iCalendar 文件包含属性。属性之间有很多相互依赖关系。我想看看删除属性时是否有任何中断（即，当属性被限制为零出现时）。
我想编写一个断言并让 Alloy Analyzer 搜索反例，但我正在为如何编写断言而苦苦挣扎。我希望断言说这样的话：
如果属性 X 被移除（即，属性 X 被限制为零出现），则没有因移除 X 而无效的实例。
在伪代码中，我想要这个：
assert NoProblemFilteringX {
(no prop: X | prop in iCalendar.properties) => all instances are still valid
}
请您提供一些有关制定所需断言的指导吗？
建议：
在将一组属性作为参数的谓词中编写您的相关性检查。谓词成立当仅当参数中给出的那些属性之间的相互依赖关系得到满足时。
重写您的事实，确保这些相互依赖关系，以便使用所有 iCalendar 属性集作为参数调用此谓词。
在断言中调用这个谓词，而这次iCalendar.properties - X作为参数给出
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句