Abstract
The last lecture of the year studied program logics for functions, including higher-order functions and functions as first-class values. Recursive procedures are one of the earliest extensions of Hoare logic. The reasoning rules are both elegant in their treatment of recursion and complicated by numerous restrictions on the use and modification of variables.
A separation logic for a language with immutable variables and mutable memory bins not only allows a clearer formulation of the rules for first-order procedures and functions, but also an extension to the higher order. In this extension, Hoare triplets are part of the assertions of logic, and can therefore be used as preconditions of higher-order functions, to specify arguments of type "function", as well as in representation predicates, to specify the methods of an object while hiding its internal state. The semantic correction of the rule for recursive functions poses problems of circularity, which are resolved either by an extension of the step-counting technique, or by the use of modal logic including the ⊳ modality (read: "later").
New ways of presenting and using program logics are opening up in higher-order and type-dependent logics. The CFML system represents a functional, imperative program by its characteristic formula: a higher-order predicate that compositionally describes all the program's valid preconditions and postconditions. This representation is particularly well suited to interactive verification and the specification of higher-order functions. Using dependent types, Hoare and Dijkstra monads add preconditions and postconditions (Hoare monads) or a weaker precondition calculus (Dijkstra monads) to the usual monads. The F* language relies on a hierarchy of Dijkstra monads and a type generator that produces verification conditions to provide an excellent environment for functional and imperative verified programming.
