我想在另一个方法的后置条件（和循环不变量）中调用一个类方法。我发现最相关的是StackOverflow 中的这篇文章。
我试图打开那里提供的链接（http://www.ibm.com/developerworks/java/library/j-jml/index.html）；但是，它不再起作用了。1-是否有任何（其他）资源可以找到“如何在其他函数的后置条件中调用类方法”？
2- 一旦我尝试在 OpenJML 中测试该示例，我收到静态验证错误：
只是我能够对这个例子使用运行时断言检查：
关于在静态验证（或运行时断言）中调用后置条件中的方法的任何帮助将不胜感激。谢谢
-- 我在 ubuntu 20.04 上使用 openjml 0.17.0-alpha-9。