nach oben

2007 | Buch

Kapitel lesen Erstes Kapitel lesen

Verification of Object-Oriented Software. The KeY Approach

Foreword by K. Rustan M. Leino

herausgegeben von: Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

Long gone are the days when program veri?cation was a task carried out merely by hand with paper and pen. For one, we are increasingly interested in proving actual program artifacts, not just abstractions thereof or core algorithms. The programs we want to verify today are thus longer, including whole classes and modules. As we consider larger programs, the number of cases to be considered in a proof increases. The creative and insightful parts of a proof can easily be lost in scores of mundane cases. Another problem with paper-and-pen proofs is that the features of the programming languages we employ in these programs are plentiful, including object-oriented organizations of data, facilities for specifying di?erent c- trol ?ow for rare situations, constructs for iterating over the elements of a collection, and the grouping together of operations into atomic transactions. These language features were designed to facilitate simpler and more natural encodings of programs, and ideally they are accompanied by simpler proof rules. But the variety and increased number of these features make it harder to remember all that needs to be proved about their uses. As a third problem, we have come to expect a higher degree of rigor from our proofs. A proof carried out or replayed by a machine somehow gets more credibility than one that requires human intellect to understand.

Inhaltsverzeichnis

Frontmatter

A New Look at Formal Methods for Software Construction

Abstract

This chapter sets the stage. We take stock of formal methods for software construction and sketch a path along which formal methods can be brought into mainstream applications. In addition, we provide an overview of the material covered in this book, so that the reader may make optimal use of it.

Reiner Hähnle

Part I: Foundations

Frontmatter

First-Order Logic

Abstract

In this chapter, we introduce a first-order logic. This logic differs in some respects from what is introduced in most logic text books as classical first-order logic. The reason for the differences is that our logic has been designed in such a way that it is convenient for talking about Java programs. In particular our logic includes a type system with subtyping, a feature not found in most presentations of first-order logic.

Not only the logic itself, but also our presentation of it is different from what is found in a logic textbook: We concentrate on the definition of the language and its meaning, motivating most aspects from the intended application, namely the description of Java programs. We give many examples of the concepts introduced, to clarify what the definitions mean. In contrast to an ordinary logic text, we hardly state any theorems about the logic (with the notable exception of Section 2.6), and we prove none of them. The intention of this book is not to teach the reader how to reason about logics, but rather how to use one particular logic for a particular purpose.

The reader interested in the theoretical background of first-order logic in the context of automated deduction might want to read the book of Fitting [1996], or that of Goubault-Larrecq and Mackie [1997]. There are a number of textbooks covering first-order logic in general: by Ben-Ari [2003], Enderton [2000], Huth and Ryan [2004], Nerode and Shore [1979], or for the mathematically oriented reader Ebbinghaus et al. [1984]. To the best of our knowledge the only textbooks covering many-sorted logic, but not allowing subsorts, are those by Manzano [1996] and Gallier [1986]. For the technical details of the particular logic described in this chapter, see [Giese, 2005].

Martin Giese

Dynamic Logic

Abstract

In the previous chapter, we have introduced a variant of classical predicate logic that has a rich type system and a sequent calculus for that logic. This predicate logic can easily be used to describe and reason about data structures, the relations between objects, the values of variables—in short: about the states of (Java) programs.

Now, we extend the logic and the calculus such that we can describe and reason about the behaviour of programs, which requires to consider not just one but several program states. As a trivial example, consider the Java statement x++;. We want to be able to express that this statement, when started in a state where x is zero, terminates in a state where x is one.

Bernhard Beckert, Vladimir Klebanov, Steffen Schlager

Construction of Proofs

Abstract

