Abstract
The second lecture was devoted to the in-depth study of "Hoare logics", i.e. program logics that follow the approach introduced by C. A. R. Hoare in 1969. We defined such a program logic for the IMP language, a small imperative language with structured control that we had already studied in the 2019-2020 lecture "Mechanized Semantics". We then developed various extensions to this logic: derived or admissible reasoning rules, non-determinism, dynamic errors, unstructured control, etc.
The lecture continued with a study of the links between program logic and the operational semantics of the IMP language. We defined and demonstrated the semantic correctness of logic: all properties of a program derivable by the rules of logic are verified by all concrete executions of the program. Several demonstration techniques have been outlined: inductive, co-inductive andstep-indexing.
Completeness is the reciprocal property of semantic correctness: can any true property of all executions of a program be expressed as a Hoare triplet and derived by rules of logic? A complete logic would make it possible to solve the halting problem. Absolute completeness is therefore impossible for a Turing-complete language. On the other hand, Hoare logic satisfies a relative completeness property showing that it is as expressive as direct reasoning about program executions, given a fixed ambient logic.
Finally, we discussed the possibilities of automating deductive verification based on Hoare logic. Provided the loop invariants are supplied manually, a weaker precondition, or stronger postcondition, computation makes it possible to reduce the verification of a program in Hoare logic to the verification of a set of implications in first-order logic, a task that can be entrusted to automatic or assisted demonstrators.
