Dynamic Separation Logic and its Use in Education

Abstract

Mathematical logic is widely used in hardware and software verification. Hoare logic is particularly suitable for reasoning about imperative programs. Its extension, separation logic, introduces the sep- arating conjunction, which makes it possible to reason about programs working with pointers and mutable data structures. Dynamic logic, an example of modal logic, is yet another formalism used for verification. This article introduces propositional dynamic separation logic, which adds separating con- junction to dynamic logic. We describe syntax, semantics and Hilbert-style deductive system for propositional dynamic separa- tion logic and prove its soundness. The definition of the logic is rather abstract. Thus, the programming language consists of so-called regular programs rather than while-programs, and the set of atomic com- mands can be arbitrary as long as they correspond to local actions. Special attention is devoted to the soundness of the frame rule, which allows writing program specification using a small footprint, i.e., specifying exactly the portion of the heap that the program reads or writes. Programs that perform tests are also treated differently from regular dynamic logic. The article also argues for the use of separation logic in computer science curriculum. It is more intu- itive that other substructural logics and can be taught even in introductory logic courses. At the same time, it is an active research area with numerous verification tools built on its foundation. Therefore, it serves an excellent introduction to formal methods.