Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

Formalising Generalised Substitutions

Jeremy Dawson

Logic and Computation Program, NICTA ^{1}

Automated Reasoning Group, Australian National University, Canberra, ACT 0200, Australia

                 http://users.rsise.anu.edu.au/^{∼}jeremy/

September 3, 2007

1National ICT Australia is funded by the Australian Government’s Dept of Communications, Information Technology and the Arts and the Australian Research Council through Backing Australia’s Ability and the ICT Centre of Excellence program.

Outline

1 Introduction
2 The Operational Models

The General Correctness Operational Model The Total Correctness Operational Model Confirming the Models

3 The Monads used in these Models

Monads Compound Monads The General Correctness Compound Monad The Total Correctness Compound Monad Relating the General and Total Correctness monads

4 The Generalised Substitutions

Definition of Commands Repetition and Iteration

Outline

1 Introduction
2 The Operational Models

The General Correctness Operational Model The Total Correctness Operational Model Confirming the Models

3 The Monads used in these Models

Monads Compound Monads The General Correctness Compound Monad The Total Correctness Compound Monad Relating the General and Total Correctness monads

4 The Generalised Substitutions

Definition of Commands Repetition and Iteration

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

Introduction

Dunne developed a theory of the generalised substitutions used in the B method. He then proved properties of these generalised substitutions. Theory based on total correctness: contrast to abstract command language, based on general correctness Both underlying “models of computation” based on a monad Each of these is a compound monad

Outline

1 Introduction
2 The Operational Models

The General Correctness Operational Model The Total Correctness Operational Model Confirming the Models

3 The Monads used in these Models

Monads Compound Monads The General Correctness Compound Monad The Total Correctness Compound Monad Relating the General and Total Correctness monads

4 The Generalised Substitutions

Definition of Commands Repetition and Iteration

The General Correctness Operational Model

Want to distinguish computations which (on a given initial state) fail to terminate terminate in final state s non-deterministically, either of the above

Neither wlp / partial correctness nor wp / total correctness does this. General correctness refinement (Dunne):

A ⊑ B ≡ wp(A, Q) ⇒ wp(B, Q) ∧ wlp(A, Q) ⇒ wlp(B, Q)

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

The General Correctness Operational Model

Type of Computations

A computation (on given state) produces a set of outcomes An outcome is either

NonTerm, indicating non-termination, or Term s, indicating termination in the state s.

In Isabelle: datatype σ TorN = NonTerm | Term σ

For a non-deterministic computation (from given initial state), result is a set of outcomes. type outcome = TorN state type of computations is state → set TorN state

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

The Total Correctness Operational Model

Only interested in total correctness (weakest preconditions). Any computation which may fail to terminate fails every post-condition. Such computation is refinement-equivalent to a computation which does fail to terminate. Type of results is either

NonTerm, indicating possible non-termination, or Term S, indicating termination in a state s ∈ S.

type of result tcres (“total correctness result”) = TorN set state type of computations is state → TorN set state weakest precondition function (hence refinement):

[C] Q s = ∃S. (∀x ∈ S. Q x) ∧ C s = Term S

Confirming the Models

In each case, to confirm model is appropriate, we show two computations refinement-equivalent iff they are the same function (of type used in model) A ⊑_{tc} B ∧ B ⊑_{tc} A ⇒ A = B equivalently, [A] = [B] ⇒ A = B we define operations operationally, and prove these definitions correspond to Dunne’s definitions (which use weakest preconditions)

(Caveat: we ignore “frames”).

Outline

1 Introduction
2 The Operational Models

The General Correctness Operational Model The Total Correctness Operational Model Confirming the Models

3 The Monads used in these Models

Monads Compound Monads The General Correctness Compound Monad The Total Correctness Compound Monad Relating the General and Total Correctness monads

4 The Generalised Substitutions

Definition of Commands Repetition and Iteration

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

Monads

Long known in category theory Define unit and extension functions, satisfying rules

unit : α → Mα
ext : (α → Mβ) → (Mα → Mβ)
ext f ∘ unit = f
ext unit = id
ext (ext g ∘ f ) = ext g ∘ ext f

or functions unit, map and join (7 axioms for these) Can represent the structure of a computation (Moggi)

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

Monads — the Kleisli category

ext B models the action of B on result of previous computation Define B ⊙ A = ext B ∘ A : sequencing computations B and A. unit models the computation which does nothing (skip).

