Rigorous Modularity: formalizing and verifying software constructions

软件开发正在经历另一种范式转变：认证编程。以前，对重要代码库的微小更改需要在部署之前进行耗时且不可靠的测试。例如，更改航天飞机软件以使飞行任务能够在元旦期间飞行，估计耗资数百万美元，因此没有得到实施。但是，类似的系统正在被部署用于控制客机、汽车和生命维持系统。 在过去的五年中，INRIA的Coq等工具使软件开发人员能够实现长期寻求的认证软件目标。这些程序不仅通过检查输入空间中的各个点来进行验证，而且还通过数学精度进行了验证。证明程序的正确行为的定理用构造演算来证明，以合理的成本产生程序坚如磐石的有效性。最具说明性的例子是勒罗伊的CompCert编译器：在18个月的时间里，他和四名研究生开发了一个产品级的C编译器(与GCC相比，它产生的代码开销只有7%)，并证明了它的正确性。在犹他大学最近的一项研究中，CompCert显示没有错误。 我的研究就是采用这种新的方法，并将其与我对软件模块化的研究相结合。CoQ是一个强大的工具，但它仅限于纯函数式编程。我相信面向对象和面向方面的模块化在这个证明定理的软件环境中是有基础的。迈耶斯和其他人已经在埃菲尔的合同建设中向我们展示了这一点。他们的洞察力受到更有限的逻辑和更小的计算能力的限制，可以结合在一起给出逻辑上合理的模块化陈述。例如，每个抽象方法都需要伴随着关于其操作的形式化逻辑语句，并且任何具体实现都必须证明一个至少与逻辑语句一样强大的定理。每个类都必须包括私有方法和字段的封装未被违反的证明。类的每一次重新实现都必须满足相同的定理：尽管它可能具有关于空间和时间效率的更强的定理。

Software development is undergoing another paradigm shift: certified programming. Previously, small changes to significant code bases would require time-consuming and unreliable testing before deployment. For example, altering the space shuttle software to enable missions to fly over New Year's day was estimated at millions of dollars, and hence not implemented. But, similar systems are being deployed to control airliners, automobiles, and life-support systems. Over the last five years, tools such as Coq from INRIA have empowered software developers to achieve the long-sought goal of certified software. These are programs which are not just verified by checking at individual points in the input space, but which are certified with mathematical precision. Theorems certify the correct behaviour of the program are proven using the calculus of constructions, yielding rock-solid validity of the program at reasonable cost. The illustrative example is LeRoy's CompCert compiler: in 18 months, he and four graduate students produced a production-grade C-compiler (the code it produces has 7% overhead compared to gcc), and a proof of its correctness. In a recent study from the University of Utah, CompCert showed zero bugs. My research is to adopt this new approach, and combine it with my research on software modularity. Coq is a powerful tool, but it is limited to pure functional programming. I believe that object- and aspect-oriented modularity has a basis in this theorem-proving software environment. Meyers and others have already given us glimpses of this in the contracts construction in Eiffel. Their insights, hampered by more limited logic and constrained by less computational power, can be combined to give a logically-sound statement of modularity. For example, each abstract method needs to be accompanied by a formal logic statement about its action, and any concrete implementation must prove a theorem at least as strong as the logic statement. Every class must include a proof that encapsulation of private methods and fields is not violated. Every re-implementation of a class must satisfy the same theorems: although it may have stronger theorems about space and time efficiency.