Languages and tools for the construction of verifiable programs

随着我们越来越依赖软件，软件的可靠性越来越受到社会的关注。仅在美国，商务部在2002年估计，每年可避免的软件错误给经济造成的损失在200亿到600亿美元之间。超过一半的成本是由用户承担的。长期目标是为“正确的软件”的理想做出贡献。重点是使软件开发的设计阶段更加可靠。该项目的主旨是，只有通过整合多种技术来提高可靠性，才能取得进一步的突破性进展。我们考虑的技术包括面向对象编程、规范技术、并发性、异常处理、定理证明和文档技术。该方法是在编译器中集成一个自动定理证明器（一阶逻辑的决策过程），并允许程序包含规范。这允许编译器检查实现是否满足其规范。它还允许编译器检测可能发生错误（违反规范）的地方，并让程序员在这些情况下编写异常处理程序。基于动作的并发比基于线程的并发更容易表达和验证。另一方面，基于动作的并发很难有效地实现。集成决策过程允许优化，例如避免对动作保护的评估。因此，这种方法为程序员编写规范提供了多种好处：检查正确性、更好的异常处理和更高效的代码。

As we become more dependent on software, the reliability of software is of increasing concern to society. In the US alone, the Department of Commerce in 2002 estimated that the cost to the economy of avoidable software errors is between 20 and 60 billion dollars every year. Over half the cost is incurred by the users. The long-term goal is to contribute to the ideal of "correct software". The focus is on making the design phase of software development more reliable. The thesis of this project is that further groundbreaking progress can only be achieved by an integration of several techniques for improving reliability. The techniques that we consider are object-oriented programming, specification techniques, concurrency, exception handling, theorem proving, and documentation techniques. The approach is to integrate an automatic theorem prover (a decision procedure for first-order logic) in the compiler and allow programs to contain specifications. This allows the compiler to check if an implementation meets its specification. It also allows the compiler to detect where errors (specification violations) can occur and make the programmer write exception handlers in those cases. Action-based concurrency is easier to express and verify than thread-based concurrency. On the other hand, action-based concurrency is difficult to implement efficiently. The integrated decision procedure allows for optimizations, like avoiding evaluations of action guards. Thus, the approach gives programmers multiple benefits for writing specifications: checking the correctness, better exception handling, and more efficient code.