f ⊙ unit = f
unit ⊙ f = f
h ⊙ (g ⊙ f ) = (h ⊙ g) ⊙ f

These properties are as expected for sequencing and skip they give another category — the Kleisli category

Monads — Examples

The non-termination monad: a computation either terminates in a new state, or fails to terminate.

unit nt s = Term s

map nt f NonTerm = NonTerm map nt f (Term s) = Term (f s)

ext nt f NonTerm = NonTerm ext nt f (Term s) = f s

The set monad: models non-deterministic (but necessarily terminating) computations.

Monads — Examples

The non-termination monad: a computation either terminates in a new state, or fails to terminate.

unit nt s = Term s

map nt f NonTerm = NonTerm map nt f (Term s) = Term (f s)

ext nt f NonTerm = NonTerm ext nt f (Term s) = f s

The set monad: models non-deterministic (but necessarily terminating) computations.

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

Compound Monads

Let M and N, each with unit and extension functions, be monads. Then is MNα a monad? Need unit_{MN} : α → MNα and ext_{MN} ext_{MN} “extends” a function f from domain α to MNα. pext, “partial extension”, does part of this

ext_{MN} : (α → MNβ) → (MNα → MNβ)
pext : (α → MNβ) → (Nα → MNβ)

Definitions for a compound monad using pext

ext_{MN} g = ext_{M} (pext g)
unit_{MN} = unit_{M} ∘ unit_{N}

Also require that pext satisfies three rules

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

Compound Monads

Let M and N, each with unit and extension functions, be monads. Then is MNα a monad? Need unit_{MN} : α → MNα and ext_{MN} ext_{MN} “extends” a function f from domain α to MNα. pext, “partial extension”, does part of this

ext_{MN} : (α → MNβ) → (MNα → MNβ)
pext : (α → MNβ) → (Nα → MNβ)

Definitions for a compound monad using pext

ext_{MN} g = ext_{M} (pext g)
unit_{MN} = unit_{M} ∘ unit_{N}

Also require that pext satisfies three rules

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

The General Correctness Compound Monad

Want set TorN α is a monad; in fact, for any monad M, M TorN α is a monad

pext : (α → M TorN β) → (TorN α → M TorN β)

pext f (Term a) = f a

             pext f NonTerm = unit_{M} NonTerm

Proof of pext rules easy.

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

The Total Correctness Compound Monad

Recall tcres = TorN set state.

pext tc : (state → tcres) → set state → tcres

defined using prod tc : set tcres → tcres

                prod tc S = NonTerm  if NonTerm ∈ S

prod tc {Term s | s ∈ S} = Term (⋃ S)

Relating the General and Total Correctness monads

swap tc : set TorN σ → TorN set σ

                swap tc S = NonTerm  if NonTerm ∈ S

swap tc {Term s | s ∈ S} = Term S

swap tc is also a monad morphism from the general correctness monad to the total correctness monad.

unit tc a = swap tc (unit gc a)
ext tc (swap tc ∘ f ) (swap tc x) = swap tc (ext gc f x)

Since it is surjective, could use monad axioms for general correctness monad to prove axioms for total correctness monad.

For some other results also, easiest to prove for general correctness and use swap tc to “transfer” them to total correctness

Outline

1 Introduction
2 The Operational Models

The General Correctness Operational Model The Total Correctness Operational Model Confirming the Models

3 The Monads used in these Models

Monads Compound Monads The General Correctness Compound Monad The Total Correctness Compound Monad Relating the General and Total Correctness monads

4 The Generalised Substitutions

Definition of Commands Repetition and Iteration

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

Frames and Variables

Each substitution has a frame, loosely, the variables which “might” be affected. But frame(x := x) = {x}. Behaviour of command (alone) doesn’t determine frame. Mostly we ignore frames. For many generalised substitution operations (except assignment) consider abstract machine state, not variables

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

skip, sequencing, magic, abort

skip and sequencing given by unit and ⊙ of monad define magic and abort operationally;

magic tc def = "magic tc s == Term {}"
abort tc def = "abort tc s == NonTerm"

prove, as consequences, Dunne’s definitions

magic alt = "magic tc = guard tc (%s. False) unit tc"
abort alt = "abort tc = precon tc (%s. False) unit tc"

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

skip, sequencing, magic, abort

