|
|
Logic & Semantics |
|
|
Logic & Semantics |
It is possible, using a corrected and generalised version of the work of Morris [1], to extend Hoare logic [2] to reason formally about programs in a Java-like language which use pointers and pointer aliasing. Two technical mechanisms have been developed to permit such reasoning: object component substitution and non-hiding assertions. Object-component substitution modifies formal substitution to permit the correct treatment of pointer aliases, without requiring explicit heap-as-array formulæ in assertions. Non-hiding assertions permit assertions to make use of auxiliary definitions, in particular including arbitrary inductive definitions of heap data structures.
Formal proofs of the correctness of significant algorithms exemplify the approach. To date proofs of in-place list-reversal and in-place list-merge have been completed and mechanically checked in Jape [3]. A proof of the Schorr-Waite algorithm [4] is in progress.
[1] J.M.Morris, A general axiom of assignment, Assignment and
linked data structure, A proof of the Schorr-Waite algorithm. In M
Broy and G. Schmidt (eds.) Theoretical Foundations of Programming
Methodology, 25-51, Reidel 1982 (Proceedings of the 1981
Marktoberdorf Summer School).
[2] C.A.R. Hoare: An axiomatic basis for computer programming,
Comm. ACM Vol 12, no 10, 1969, 576-580 and 583.
[3] R. Bornat and B.A.Sufrin: Animating formal proof at the
surface: the Jape proof calculator, The Computer Journal, 43, 3,
1999, 177-192.
[4] H. Schorr and W.M.Waite: An efficient machine-independent
procedure for garbage collection in various list structures, Comm.
ACM Vol 10, no 8, 1967, 501-506.
(There is also some very interesting work on new and dispose, using
object-component substitution, by Calcagno, Ishtiaq & O'Hearn; if
I've worked that up into a pragmatically useful tool I'll show an
example or two; if not I'll hint darkly at it).
Current versions of this work are available from my web page, http://www.dcs.qmw.ac.uk/~richard
