本系列文章也在TechXchange：开发高品质软件
安全可靠的软件需要代码满足规范要求。这些通常是编写的文档，必须由程序员翻译成应用程序。不幸的是，规范和实现之间的契约可能很脆弱，甚至被忽略，这可能会导致问题。如果这些规范能够由编译器强制执行，那就太好了。
合同是Ada 2012中新增的一项技术，基于SPARK，它是Ada的一个可证明子集。程序员可以注释软件的各个方面，比如前置条件和后置条件。这允许编译器证明代码执行了开发人员指定的操作。这包括可能调用函数的代码，允许删除许多有效性检查，因为编译器确保参数满足指定的要求。
这些文章提供了基于契约的编程的例子和见解:
- Ada 2012:契约的喜悦
- 契约驱动的编程使规范超越了石器时代
- 使用契约来执行有效的编码
- Q&A:正式方法推动零缺陷软件
- Bug验证软件的安魂曲:测试和静态分析
- Bug验证软件的安魂曲，第2部分:通过SPARK 2014进行正式验证
Spark入门是另一个很好的资源。这是一个互动的网站，你可以在这里尝试合同。
