递归在合金分析仪中是如何工作的？

Question

我看到合金分析器中有一个选项允许递归到特定深度 (1-3)。

但是如果递归深度有限，找不到反例怎么办？

会不会有错误或警告，或者这样的反例会被默默地忽略？

Answer 1

Alloy 基本上不支持递归。当遇到递归时，它展开代码最大次数。因此，如果它找不到解决方案，它只是，嗯，找不到解决方案。如果它只有在知道有潜在解决方案的情况下才能生成错误，这将解决最初的问题。

恕我直言，这是合金中最薄弱的地方之一。递归在几乎所有规范中都非常重要。