这篇文章是嵌入式软件系列:使用Ada契约强制编码
软件开发人员和他或她的编程语言之间的关系有时似乎遵循着浪漫/婚姻中常见的弧线:疯狂的迷恋、短暂的蜜月、不切实际的期望、现实和不兼容，然后分居或也许是没有激情的同居。关键问题是，下一步怎么办?是痛苦的离婚，寻找新伴侣，还是和解，重新燃起热情?
就Ada而言，由于ISO(国际标准化组织)最近批准了新的Ada 2012标准，后者的结果是明智的选择。有一段时间，人们普遍认为Ada是一种小众语言，正在被更有吸引力的竞争对手(如c++和Java)所取代。这种看法是相当扭曲的。在可靠性至关重要的行业中，Ada仍然被大量使用(尽管可能没有像早期那样大张旗鼓)。重要的是，语言并不是一成不变的;它正在经历一些重大的改进，以响应真实的用户需求，并考虑到软件和硬件领域的技术趋势。经过更新和振兴，Ada准备好了抓住当今软件开发人员的心和思想。
Ada 2012最令人兴奋的新增功能是基于合同的编程。这个概念很简单:像子程序这样的程序元素被设计来满足特定的软件需求(“契约”)，因此这些程序元素的语法应该支持指定这些需求。作为一个具体的例子，子程序的契约包括它的先决条件(子程序在进入时假定的属性)和它的后置条件(子程序在退出时保证的属性)。图1显示了一个与插入过程相关联的契约示例，该插入过程用于将元素添加到一个简单的队列中。契约可以由编译器或补充的分析工具进行静态检查，也可以通过运行时检查进行动态强制执行。
Queue: array (1..N) of Float;Last: Integer:= 0;——最后一个元素过程的索引插入(X: Float)， Pre =>最后在0 ..N-1, Post =>最后在1 ..N和队列(最后)= X;
基于契约的编程是一种日益重要的软件开发风格，特别是在可靠性、安全性和/或安全性至关重要的高完整性系统中。它易于进行静态分析，并有助于满足认证目标，如DO-178C航空电子设备软件安全标准[1]的正式方法补充。工具可以尝试证明子程序的后置条件是从其前置条件派生出来的，或者寻找反例。契约还可以用来表明程序不会有运行时错误。契约的概念并不新鲜，但是Ada现在是使用最广泛的语言，它将显式支持作为标准语法和语义的一部分(例如，相对于样式化的注释)。这意味着契约总是与程序同步，并且可以被任何符合语言标准的编译器处理。
将基于契约的编程与该语言现有的面向对象编程功能集成是一个挑战，特别是如何管理继承与前置和后置条件的交互。Ada 2012通过提供与Liskov替换原则[2]一致的语义来解决这个问题，该原则实际上确保了子类作为其超类的专门化。
除了基于合约的编程之外，Ada 2012还在实时调度、多处理器和多核支持以及预定义的库方面增加了主要的增强。语言版本还包括一系列小的改进，包括清理一些未完成的部分。
Ada设计一直关注于可靠性、可读性和错误的早期检测。Ada 2012意义重大，因为这些目标在当今软件密集和相互关联的世界中变得越来越重要。20年前在独立系统中造成不便的漏洞，现在可能会产生深远的影响，造成重大的经济损失，甚至可能造成生命损失。从某种意义上说，软件行业已经赶上了Ada。此外，Ada 2012的一些特性，比如基于合同的编程，使用起来很有趣。语言修订版认识到表示法的表现力和便利性很重要，因此Ada 2012提供了一种自然、简洁(但可读)的语法，包括量化和条件表达式。
简而言之，如果软件开发人员能以全新和彻底的眼光看待Ada 2012，可能会燃起新的火花。
更多信息请参阅嵌入式软件系列:使用Ada契约强制编码
参考文献
- RTCA / EUROCAE - 178 c / ED-12C。机载系统和设备认证中的软件考虑，2011年12月。
- B. Liskov和J. Wing。“子类型的行为概念”，《ACM编程语言和系统学报》(TOPLAS)，第16卷，第6期(1994年11月)，1811-1841页。
