Languages and tools for the construction of verifiable programs

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

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.