Rigorous Modularity: formalizing and verifying software constructions

点击翻译按钮获取中文摘要

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.