Operational Annotations: A new method for sequential program verification

TL;DR

This paper introduces a novel method for program verification that replaces traditional assertions with terminating programs to specify state sets, enabling a new operational approach to partial correctness in sequential programs.

Contribution

It proposes using terminating programs as state set specifications and introduces the operational triple [A] P [B] for program verification, offering a new perspective beyond Hoare logic.

Findings

Operational triples effectively specify partial correctness.

Replacing assertions with programs simplifies verification.

The method provides a new operational semantics for program correctness.

Abstract

I present a new method for specifying and verifying the partial correctness of sequential programs. The key observation is that, in Hoare logic, assertions are used as selectors of states, that is, an assertion specifies the set of program states that satisfy the assertion. Hence, the usual meaning of the partial correctness Hoare triple $\{f\}\{P\}\{g\}$: if execution is started in any of the states that satisfy assertion $f$, then, upon termination, the resulting state will be some state that satisfies assertion $g$. There are of course other ways to specify a set of states. I propose to replace assertions by terminating programs: a program $A$ specifies a set of states as follows: we start $A$ in any state whatsoever, and all the states that $A$ may terminate in constitute the specified set. I call this set the post-states of $A$. I introduce the operational triple $[A]\, P\, [B]$ to mean: if execution of $P$ is started in any post-state of $A$, then upon termination, the resulting state will be some post-state of $B$. Here, $A$ is the pre-program, and plays the role of a pre-condition, and $B$ is the post-program, and plays the role of a post-condition.