JML中的“减少”是如何定义的？

Question

decreases之后的语句必须在每个循环中变得更小，并且始终是非零的。但它必须达到0吗？一定要一个一个变小吗？

Answer 1

正如JML文档中所述，减少(您也可以写减少)意味着带该说明符的int或长表达式“在执行循环时必须不少于0，并且每次循环必须减少至少一个(1)”。

因此，它可能达到或不可能达到0，但不能变小。而且，它必须至少变小，但不一定是一个。请注意文档中的示例，以获得更精确的解释。