Catálogo de publicaciones - libros

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.

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 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 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 logics, but rather how to 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].

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 () 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 statement . We want to be able to express that this statement, when started in a state where is zero, terminates in a state where is one.

The primary means of reasoning in a logic are , 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 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.

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.

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

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.

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 . 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 . These contain parameters that can be instantiated with a specification or parts of a specification to yield . These are finite sets of formulae that can be submitted to the KeY prover.

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

This whole book is about the KeY and . This chapter now focuses on the KeY , 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.