Automatic verification of Eiffel programs
Julian Tschannen · Repository for Publications and Research Data (ETH Zurich) · 2009
Correctness of software systems can be proven by using static verification techniques. Static verifiers such as Spec# and ESC/Java have been developed for object-oriented languages. These verifiers have shown that static verification can be applied to object-oriented languages such as C# and Java. However, these verifiers are not easy to use, as they introduce many new concepts that programmers have to learn. To apply these verifiers to a real project, one has to modify existing code by adding contracts and annotations such as pure method marks or ownership information. Eiffel supports Design by Contract. Current libraries and programs are therefore already annotated with contracts. The goal of this thesis is to develop an automatic verifier for Eiffel which can prove existing code without the need of further annotations. The main features supported by the tool are agents and dynamic invocation. The tool, called EVE Proofs, translates Eiffel programs to Boogie and runs a fully automatic theorem prover to check correctness of the code. EVE Proofs is integrated in EVE, the Eiffel Verification Environment. This integration enables Eiffel programmers to use it directly from the programming environment. To reason about framing of routines, one needs modifies clauses. To prove existing Eiffel code, we implemented an automatic extraction of modifies clauses. Although the extraction of modifies clauses is limited, it enables us to prove examples with simple frame conditions. To show the feasibility of EVE Proofs, we present some examples which can be successfully verified. The examples include the command pattern to show the verification of agents and the strategy pattern to show the verification of dynamic invocation.