Date: 2015-04-27
Categories: research

Why operational models?

Why give operational specifications and proofs? Why not prefer, say, a program logic?

Most of my work focuses on operational models of programs, and operational proofs about these models. It is much more common to develop program logics and perform proofs in the logic. There are some reasons to prefer operational models and proofs:

Clear specification: An operational model in terms of a state transition system gives a very clear specification of behaviour. In contrast, the behaviour of programs in a program logic are often given in a way that makes essential use of the syntax of the logic. This can obscure the behaviour.
Expressivity, lean startup: Operational proofs in theorem provers such as HOL and Coq allow you to take advantage of the powerful and flexible logic built into the theorem prover (the native logic), rather than constructing a program logic first. Program logics are restricted versions of these native logics. If you want to prove something about a particular system, why go indirectly, by constructing a program logic? Constructing a program logic and proving it sound takes time and effort.
- Against this, it may be the case that program logics identify common reasoning patterns that reduce the effort for many proofs. But theorem provers also allow such reasoning to be identified in the form of lemmas and tactics.
Program logics are typically ad-hoc. I have seen many more program logics than I have seen non-trivial programs verified using program logics. The reason is that each program logic is restricted in some way, and mostly tied to a small class of examples. When the next example comes along that doesn't fit the class, a new program logic has to be invented. The native logic of a theorem prover is not ad-hoc in the same way, and to the same extent.
Reuse: Operational models (particularly labelled transition systems) and proofs are more reusable than programs modelled and specified using program logics. The reason is that state transition systems represent a "lowest common denominator" language for specification. As such, two operational models and proofs can usually be combined relatively easily. Two programs, built in different programming languages, with proofs in different program logics, may be very hard to combine (you have to build a program logic that encompasses the existing logics, and this may be hard).
- Against this, when using a program logic, it may be clear what the theorems guarantee about the operational behaviour of the program. However, this is not always the case. Ideally (for me) top-level theorem statements in program logics should be clearly translated into equivalents about the operational behaviour.