Abstract
How can we show that a program is correct (all its executions compute the expected result) or, at the very least, that it is safe (no execution produces a " crash " or a security flaw) ? We can reason directly about program semantics, but this is laborious. Program logics provide higher-level principles for reasoning about the properties of a program.
This deductive approach appeared as early as 1949 in a brief paper by Turing himself, and was rediscovered and generalized by Floyd in 1967, on programs of the " flowchart " type. But it was Hoare, in 1969, who introduced the concept of " program logic " and gave the basic rules of such logic for structured control languages.
In this fourth lecture, we have defined and then mechanized in Coq a Hoare logic for the IMP language. The mechanization makes clear the two ways of defining the " Hoare triplets " {P} c {Q} that are valid : axiomatically, by deduction rules, or semantically, in terms of program executions c. The equivalence between the two definitions demonstrates the correctness and completeness of Hoare's logic.
Hoare's logic extends quite easily to programs manipulating arrays, but with greater difficulty to programs with pointers manipulating chained data structures. Deep reflection on the notions of locality, aliases and resources led O'Hearn, Reynolds and Yang, between 1999 and 2001, to invent separation logic, with its notions of a memory footprint for each logical assertion and a separating conjunction between these assertions. Separation logic is highly effective for verifying unshared chained data structures. Its extension to shared-memory parallelism, concurrent separation logic, is the subject of much recent research.