The primary means of reasoning in a logic are calculi, collections of purely syntactic operations that allow us to determine whether a given formula is valid. Two such calculi are defined in Chap. 2 and 3 for first-order predicate logic and for dynamic logic (DL). Having such calculi at hand enables us in principle to create proofs of arbitrarily complex conjectures, using pen and paper, but it is obvious that we need computer support for all realistic applications. Such a mechanised proof assistant primarily helps us in two respects: 1. The assistant ensures that rules are applied correctly, e.g., that rules can only be applied if their side-conditions are not violated, and 2. the assistant can provide guidance for selecting the right rules. Whereas the first point is a necessity for making calculi and proofs meaningful, the second item covers a whole spectrum from simple analyses to determine which rules are applicable in a certain situation to the complete automation that is possible for many first-order problems.

Philipp Rümmer

Part II: Expressing and Formalising Requirements

Frontmatter

Formal Specification

Abstract

This chapter serves as an introduction to formal specifications. In Sect. 5.1 we reconsider in greater detail, but still on a fairly general level, the basic building blocks of formal specification—pre- and postconditions, invariants, and modifies clauses—that have already been informally introduced in Sect. 1.3. The next two sections then show how these notions can be formulated in two popular specification languages, OCL and JML. A short comparison between the two languages in Section 5.4 concludes this chapter.

Methodological questions like: How should operation contracts be inherited by subclasses? At which system states are invariants required to hold? How can modular specification and verification be effected? will be postponed till Chapter 8.

Andreas Roth, Peter H. Schmitt

Pattern-Driven Formal Specification

Abstract

There are few examples of innovations in software engineering that caught on as quickly and as pervasively as software design patterns [Gamma et al., 1995] did. Offering reusable solutions for recurring software design problems, software design patterns (from now simply called “patterns”) proved to be attractive not only for software designers and developers: as academic teachers we often observe that patterns belong to a small number of methods that are immediately perceived as useful by most students. The pedagogical advantages of patterns are at least as big as the productivity gain.

Richard Bubel, Reiner Hähnle

Natural Language Specifications

Abstract

This chapter describes how to use the KeY tool to bridge the gap between formal and informal specifications. Specifications need to be understood, maintained and authored by people with varying levels of familiarity with a formal specification language such as OCL. While a user of the KeY theorem prover should know a formal specification language, we cannot expect the same from a typical software developer, manager or customer. Hence there is need for specifications of different levels of formality, and we need to keep these different versions synchronised.

The KeY tool addresses these problems by making it possible to automatically translate formal (OCL) specifications to natural language (English and German), and by providing a multilingual editor in which specifications can be edited in OCL and natural language in parallel.

This chapter starts with an overview of the natural language features of KeY in Section 7.1. Sections 7.2 and 7.3 describe basic principles and components. The multilingual editor is described in Section 7.4. We outline how domain specific vocabulary is handled in Section 7.5, and conclude with pointers to further reading and a summary in Sections 7.6 and 7.7.

Kristofer Johannisson

Proof Obligations

Abstract

This chapter deals with the question how we can prove properties of specifications and of the relations between specifications and programs. The most important instance of such a property is the correctness of a program with respect to its specification.

In Chapter 5 we discussed specifications expressed with the languages UML/OCL and JML and their translations into the first-order fragment of Java Card DL. We now present our answers to the questions we left open there. What is the role we want class invariants to play? In which states should they hold and how do we prove this? What is the relation between postconditions and invariants?

We formulate a series of proof obligations templates. These contain parameters that can be instantiated with a specification or parts of a specification to yield proof obligations. These are finite sets of Java Card DL formulae that can be submitted to the KeY prover.

Andreas Roth

From Sequential Java to Java Card

Abstract

The Java Card dialect of Java is often thought of as a subset of Java. Java Card is used to program smart cards, and due to the limited nature of smart cards Java Card is a much simpler programming language than Java; currently, there is no concurrency in Java Card, floating point arithmetic, or dynamic class loading. Because of these simplifications, verification of smart card applications written in Java Card is substantially easier than verification of full-featured Java applications. However, there are some smart card specific features in Java Card that are not present in standard Java, namely object persistency and an atomic transaction mechanism. Another way to put it is that, technically, Java Card is not a subset of Java, it is a superset of a subset of Java. This chapter explains these Java Card specific features and describes extensions to the basic Java Card DL to handle them. In this chapter we assume that the reader is already familiar with basic Java Card DL presented in Chapter 3.

