Formalizing General Correctness

Jeremy Dawson

Automated Reasoning Group and Dept. of Computer Science Australian National University

Canberra, Australia

jeremy@csl.anu.edu.au

Supported by an ARC Large Grant

Formalizing General Correctness

Based on Steve Dunne’s abstract commands, which is based on Jacobs & Gries semantics.

wp(A, P) – “weakest precondition”, condition on state that command A will terminate in new state satisfying P

trm (A) – “termination condition”, condition on state that command A will terminate

wlp(A, P) – “weakest liberal precondition”, condition on state that if command A terminates, it will do so in new state satisfying P

wp(A, P) s = trm (A) s ∧ wlp(A, P) s

Note: non-determinism is allowed, so

wlp(A, P) s ≠ trm (A) s → wp(A, P) s

Refinement - A refines B

Partial correctness : ∀Q s.wlp(A, Q) s → wlp(B, Q) s Total correctness : ∀Q s.wp(A, Q) s → wp(B, Q) s General correctness : both above are satisfied

Specifying abstract commands

(Dunne)

eg, sequencing “A; B”, ∧ lifted over state s

wlp(A; B, Q) = wlp(A, wlp(B, Q))

trm (A; B) = trm (A) ∧ wlp(A, trm (B))

Operational Semantics

datatype outcome = NonTerm | Term state
types
cmdMeaning = "state => outcome set"
expMeaning = "state => nat"
bexpMeaning = "state => bool"
consts
seq      :: "[cmdMeaning, cmdMeaning] =>
    cmdMeaning"
guard    :: "bexpMeaning => cmdMeaning =>
    cmdMeaning"

Monads

So when we model sequencing of two commands A and B, we first apply A to a given state, obtaining a set of outcomes, and we must then apply B, a function of type

state → outcome set

to the set of outcomes obtained from A. We can think of this as “extending” the function B to a function of type

outcome set → outcome set

When this can be done in a way that satisfies certain conditions, we call the relationship between the types a monad.

A Compound Monad

In fact, this is an example of a compound monad. The type outcome, relative to the type state, is a monad, where the extension function, of type

(state → outcome ) → (outcome → outcome )

would be given by

          exto f NonTerm = NonTerm

exto f (Term s) = fs

For any type α, the type α set (the type of sets of things of type α) is also a monad, where the extension function, of type

(α → α set ) → (α set → α set )

would be given by

exts f os = _{o∈os}^{⋃} f o

Its Extension Function

Here is the extension function for the compound monad, of type

(state → outcome set ) →

(outcome set → outcome set )

extos f os =

let f′ (Term s) = f s

    f′ NonTerm = units NonTerm

in exts f′ os extos f os =

let f′ (Term s) = f s

    f′ NonTerm = {NonTerm}

in ⋃_{o∈os} f′ o Then define sequencing of commands by

(A; B) s = extos B (A s)

Meaning of Commands

eg, Guarded command

The command P ⟶ A is the same as A if P holds, but is infeasible if P does not hold. Dunne’s definition: (→ lifted over s)

trm (P ⟶ A) = P → trm (A)

wlp(P ⟶ A, Q) = P → wlp(A, Q)

Our definition:

guard ?P ?A ?s == if ?P ?s then ?A ?s else {}

Using Isabelle, we prove, from our definitions, the wlp and termination conditions for commands (which Dunne uses to define these commands)

Meaning of Refinement

We proved characterizations of refinement

totcref A B = ∀s.B s ⊆ A s ∨ NonTerm : A s

partcref A B = ∀s.B s ⊆ {NonTerm} ∪ A s

gencref A B = ∀s.B s ⊆ A s

Note how that for general correctness is simpler than the other two. This explains some of the advantages of working with general correctness, as outlined by Dunne.

Issues

• Assignment rule

wlp(x := E, Q) = Q[x := E]

Substituting in Q means Q not just function state → bool but term of a defined language (eg the command language plus logical variables – Gordon).

• But to prove this rule from operational definition, can only prove it as equality of functions state → bool

• Paper addresses other tricky issues arising from Dunne’s formulation.

Free Iteration

repall A is the (unbounded) choice of any number of repetitions of A. The termination condition for repall A is that for every n, A^{n} terminates.

The free iteration of A is A^{∗}, where the outcomes of A^{∗} are those of repall, augmented by NonTerm in the case where it is feasible to execute A infinitely many times sequentially.

It is considerably easier to define this concept operationally than in terms of wlp and trm.

Dunne defines both trm (A^{∗}) and wlp(A^{∗}, Q) as fixpoints:

trm (A^{∗}) = νY.wp(A, Y)
wlp(A^{∗}, Q) = μY.wlp(A, Y) ∧ Q

and he also defines A^{∗} itself as a least fixpoint under the Egli-Milner refinement relation

A^{∗} ≡ μ_{em}X.(A; X)□skip