Rigorous Modularity: formalizing and verifying software constructions

软件开发正在经历另一个范式转变：认证编程。以前，对重要代码库的小更改需要在部署之前进行耗时且不可靠的测试。例如，修改航天飞机软件以使任务能够在元旦期间飞行，估计需要数百万美元，因此没有实施。但是，类似的系统正在被部署来控制飞机、汽车和生命支持系统。 在过去的五年中，INRIA的Coq等工具使软件开发人员能够实现长期追求的认证软件目标。这些程序不仅通过检查输入空间中的各个点来验证，而且通过数学精度来验证。定理证明的正确行为的程序证明使用微积分的建设，以合理的成本产生坚如磐石的程序的有效性。 LeRoy的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.