Humboldt-Universität zu Berlin - Mathematisch-Naturwissenschaftliche Fakultät - Institut für Informatik

Donnerstag, 15. Juli 2004, 15-17 Uhr
Haus 3, Raum 3.001 in der Rudower Chaussee 25

Das Institut für Informatik lädt zur Ringvorlesung ein:

Prof. Dr. W.-P. de Roever
Universität Kiel

Data Refinement: Model-oriented proof methods and their comparison

The subject of the talk is the comparison of methods for proving data refinement. By introducing abstraction relations, these methods can be reduced to proving semi-commutativity of four kinds of so-called simulation diagrams between an abstract data type operation and its corresponding concrete counterpart, namely, for forwards and backwards simulation, U-, and U-inverse simulation. In the talk we illustrate why forwards and backwards simulation considered separately are not complete as proof methods, and discuss why their combination is complete, indeed.

As such, these characterizations are formulated as inclusions between relations. However, many data-refinement proofs in the literature are based on assertional characterizations (e.g., those of Hehner, Hoare, Jones, Reynolds, the refinement calculi of Back and von Wright, and of Gardiner and Morgan, and many others). In this talk we prove how these relational characterizations of simulation can be reformulated within an assertional framework, both for partial correctness and total correctness semantics. The central mathematical tool used is that of various Galois connections.

Our main result is that the corresponding proof methods for data-refinement are either equivalent or not complete. This is worked out in our monograph on this subject mentioned below.

Galois connections are also used to relate the various styles of semantics to each other, more precisely, predicate-transformer-based semantics with relational semantics for both partial and total correctness.

Finally, if time permits, a sound and complete Hoare logic for a minimal language for specifying data types is discussed and related to the results mentioned above.

The talk is based on a book with the same title, written by the lecturer and Kai Engelhardt, and published by Cambridge University Press as Tract nr. 47 in their Cambridge Tracts in Theoretical Computer Science, 1998.

Adresse:
Humboldt-Universität zu Berlin
Institut für Informatik
Haus 3, Raum 001
Rudower Chaussee 25/Ecke Magnusstr.
12489 Berlin