问题标签 [jml]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
formal-verification - 无法证明仅依赖于实现/内联的基本功能
我有这门课。当我使用 getBar() 的合同时，我可以证明 pass(int i) 方法，而不是没有它。除了 getBar() 的合约也被证明。为什么我不能通过内联证明通过？我尝试了 Key 2.8 和 Key 2.7。
filter - 查询以获取与 Jira 中带有某些标签的故事关联的所有子任务
例如，我在 Jira 中有一些标签为 A、B、C 的用户故事。但是在子任务级别没有标签。现在我需要获取该标签的所有用户故事、他们的任务和子任务的计数。
如何获得没有标签但链接到已标记用户故事的子任务。
java - OpenJML 后置条件（和循环不变量）包含类方法调用
我想在另一个方法的后置条件（和循环不变量）中调用一个类方法。我发现最相关的是StackOverflow 中的这篇文章。
我试图打开那里提供的链接（http://www.ibm.com/developerworks/java/library/j-jml/index.html）；但是，它不再起作用了。1-是否有任何（其他）资源可以找到“如何在其他函数的后置条件中调用类方法”？
2- 一旦我尝试在 OpenJML 中测试该示例，我收到静态验证错误：
只是我能够对这个例子使用运行时断言检查：
关于在静态验证（或运行时断言）中调用后置条件中的方法的任何帮助将不胜感激。谢谢
-- 我在 ubuntu 20.04 上使用 openjml 0.17.0-alpha-9。