我正在学习"合同设计"开发方法。然而，我很难看到它的优点。
例如，据说这种方法的一个特点是，函数的先决条件可以在其标头中表示。因此，我们可以有一个例子，其中我们将数字10除以任何前提条件是它必须大于0:的数字
get_result(value:INTEGER): REAL is
require
valid_value: value > 0
do
Result := 10 / value
ensure
Result = 10 / value
end
然而，与其他更传统的方式相比，它给我带来了什么好处？
get_result(value:INTEGER): REAL is
do
if value>0
Result := 10 / value
else
--throw an exception:
throw valid_value_exception
end
end
我所看到的是，在这两种方法之间唯一发生变化的是验证先决条件的网站。在第一种形式中，先决条件在函数的标头中进行验证，而在第二种形式中则在函数，但是在这两种情况下，您都必须继续进行验证。
我确信我错过了一些重要的事情。如果有人能帮我，我将不胜感激。
合同设计方法论的关键属性是，正确的程序在监视断言和不监视断言时的行为完全相同。换句话说，在正确的程序中，可以在不影响程序行为的情况下关闭断言监视。
在确保所有必需的测试都通过后(这是一种不合理的方法(，或者通过使用在编译时而不是运行时检查断言的验证工具来关闭断言监控(该示例是用Eiffel编写的，相应的验证工具是AutoProof；其他支持按合同设计的语言也有其他类似的工具(。
尽管参数应高于零的要求可以记录在功能描述中，但注释(通常(不可由编译器、代码分析器等编程语言工具使用，也不能用于程序验证、自动测试生成和其他自动化任务。
先决条件和后决条件也在责任分离中发挥作用。先决条件允许供应商依赖客户提供的担保。后置条件允许客户依赖供应商提供的担保。请注意，在这两种情况下，都不需要重复检查，也不需要捕获异常或检查结果。所有的知识都是在相关的断言中积累起来的。如果在方法主体内部进行检查，在实现部分，将不会粘合保证的内容、预期的结果等。
先决条件和后决条件的使用可以使调用链接起来。让我们考虑一个表达式
get_result ((get_result (n * n + 1).ceiling)
构造满足了第一个特征调用的前提条件。它的后置条件保证结果为正值。对ceiling的调用确保外部特性的参数满足其前提条件。因此，我们可以证明，如果不研究get_result的实现(前提是它是正确的(，表达式就不会抛出异常。事实上，有几种实现是可能的，但我们不在乎使用哪种实现。
总之，先决条件和后决条件
- 可以在运行时关闭以获得正确的程序
- 可由程序分析工具消耗
- 用于在编译时验证程序(并使此验证模块化(
- 客户和供应商之间的单独责任(谁犯了错误？(
- 消除了在客户端进行额外检查的需要，从而简化了功能调用链接