[Prev][Next][Index][Thread]
teaching Hoare logic
Date: Tue, 11 Oct 88 15:53:29 EDT
The fact that there is a sound and relatively complete axiom system for L4
(i.e. an Algol subset in which procedures cannot access global variables) is
very interesting, and worth mentioning in a course. It would be misleading to
give students the impression that Hoare logic simply does not work with higher
types. L4 is a rather powerful langauge with higher types. The results for L4
show that it is possible to use Hoare logic to reason about programs with
higher types and infinite range. Informally, infinite range means that a
higher type parameter can take on an infinite number of different meanings.
I interpret the results on L4 to show that the limitations of Hoare
logic are due to the way the store can be accessed in some languages
with higher types rather than the presence of higher types alone.
There is some discussion of the historical background of this area
in the introduction of my paper with Ed Clarke and Joe Halpern.
The full paper will appear in Information and Computation next year
(if anyone would like a preprint, please send me a message).
Steve