18 - Case study: Separation logic with first-class functions

Summary

In a conventional separation logic we have a “maps-to” operator a ↦ b saying that the heap contains (exactly) one cell at address a containing value b. This operator in the separation logic corresponds to the load and store operators of the operational semantics.

Now consider two more operators of an operational semantics: function call and function definition. When function names are static and global, we can simply have a global table relating functions to their specifications—where a specification gives the function's precondition and postcondition. But when the address of a function can be kept in a variable, we want local specifications of function-pointer variables, and ideally these local specifications should be as modular as the rest of our separation logic. For example, they should satisfy the frame rule. That is, we might like to write assertions such as (a ↦ b) * (f : {P}{Q}) meaning that a is a memory location containing value b, and a different address f is a function with precondition P and postcondition Q. Furthermore, the separation * guarantees that storing to a will not overwrite the body of f.

To illustrate these ideas in practice, we will consider a tiny programming language called Cont. The functions in this language take parameters f(x, y, z) but they do not return; thus, they are continuations.