Wojciech Mostowski

Part III: Using the KeY System

Frontmatter

Using KeY

Abstract

This whole book is about the KeY approach and framework. This chapter now focuses on the KeY system, and that entirely from the user’s perspective. Naturally, the graphical user interface (GUI) will play an important role here. However, the chapter is not all about that. Via the GUI, the system and the user communicate, and interactively manipulate, several artefacts of the framework, like formulae of the used logic, proofs within the used calculus, elements of the used specification languages, among others. Therefore, these artefacts are (in parts) very important when using the system. Even if all of them have their own chapter/section in this book, they will appear here as well, in a somewhat superficial manner, with pointers given to in-depth discussions in other parts.

Wolfgang Ahrendt

Proving by Induction

Abstract

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.

Angela Wallenburg

Java Integers

Abstract

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 Java Card DL (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 Java 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 Java Card DL and Java. It turns out that the Java integers are not a refinement of the type integer in Java Card DL but a so-called retrenchment which constitutes a generalisation of refinement. Note, that the problems and solutions given in this section are not restricted to Java Card DL and Java. 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].

Steffen Schlager

Proof Reuse

Abstract

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 (\(\Rightarrow\) 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 Java software.

Vladimir Klebanov

Part IV: Case Studies

Frontmatter

The Demoney Case Study

Abstract

So far in this book no specific Java Card 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 Java Card programs. The basis and running example for this chapter is the demonstrative Java Card electronic purse application Demoney provided by

Trusted Logic S.A. The purpose of this chapter is not to present full specifications for Demoney and a thorough verification procedure, or give a tutorial on using the KeY system verification facilities (\(\Rightarrow\) Chap. 10). Rather, we will discuss general problems associated with Java Card verification attempts: provide advice on what to specify about Java Card applets, how to specify it using different specification languages, and give the reader hints necessary to perform efficient verification of his or her own Java Card applets. Verifications that we are going to discuss were performed on an absolutely unmodified source code of Demoney, 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 Java Card code, in other words, perform post-hoc verification. We also assume that, to a certain extent, the reader is familiar with Java Card technology, described by Chen [2000] (\(\Rightarrow\) Chap. 9).

In the next section we present the Demoney 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 Demoney 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 Java Card applets are presented, example specifications are given based on Demoney and verification is discussed. Finally, Section 14.6 summarises this chapter.

Wojciech Mostowski

The Schorr-Waite-Algorithm

Abstract

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 Java 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.

Richard Bubel

Appendices

Frontmatter

Predefined Operators in Java Card DL

Abstract

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

Steffen Schlager

The KeY Syntax

Abstract

The KeY system accepts different kinds of inputs related to Java Card DL. From the user point of view these inputs can be divided into the following categories:

system rule files,
user defined rule files,
user problem files/proofs with optional user defined rules,
Java Card DL terms and formulae required by the interaction component of the KeY system.

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:

in schematic mode schema variables can be defined and used (usually in definition of rules/taclets) and concrete terms or formulae are forbidden,
in normal mode schema variables and all other schematic constructs are forbidden, while concrete terms and formulae are allowed.

Additionally, most of terms and formulae constructs can appear in both schematic and normal mode, but take slightly different form depending on the mode.

Wojciech Mostowski

Backmatter

Titel: Verification of Object-Oriented Software. The KeY Approach
herausgegeben von: Bernhard Beckert
Reiner Hähnle
Peter H. Schmitt
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-540-69061-0
Print ISBN: 978-3-540-68977-5
DOI: https://doi.org/10.1007/978-3-540-69061-0