A contract language for modular specification and verification of temporal properties

Sammanfattning: Deductive software verification is used to prove correctness of programs with respect to contracts. Contracts are commonly expressed on procedures of a program using Hoare logic. Such contracts consist of a precondition, specifying a condition that must hold before the procedure is executed, and a postcondition which specifies what is guaranteed in return. A contract can be considered an agreement between the user of a procedure and its developer. It is important that the process of verifying that the procedures of a program satisfy their respective contracts is scalable. Scalability can be achieved by making sure verification is procedure-modular, which means that every procedure call can be replaced by the contract of the called procedure directly instead of being evaluated. The axioms of Hoare logic makes it a good basis for procedure-modular reasoning. But Hoare logic is not well-suited for reasoning about a procedure’s behaviour over a sequence of states. The stated questions are how a contract language for specifying such temporal properties can be designed, and how a procedure can be verified to satisfy contracts expressed in such a contract language in a procedure-modular way. To answer the question, a simple programming language with procedures is presented first. The intent is that contracts are expressed on programs written in this programming language. Two contract languages are presented. It is shown how contracts can be formulated in these languages to specify temporal properties of procedures, and how procedures can be verified to satisfy such temporal contracts. The first contract language is limited in terms of its expressivity, but its contracts can be automatically verified. The second language can be used to express more complex properties, but its verification problem turns out to be undecidable. Alternative approaches to its verification problem are discussed.