skip and sequencing given by unit and ⊙ of monad define magic and abort operationally;

magic tc def = "magic tc s == Term {}"
abort tc def = "abort tc s == NonTerm"

prove, as consequences, Dunne’s definitions

magic alt = "magic tc = guard tc (%s. False) unit tc"
abort alt = "abort tc = precon tc (%s. False) unit tc"

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

preconditioned command, guarded command

Again, we define them operationally;

"precon tc P C s = if P s then C s else NonTerm"
"guard tc P C s = if P s then C s else Term {}"

and prove, as consequences, Dunne’s definitions

"wp tc (precon tc P C) Q s = (P s & wp tc C Q s)"
"wp tc (guard tc P C) Q s = (P s --> wp tc C Q s)"

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

preconditioned command, guarded command

Again, we define them operationally;

"precon tc P C s = if P s then C s else NonTerm"
"guard tc P C s = if P s then C s else Term {}"

and prove, as consequences, Dunne’s definitions

"wp tc (precon tc P C) Q s = (P s & wp tc C Q s)"
"wp tc (guard tc P C) Q s = (P s --> wp tc C Q s)"

Definition of Commands — Choice

Defining by weakest precondition: conjunction of individual weakest preconditions.

General Correctness: choice gc C s = ⋃_{C∈C} C s.

Total Correctness: choice tc C can fail to terminate if any C ∈ C can fail to terminate.

choice tc C s = pext tc (λC. C s) C, expands to if {C s | C ∈ C} contains NonTerm then choice tc C s = NonTerm if {C s | C ∈ C} = {Term S_{C} | C ∈ C}, then choice tc C s = Term (⋃_{C∈C} S_{C})

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

Use of Coinductive Definitions

A^{0} = skip, A^{n+1} = A ; A^{n} A^{∧} is like choice of any A^{n}, also NonTerm if infinite repetition possible (an “infinite chain”) In [6] we defined an infinite chain by a function : ℕ → state (satisfying conditions) Better to use Isabelle’s coinductive definition facility, related proofs much easier

Use of Coinductive Definitions

infchs tc C: the set of states from which it is possible to execute C infinitely many times sequentially

coinductive "infchs tc C"
   intros "C s = Term S ==> ns : S ==>
                 ns : infchs tc C ==> s : infchs tc C"

reach NT C: the set of states from which NonTerm is reachable

inductive "reach NT C"
   intros "C s = NonTerm ==> s : reach NT C"
    "C s = Term S ==> ns : S ==>
                  ns : reach NT C ==> s : reach NT C"

Use of Coinductive Definitions

infchs tc C: the set of states from which it is possible to execute C infinitely many times sequentially

coinductive "infchs tc C"
   intros "C s = Term S ==> ns : S ==>
                 ns : infchs tc C ==> s : infchs tc C"

reach NT C: the set of states from which NonTerm is reachable

inductive "reach NT C"
   intros "C s = NonTerm ==> s : reach NT C"
    "C s = Term S ==> ns : S ==>
                  ns : reach NT C ==> s : reach NT C"

Use of Coinductive Definitions

icnt tc C: the states from which C s gives NonTerm

coinductive "icnt tc C"
   intros "C s = NonTerm ==> s : icnt tc C"
    "C s = Term S ==> ns : S ==>
                     ns : icnt tc C ==> s : icnt tc C"

(same intro rules as for reach NT which was an inductive definition)

We then prove that icnt tc C = reach NT C ∪ infchs tc C

Definitions of A^{∧}

Dunne defined A^{∧} as a least-fixed point

We use the operational definition for A^{∧} and then prove that A^{∧} is least fixpoint of λX . (A; X ) □ skip (where □ means choice)

rephat def = "rephat C state ==
          if state : icnt tc C then NonTerm
                          else Term (treach C state)"
fprep tc def = "fprep tc A X ==
                    X = choice tc seq tc A X, unit tc"
rephat isfp = "fprep tc A (rephat A)"
rephat is lfp = "fprep tc A Y ==> ref tc (rephat A) Y"

Introduction  The Operational Models  The Monads used in these Models  The Generalised Substitutions

Other results

Least upper bound of set of generalised substitutions Least upper bound of set of conjunctive predicate transformers Generalised substitutions correspond to predicate transformers satisfying a non-empty conjunctivity condition Discussion of results involving frames — how to express them Assorted further results from Dunne [8], see paper, also Appendix