Catálogo de publicaciones - libros

Compartir en
redes sociales


Verification of Object-Oriented Software. The KeY Approach: Foreword by K. Rustan M. Leino

Bernhard Beckert ; Reiner Hähnle ; Peter H. Schmitt (eds.)

Resumen/Descripción – provisto por la editorial

No disponible.

Palabras clave – provistas por la editorial

No disponibles.

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2007 SpringerLink

Información

Tipo de recurso:

libros

ISBN impreso

978-3-540-68977-5

ISBN electrónico

978-3-540-69061-0

Editor responsable

Springer Nature

País de edición

Reino Unido

Fecha de publicación

Información sobre derechos de publicación

© Springer-Verlag Berlin Heidelberg 2007

Tabla de contenidos

A New Look at Formal Methods for Software Construction

Reiner Hähnle

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.

- A New Look at Formal Methods for Software Construction | Pp. 1-18

First-Order Logic

Martin Giese

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

- Part I: Foundations | Pp. 21-68

Dynamic Logic

Bernhard Beckert; Vladimir Klebanov; Steffen Schlager

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.

- Part I: Foundations | Pp. 69-177

Construction of Proofs

Philipp Rümmer

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.

- Part I: Foundations | Pp. 179-242

Formal Specification

Andreas Roth; Peter H. Schmitt

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.

- Part II: Expressing and Formalising Requirements | Pp. 245-294

Pattern-Driven Formal Specification

Richard Bubel; Reiner Hähnle

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.

- Part II: Expressing and Formalising Requirements | Pp. 295-315

Natural Language Specifications

Kristofer Johannisson

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.

- Part II: Expressing and Formalising Requirements | Pp. 317-333

Proof Obligations

Andreas Roth

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.

- Part II: Expressing and Formalising Requirements | Pp. 335-374

From Sequential to

Wojciech Mostowski

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.

- Part II: Expressing and Formalising Requirements | Pp. 375-405

Using KeY

Wolfgang Ahrendt

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.

- Part III: Using the KeY System | Pp. 409-451