Programming Language Semantics via Hoare Logic

Published on: 2021-07-21
Last Updated: 2021-07-21
Tags: Hoare Logic Agda Program Correctness Verification Formal Proof

Axiomatic Semantics via Hoare Logic

In 1967, as an alternative to \(\lAngle\) operational \(\rAngle\) semantics, Floyd produced his seminal paper ‘Assigning Meanings to Programs’ in which a program is given semantics via attachment of propositions to the connections in a flow chart with nodes as commands. In Floyd’s deductive system, whenever a command (a node) is reached via a connection whose associated proposition is true, then, if execution of the program leaves that node, it will leave through a connection whose associated proposition is also true.

“A semantic definition of a particular set of command [program] types, then, is a rule for constructing, for any command \(c\) of one of these types, a verification condition \(V_c(P;Q)\) on the antecedents and consequents of \(c\)”. - Floyd

The principle idea is that rather than define a program (however large or small) by the way it should be executed, a program can be defined by the antecedents upon the state space that must be true before execution — hereafter referred to as preconditions — and the associated consequents upon the state space that can be guaranteed to be true after execution — hereafter referred to as postconditions — thus freeing the semantics from concerns of the how in favour of the what.

These ‘antecedents/consequents upon the state space’ are first-order logic predicates or propositions and the state space is taken most generally to be a set of pairs of identifiers and values; again the formulation here shields us from implementation details such as whether these ‘identifiers’ identify memory addresses within a machine or Post-it Notes on a wall.

Later then, in 1969, Hoare built upon and expanded Floyd’s work1, applying the system to text ( \(\large{\lAngle}\normalsize{P}\large{\rAngle}% \normalsize{S}\large{\lAngle}\normalsize{Q}\large{\rAngle}\normalsize\) ) rather than to flow charts, creating a deductive system for reasoning about the correctness of programs ( \(\large{\llbracket}\normalsize{p}\large{\rrbracket}\,% \normalsize{S}\,\large{\llbracket}\normalsize{Q}\large{\rrbracket}\normalsize\) ) as we would more naturally recognise them. Central to Hoare’s system is the notion of a Hoare triple which is a reformulation of Floyd’s verification condition \(V_c(P;Q)\). A Hoare triple associates a precondition, or a state, before execution of a particular program with a resultant postcondition, or state, after execution.2

  1. Thus Hoare logic is sometimes referred to as Floyd-Hoare Logic↩︎

  2. NB Here, as in much of the literature, preconditions and postconditions and the actual subsets of the state space that they describe are used interchangeably. i.e. False = and True = \(S\) where \(S\) is the whole state space.↩︎