Rigorous Modularity: formalizing and verifying software constructions

严格的模块化：形式化和验证软件结构

• 批准号: 341829-2012
• 负责人: Dutchyn, Christopher
• 金额: $ 1.02万
• 依托单位: University of Saskatchewan
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2015
• 资助国家: 加拿大
• 起止时间: 2015-01-01 至 2016-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=572375
• 关键词: Rigorous; Modularity; formalizing; verifying; software

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.

软件开发正在经历另一种范式转变：认证编程。以前，对重要代码库的微小更改需要在部署前进行耗时且不可靠的测试。例如，修改航天飞机软件以使任务能够在元旦飞行估计需要数百万美元，因此没有实施。但是，类似的系统也被用于控制飞机、汽车和生命维持系统。