JML规范的行业流行

Question

在我目前在大学学习的Java课程中，重点是在Javadoc注释中使用@require和@ensure子句等JML构造。我理解这是在实现契约设计范式，并且存在能够使用JML对软件进行数学验证的某些工具(假设这些子句是适当定义的)。

不过，我很好奇他们在工业界的普遍程度。这些条款是否实际使用？如果是的话，范围有多广？至少在我看来，防御性编程通常会使它们对于一些琐碎的方法来说是多余的(甚至是一些简单的事情，比如在代码中实现空守卫)。

Answer 1

契约式设计并不常见，因此这样的注释将是非常罕见的。这并不意味着他们根本就不会被使用！相反，契约式设计是最有用的，当正确性是最重要的，例如对于算法实现或安全关键系统。

但是绝大多数的软件开发并不被认为是安全的关键。您的需求更有可能是“作为业务分析师，我可以单击按钮将报表保存为Excel电子表格，以便执行自己的分析”。在这种情况下，正式核查没有任何价值，很难表达可以核查的有用合同。

当前的行业最佳实践是使用自动化测试用例来验证需求是否满足，以及系统的行为是否正确。测试有系统的局限性:测试只是例子，不能证明所有输入都是正确的，除非我测试所有输入。因此，测试和正式验证方法并不是相互替换的，而是相辅相成的:理想情况下，两者都是您所做的。

通常使用的唯一自动化形式验证系统是编程语言的静态类型系统。静态类型可以用来表示一些简单的契约，但是有一些明显的限制，这取决于语言。但是，即使是静态类型也不是普遍使用的:大量重要的开发(即使是对安全敏感的系统，比如web应用程序)都是在动态语言(如PHP、Python或Ruby )中进行的，这些语言通常缺乏任何内置的静态分析。