Catálogo de publicaciones - libros

In this chapter we describe how the concept of mathematical induction can be used in a practical way to prove program correctness. To complete an inductive proof the user needs to guide the theorem prover in KeY along the way. The knowledge about the fundamentals of induction that is required for this will be introduced. Since this chapter is written in tutorial style it is a good idea to work out the examples in the KeY prover in parallel to reading. It can also be read as a general introduction to induction in program verification.

Specification languages typically offer idealistic data types that are not available in programming languages. For example, the integer data types available in the specification languages UML/OCL, Z, B, and (which can also be seen as a specification language) are isomorphic to the mathematical integers ℤ having an infinite domain. On the other hand, the built-in integer types in and many other programming languages have finite domains. As a consequence the semantics of data types on specification and implementation level differ (at least on the boundaries of the domain).

In this section we clarify the quite subtle relation between integer data types in and . It turns out that the integers are not a of the type in but a so-called which constitutes a generalisation of refinement. Note, that the problems and solutions given in this section are not restricted to and . They analogously apply to other specification languages like e.g., UML/OCL, Z and B and to several programming languages like e.g., C and C++.

This section may also serve as a lightweight introduction to refinement and retrenchment (for a more detailed and systematic introduction we recommend [Derrick and Boiten, 2001] and [Banach and Poppleton, 1998], respectively). This section is based on material published in [Beckert and Schlager, 2004, 2005, Schlager, 2002].

Experience shows that the prevalent use case of program verification systems is not a single prover run. It is far more likely that a proof attempt fails, and that the program (and/or the specification) has to be revised. Then, after a small change, it is better to adapt and reuse the existing partial proof than to verify the program again from first principles. A particular advantage is that proof reuse can reduce the number of required user interactions.

Here we present such a technique for proof reuse. In fact, towards the end of this chapter ( Sect. 13.9), we will show how our method can improve the user experience for a whole range of verification scenarios. Until then, we limit ourselves to the setting described above, with the further assumption that only the implementation changes and the specification remains unchanged.

After discussing the features of the method, we will introduce a small running example, cover the theoretical and practical details of proof reuse, examine other solutions to the problem, and finally survey the full range of proof reuse applications in deductive verification of software.

So far in this book no specific examples have been discussed, apart from very simple transactions related examples in Chapter 9. In this chapter we are going to discuss how the KeY system is used to verify real world programs. The basis and running example for this chapter is the demonstrative electronic purse application provided by

The purpose of this chapter is not to present full specifications for and a thorough verification procedure, or give a tutorial on using the KeY system verification facilities ( Chap. 10). Rather, we will discuss general problems associated with verification attempts: provide advice on what to specify about applets, how to specify it using different specification languages, and give the reader hints necessary to perform efficient verification of his or her own applets. Verifications that we are going to discuss were performed on an absolutely unmodified source code of , thus, the context of this chapter is slightly different from the rest of the book—we do not consider the use of formal methods during the development process, instead we show how one can verify preexisting, legacy code, in other words, perform verification. We also assume that, to a certain extent, the reader is familiar with technology, described by Chen [2000] ( Chap. 9).

In the next section we present the application in more detail, in Section 14.3 we discuss different specification techniques and languages available in the KeY system, their advantages and disadvantages in the context of verification. Section 14.4 discusses modular verification and the use of method contracts in proofs, which is necessary to make the verification process scalable. Then in Section 14.5 different properties related to applets are presented, example specifications are given based on and verification is discussed. Finally, Section 14.6 summarises this chapter.

The Schorr-Waite graph marking algorithm named after its inventors Schorr and Waite [1967] has become an unofficial benchmark for the verification of programs dealing with linked data structures.

It has been originally designed with a LISP garbage collector as application field in mind and thus, its main characteristic is low additional memory consumption. The original design claimed only two markers per data object and, more important, only three auxiliary pointers at all during the algorithm’s runtime. It is the latter point, where most other graph marking algorithms lose against Schorr-Waite and need to allocate (often implicitly as part of the method stack) additional memory linear in the number of nodes in the worst case. These resources are used to log the taken path for later backtracking when a circle is detected or a sink reached.

Schorr and Waite’s trick is to keep track of the path by reversing traversed edges offset by one and restoring them afterwards in the backtracking phase of the algorithm. A detailed description including the implementation to be verified is given in Section 15.1.

Formal treatment of Schorr-Waite is challenging as reachability issues are involved. Transitive closure resp. reachability is beyond pure first-order logic and some extra effort has to be spent to deal with this kind of problems (see [Beckert and Trentelman, 2005] for a detailed discussion). On the other side, the algorithm is small and simple enough to serve as a testbed for different approaches. We introduce a notion of reachability as part of Sect. 15.2 and come back to it for the actual verification, which makes up most of Sect. 15.3.

This appendix lists syntax and semantics of all predefined function and predicate symbols of .

The KeY system accepts different kinds of inputs related to . From the user point of view these inputs can be divided into the following categories: From the system’s perspective the division is similar, but on top of this, the distinction between schematic mode and term (normal) mode is very important: Additionally, most of terms and formulae constructs can appear in both schematic and normal mode, but take slightly different form depending on the mode.