Mechanizing nondeterministic programming logics in higher-order logic

Gavan Tredoux

November 11, 1992

Contents

1 Introduction 3 1.1 Overview of the HOL system . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Program semantics in HOL . . . . . . . . . . . . . . . . . . . . . . . . . . 5

2 Nondeterminism and semantics 6

3 Execution Sequences 7 3.1 Overview of execution sequence semantics . . . . . . . . . . . . . . . . . . 7 3.2 Complete Partial Orders . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

3.2.1 Orderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.2.2 Well-founded sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

3.3 Lengths of sequences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.3.1 Type definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.3.2 A complete partial ordering . . . . . . . . . . . . . . . . . . . . . . 12 3.3.3 Arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

3.4 Execution sequences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.4.1 Type definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.4.2 A complete partial ordering . . . . . . . . . . . . . . . . . . . . . . 17 3.4.3 Arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

4 Commands 22 4.1 Partial Commands and recursion . . . . . . . . . . . . . . . . . . . . . . . 22 4.2 Predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 4.3 Semantics of commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 5 Programming Logics 27

5.1 Weakest Preconditions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 5.1.1 Predicate transformers . . . . . . . . . . . . . . . . . . . . . . . . . 27 5.1.2 Healthiness conditions . . . . . . . . . . . . . . . . . . . . . . . . . 28 5.1.3 Semantics of guarded commands . . . . . . . . . . . . . . . . . . . 28

5.2 Hoare Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 5.2.1 Partial correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 5.2.2 Total correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32

5.3 Invariant Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 5.4 Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

6 Conclusion and further work 40

Chapter 1

Introduction

This document describes the mechanization of some nondeterministic programming logics in higher-order logic. A program semantics based on execution sequences is described, together with its mechanization. The derivation of some standard programming logics establishes the reasonableness of the semantics. It is shown that the richness of the semantics permits reasoning about safety and liveness properties of programs, in particular possibly nonterminating programs.

1.1 Overview of the HOL system

HOL is a proof assistant and verifier, descended from the LCF family of theorem-provers [MGW79, Pau87], embedding a higher-order logic in a functional programming language, ML [Gor88]. The system guarantees adherence to the logic by isolating its axioms and primitive rules of inference in an abstract data type, thm. The strongly-typed nature of ML ensures that theorems (objects of type thm) can only be obtained from the axioms and primitive rules of inference. The embedding in ML also allows an arbitrary degree of mechanization, in the form of derived rules of inference and proof strategies, while still guaranteeing soundness. This is in contrast to non-inferential approaches to theorem-proving which typically deliver ‘theorems’ after complicated rewriting and resolution procedures without guaranteeing the soundness of those procedures [BM79]. To date, HOL has been used mostly for the specification and verification of hardware [ACG87], but the expressive power of higher-order logic captures, in principle, anything that is mathematically tractable [Cam90, Gor89, Mel].

The HOL logic is based on Church’s Simple Theory of Types [Chu40, And86], and is essentially Predicate Calculus enriched with typed lambda calculus. Variables may range over functions and predicates, and the arguments of functions and predicates may themselves be functions or predicates. Each term of the logic must be well-typed, having a type consistent with the types of its subterms. HOL has a number of built-in types, for example boolean values bool, natural numbers num, and strings string. There are also type constructors, which construct new types from existing types (for example, function spaces between types, and lists of elements of a type) and facilities for adding new types to the logic. A typed term will be denoted by t:σ, where t is the term and σ is its type. Most of the constructs of the predicate calculus are implemented straightforwardly in HOL, but some unusual features worth noting are:

• Predicates are functions with range bool. For example, using lambda notation, the function λ:num.n < 5 is a predicate on the natural numbers, mapping any natural number n to T (for true) or to F (for false), depending on whether n is less than 5 or not. A set of values of some type may be identified with its membership predicate on that type.

• Hilbert’s ε-operator plays an important role. If P is a predicate over values of type σ, then εx:σ.Px is an unspecified but fixed value of type σ, such that, if anything satisfies P then x satisfies P. If nothing satisfies P then x is left unspecified but fixed, of type σ. More formally, it is an axiom of the logic, that if ⊢ ∃x.Px then ⊢P(εx.Px) [Lei69, And86].

• There is notation for conditional statements. ‘If c then d else c’ is denoted by c ⇒ d | e.

• The type discipline is polymorphic, so that terms with variable types are allowed [Mil78].

Proof in HOL is by natural deduction; theorems are obtained by rules of inference from axioms and previously proved theorems, in the ‘forward’ direction. HOL also supports simulation of ‘backward’ goal-directed proof, through the use of Milner’s tactics [MGW79, Mil85], which automatically translate goal-directed ‘proofs’ into ‘forward’ proofs [Pau83].

The HOL logic can be extended by postulating new axioms, which runs the risk of introducing inconsistency into the logic, or by definition alone. Extension by definition is conservative in that it cannot introduce inconsistency [Mel89]. There are three mechanisms for making new definitions:

• Type definition. A new type can be introduced as a non-empty named subset of an existing type, by providing an isomorphism from the new type to that subset, together with a proof that the subset is non-empty. New type operators may also be defined, and there are facilities for automating the introduction of a restricted class of recursively defined types [Mel89].

• Constant definition. A new constant can be introduced as a non-recursive abbreviation for a term in the logic, which may not have a polymorphic type.

• Constant specification. If it can be proved that ⊢ ∃x.Px then a constant c can be introduced satisfying ⊢Pc. This allows partial specification, where the predicate P can be satisfied by more than one value because it fixes some but not all of the properties of the values; precisely which value the constant is, of those satisfying the predicate, is left unspecified. For example a total function can be introduced by specifying its behaviour on a proper subset of its domain only, leaving it unspecified elsewhere.

The extensive use of definitions entails that proofs rely heavily on rewriting routines; these are implemented as derived rules of inference in ML functions, preserving soundness. ML is itself a higher-order functional language (functions may take functions as arguments) so that rewriting routines may be soundly tailored by the user to specific situations, in arbitrarily complex ways. The soundness of user extensions to inference mechanisms poses a difficult problem for most theorem-provers not in the LCF fold [BM81].

Extensions to the HOL logic are organized hierarchically in theories; named collections of types, type operators, constants, definitions, axioms and theorems. A library of commonly used theories is built-in, for example theories concerning sets, the natural numbers and finite-length lists. The expressive power of the logic, due to its higher-order variables and type polymorphism, allows the formulation and proof of very general definitions and lemmas, which can be reused in many different contexts. The extent to which this simplifies mechanization will become apparent below.

1.2 Program semantics in HOL

An overview of previous mechanizations of program semantics in HOL, in particular [Gor89, BvW90, Age92].

Nondeterminism and semantics

Denotational semantics popularized in the 1970s by Scott and Strachey, dealt only with deterministic programs. Dijkstra focused attention on nondeterminism in [Dij76], although this had been considered before, for example in [Flo67]

The term ‘nondeterminism’ has been used variously, with different meanings. This chapter surveys approaches in the literature to the problem of nondeterminism in programs - in particular, Plotkin and Apt’s use of powerdomains [Plo79, AP86].

Execution Sequences

This chapter provides an overview of execution sequences and describes their representation in HOL.

3.1 Overview of execution sequence semantics

Execution sequences have been used before in program semantics; by Blikle [Bli87], in Temporal Logic [Pnu81, MP83], and by Brink and Rewitzky in their model of Dijkstra’s algebra of weakest preconditions [Dij76, BR91, Rew91]. The formulation used here differs from these in several aspects, to be explained below.

The semantics is based on an abstract machine state, on which computation acts. This would typically be the vector of values of all program variables. Certain computations can be considered atomic, causing a transition between program states. Atomic computations can be thought of as two-element sequences of states, where the first state in the sequence is transformed into the second by the computation. So if an atomic computation A transforms state s_{1} into state s_{2} then it can be identified with the sequence < s_{1}, s_{2} >. This in contrast to the relational model where all computations are represented by two-element sequences, as in [Gor89, Mad92, MC80].

Composition of atomic computations extends these sequences into ones containing multiple states. Suppose the atomic computation A_{1} is the sequence < s_{1}, s_{2} >, and A_{2} is < s_{2}, s_{3} >, then the composition ‘A_{1} followed by A_{2}’ can be identified with the threeelement sequence < s_{1}, s_{2}, s_{3} >. Finite computations are in general modelled as finite compositions of atomic computations, and identified with finite sequences of states. An infinite, non-terminating computation can be modelled by an infinite sequence of states, as an infinite composition of atomic computations.

This simple distinction between terminating and non-terminating computations is employed widely in formal treatments of program semantics, as in [Dij76, Gri81, Nel89, DS90].

An additional distinction has been made between finite, properly terminated computations, and finite but improperly terminated, computations [Apt84, BR91, Pnu81]. The latter have also been referred to as aborted computations where abortion is distinguished from nontermination. The semantics employed here embraces this further disctinction, which entails that there are three sorts of execution sequences, which will be referred to as terminated, aborted and infinite. In the discussion that follows a terminated sequence will be denoted by < s_{1}, s_{2}, …, s_{n} >, an aborted sequence by < s_{1}, s_{2}, …, s_{n}), and an infinite sequence by < s_{1}, s_{2}, …, s_{n}, …). Denote an arbitrary sequence by < s_{1}, s_{2}, …, s_{n}, … >, which may be terminated, or aborted, or infinite.

In this model of computation, all computation is effective, in the sense that it always does something. This means that any sequence representing a computation contains at least two states, there are no ‘null’ computations that do nothing – unlike [BR91], where null computations are allowed and are identified with one-element sequences. Moreover, intermediate states of computations are significant, in contrast to the relational model referred to above.

In general, two computations can be composed by ‘pasting’ together their execution sequences, assuming that the first computation terminates in a state from which the second may proceed. Suppose a computation C_{1} has the sequence < s_{1}, s_{2}, …, s_{n} > and C_{2} has the sequence < t_{1}, t_{2}, …, t_{n}, … >, where s_{n} = t_{1}. Then the composed computation is < s_{1}, s_{2}, …, s_{n}, t_{2}, …, t_{n}, … >. The composition will be aborted if C_{2} is aborted, terminated if C_{2} terminates, and infinite if C_{2} is infinite; the composition is the same sort of sequence as C_{2}. Note that computations cannot be composed if the first does not terminate, or if the first terminates in a state that the second does not proceed from.

The following fundamental operations on execution sequences are naturally defined, as are many other operations, and will feature strongly in the discussion below:

• first returns the first state of any sequence, so that first < s_{1}, s_{2}, …, s_{n}, … > = s_{1}.

• last returns the last element of any finite sequence, terminated or aborted, so that last < s_{1}, s_{2}, …, s_{n} > = s_{n}, and last < s_{1}, s_{2}, …, s_{n}) = s_{n}.

• join composes a terminated sequence with any sequence proceeding from its final state, so that as above < s_{1}, s_{2}, …, s_{n} > join < t_{1}, t_{2}, …, t_{n}, … > = < s_{1}, s_{2}, …, s_{n}, t_{2}, …, t_{n}, … >, assuming that t_{1} = s_{n}.

A program can now be treated as a ‘bundle’ of computations, and identified with the set of execution sequences which represent those computations. Each sequence contained by the program is a possible computation under its control, proceeding from the first state of the sequence. There are two immediate consequences of this definition

• Unbounded nondeterminism. Where a program contains more than one sequence proceeding from some state, then it is not determined which computation would be ‘chosen’ in any ‘invocation’ of the program; all such computations are equally possible. As no restriction has been placed on the sets representing programs, this nondeterminism can be unbounded, allowing an arbitrary number of sequences proceeding from the same state. A program is deterministic if it contains at most one sequence proceeding from any state.

• Partial programs. Programs need not have at least one sequence proceeding from each state, some states may have no sequence, in the program, proceeding from them. In that case the program is undefined at such states, and is said to be partial. A program is total if it has at least one sequence proceeding from each state. [Nel89, Mor88, Bac92].

Programs can be specified by stating which execution sequences they contain. For example the program skip can be defined as the set {< s, s >| s ϵ S} where S is the set of all machine states. So skip is precisely the set of all two-element sequences of states, where the first state is identical to the second and last, indicating that skip leaves the machine state unchanged. Note that skip is deterministic and total, in the senses explained above.

Programs may also be combined set-theoretically. For example, set union can be used to model non-deterministic choice between programs, combining the sequences of both in the same program. If this combination results in, say, two possible sequences proceeding from the same state, one from each program, then the sequence chosen will, as explained above, not be determined.

Composition of programs is naturally modelled using composition of sequences. If P and Q are programs, then define P ; Q = {e | e ϵ P and e does not terminate} ∪ {e_{1} join e_{2} | e_{1} ϵ P, e_{2} ϵ Q and the join is defined}. So the composition of P with Q contains all those sequences in P which do not terminate, together with all possible compositions of some sequence in P and some in Q.

An important operation on programs, which motivates many details of the semantics, is recursion. Recursion on a program may be thought of as an infinite composition of the program with itself, and modelled by an extension of transitive closure on relations, under composition of relations, to a transitive closure of execution sequences, under the join operation. For any program P, identify the recursion of P, recP, with the set containing all ‘non-extendable joins’, which are:^{1}

• All possible infinite joins e_{1} join e_{2} join e_{3} … where for each i, e_{i} ϵ P.

• All possible finite joins e_{1} join e_{2} join e_{3} … join e_{n} where for each i ≤ n, e_{i} ϵ P, and there is no e ϵ P such that e_{n} join e is defined.

1The notation glosses over the associativity of join so that brackets may be omitted – this is formally derived later

An infinite join of sequences can be defined as the least upper bound of the set {e_{1}, e_{1} join e_{2}, e_{1} join e_{2} join e_{3}, …} with respect to the extension ordering on execution sequences. Say that e_{2} is an extension of e_{1} if e_{1} = e_{2} or there is some e_{3} such that e_{1} join e_{3} = e_{2}, and order e_{1} ‘below’ e_{2}. This ordering plays a key role in the semantics.

The semantics outlined above suggests strongly that an execution sequence can be completely characterized by its elements and length. Moreover the sort of an sequence is most naturally interpreted as a statement about its length. Here a terminated sequence is associated with a finite ‘whole’ length, an infinite sequence with an ‘infinite’ length, and an aborted sequence with a finite but ‘fragmented’ length – embodying the idea that an aborted sequence is in a sense incomplete. This characterization requires a theory of lengths, and as will be demonstrated, an ordering on these lengths which leads naturally to the extension ordering on sequences.

3.2 Complete Partial Orders

Some essential definitions of partial orders, chains, and least upper bounds. These definitions are used throughout, to order lengths of sequences, the sequences themselves, and to construct least upper bounds of chains of lengths, and chains of sequences.

3.2.1 Orderings

refl
    |- !r. refl r = (!d. r d d)
antisym
    |- !r.
       antisym r =
       (!d1 d2. r d1 d2 /\ r d2 d1 ==> (d1 = d2))
trans
    |- !r.
       trans r =
       (!d1 d2 d3. r d1 d2 /\ r d2 d3 ==> r d1 d3)
partial_order
    |- !r. partial_order r = refl r /\ antisym r /\ trans r
chain
    |- !Ch r. chain r Ch = (!i. r(Ch i)(Ch(i + 1)))
chain_comp
    |- !Ch r.
        partial_order r ==>
        (chain r Ch = (!n m. r(Ch n)(Ch(n + m))))
chain_less_eq

|- !C r.
partial_order r ==>
(chain r C = (!n m. n <= m ==> r(C n)(C m)))
chain_total
|- !C r.
partial_order r ==>
chain r C ==>
(!m n. r(C m)(C n) \/ r(C n)(C m))
is_ub
|- !d C r. is_ub r d C = (!n. r(C n)d)
is_lub
|- !d C r.
is_lub r d C =
is_ub r d C /\ (!k. is_ub r k C ==> r d k)
lub
|- !C r. lub r C = (@d. is_lub r d C)
stunt_chain
|- !C r.
stunt_chain r C =
chain r C /\ (?n. is_ub r(C n)C)
cpo
|- !r.
cpo r =
partial_order r /\
(!C. chain r C ==> is_lub r(lub r C)C)
lub_unique
|- !C r a b.
partial_order r ==>
is_lub r a C ==>
is_lub r b C ==> (a = b)
stunt_chain_lub
|- !C r. stunt_chain r C ==> (?n. is_lub r(C n)C)

3.2.2 Well-founded sets

dec_chain
|- !C W R.
dec_chain C W R =
(!n. W(C n)) /\ (!n. R(C(SUC n))(C n))
wfp
|- !W R. wfp W R = ~(?C. dec_chain C W R)

3.3 Lengths of sequences

A theory of lengths is needed to allow a uniform representation of sequences. Lengths form a complete partial order, and enjoy addition and subtraction.

3.3.1 Type definition

let lnum = define_type `lnum`
`lnum = WHOLE num | FRAG num | OO`;;
lnum
    |- !f0 f1 e.
        ?! fn.
         (!n. fn(WHOLE n) = f0 n) /\
         (!n. fn(FRAG n) = f1 n) /\
         (fn OO = e)
is_WHOLE
    |- (!n. is_WHOLE(WHOLE n) = T) /\
       (!n. is_WHOLE(FRAG n) = F) /\
       (is_WHOLE OO = F)
is_OO
    |- (!n. is_OO(WHOLE n) = F) /\
       (!n. is_OO(FRAG n) = F) /\
       (is_OO OO = T)
is_FRAG
    |- (!n. is_FRAG(WHOLE n) = F) /\
       (!n. is_FRAG(FRAG n) = T) /\
       (is_FRAG OO = F)
WHOLE_dest
    |- !n. WHOLE_dest(WHOLE n) = n
FRAG_dest
    |- !n. FRAG_dest(FRAG n) = n

3.3.2 A complete partial ordering

lnum_less_eq
    |- !l m.
        l <-+ m =
        is_WHOLE l /\ is_WHOLE m /\
        (WHOLE_dest l) <= (WHOLE_dest m) \/
        is_WHOLE l /\ is_FRAG m /\

(WHOLE_dest l) < (FRAG_dest m) \/
is_WHOLE l /\ is_OO m \/
(l = m)
lnum_less
|- !l m. l <+ m = l <-+ m /\ ~(l = m)
lnum_less_trans
|- trans $<+
lnum_less_eq_partial_order
|- partial_order $<-+
lnum_cpo
|- cpo $<-+

3.3.3 Arithmetic

WHOLE_plus
|- (!n m. m WHOLE_plus (WHOLE n) = WHOLE(m + n)) /\
(!n m. m WHOLE_plus (FRAG n) = FRAG(m + n)) /\
(!n m. m WHOLE_plus OO = OO)
FRAG_plus
|- (!n m. m FRAG_plus (WHOLE n) = FRAG(m + n)) /\
(!n m. m FRAG_plus (FRAG n) = FRAG(m + n)) /\
(!n m. m FRAG_plus OO = OO)
OO_plus
|- (!n. OO_plus(WHOLE n) = OO) /\
(!n. OO_plus(FRAG n) = OO) /\
(OO_plus OO = OO)
lnum_plus_parts
|- (!m l n. (WHOLE m) ++ l = m WHOLE_plus l) /\
(!l m. (FRAG m) ++ l = m FRAG_plus l) /\
(!l m. OO ++ l = OO_plus l)
lnum_plus
|- !m n.
((WHOLE m) ++ (WHOLE n) = WHOLE(m + n)) /\
((WHOLE m) ++ (FRAG n) = FRAG(m + n)) /\
((WHOLE m) ++ OO = OO) /\
((FRAG m) ++ (FRAG n) = FRAG(m + n)) /\
((FRAG m) ++ (WHOLE n) = FRAG(m + n)) /\
((FRAG m) ++ OO = OO) /\
(OO ++ (WHOLE n) = OO) /\
(OO ++ (FRAG n) = OO) /\
(OO ++ OO = OO)
lnum_plus_id

|- !l. (l ++ (WHOLE 0) = l) /\ ((WHOLE 0) ++ l = l)
lnum_plus_com
|- !l1 l2. (l1 ++ l2 = l2 ++ l1)
lnum_plus_assoc1
|- !l1 l2 l3. (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)
lnum_plus_mono
|- !l l1 l2.
    is_WHOLE l ==>
    l1 <-+ l2 ==>
    (l1 ++ l) <-+ (l2 ++ l)
lnum_strict_plus_mono
|- !l l1 l2.
    is_WHOLE l ==>
    l1 <+ l2 ==>
    (l1 ++ l) <+ (l2 ++ l)
WHOLE_sub
|- !n m. m WHOLE_sub (WHOLE n) = WHOLE(m - n)
FRAG_sub
|- !n m. m FRAG_sub (WHOLE n) = FRAG(m - n)
OO_sub
|- !n. OO_sub(WHOLE n) = OO
lnum_sub_parts
|- (!m l n. (WHOLE m) -- l = m WHOLE_sub l) /\
   (!l m. (FRAG m) -- l = m FRAG_sub l) /\
   (!l m. OO -- l = OO_sub l)
lnum_sub
|- !m n.
    ((WHOLE m) -- (WHOLE n) = WHOLE(m - n)) /\
    ((FRAG m) -- (WHOLE n) = FRAG(m - n)) /\
    (OO -- (WHOLE m) = OO)
PR
|- (!n. PR(WHOLE n) = WHOLE(n - 1)) /\
   (!n. PR(FRAG n) = FRAG(n - 1)) /\
   (PR OO = OO)
SC
|- (!n. SC(WHOLE n) = WHOLE(n + 1)) /\
   (!n. SC(FRAG n) = FRAG(n + 1)) /\
   (SC OO = OO)
lnum_PR_mono
|- !l1 l2.
    (WHOLE 1) <-+ l1 ==>
    l1 <-+ l2 ==>
    (PR l1) <-+ (PR l2)

lnum_PR_mono_strict_alt
    |- !l1 l2.
        (WHOLE 0) <+ l1 ==>
        ((PR l1) <+ (PR l2) = l1 <+ l2)

3.4 Execution sequences

Execution sequences are implemented as pairs, a function to return the elements together with the length of the sequence. They form a complete partial order, and enjoy composition and subtraction. Composition is associative and continuous.

3.4.1 Type definition

IS_exseq_REP
    |- !r.
        IS_exseq_REP r =
        (?f l.
          (r = (\m. ((WHOLE m) <+ l => f m | (@x. T))),l) /\
          (WHOLE 1) <+ l)
exseq_TY_DEF
    |- ?rep. TYPE_DEFINITION IS_exseq_REP rep
exseq_ISO_DEF
    |- (!a. ABS_exseq(REP_exseq a) = a) /\
       (!r. IS_exseq_REP r = (REP_exseq(ABS_exseq r) = r))
exseq_fn_dest
    |- !e. exseq_fn_dest e = FST(REP_exseq e)
length
    |- !e. length e = SND(REP_exseq e)
length_min
    |- !e. (WHOLE 1) <+ (length e)
TERM
    |- !e. TERM e = is_WHOLE(length e)
ABORT
    |- !e. ABORT e = is_FRAG(length e)
INF
    |- !e. INF e = is_OO(length e)
elt
    |- (!n e. elt(WHOLE n)e = exseq_fn_dest e n) /\
       (!n e. elt(FRAG n)e = exseq_fn_dest e n)
last

    |- !e. last e = elt(PR(length e))e
first
    |- !e. first e = elt(WHOLE 0)e
mk_exseq_rp
    |- !f l.
        mk_exseq_rp(f,l) =
(\n. ((WHOLE n) <+ l => f n | (@y. T))),l
mk_exseq
|- !f l. mk_exseq(f,l) = ABS_exseq(mk_exseq_rp(f,l))
mk_exseq_REP
    |- !f l.
        (WHOLE 1) <+ l ==>
        IS_exseq_REP(mk_exseq_rp(f,l))
mk_exseq_thm
    |- !f l.
        (WHOLE 1) <+ l ==>
        (length(mk_exseq(f,l)) = l) /\
        (!n.
          elt(WHOLE n)(mk_exseq(f,l)) =
          ((WHOLE n) <+ l => f n | (@x. T)))
exseq_eq
    |- !x y.
        (length x = length y) /\
        (!n.
          (WHOLE n) <+ (length x) ==>
          (elt(WHOLE n)x = elt(WHOLE n)y)) =
        (x = y)
pair
   |- !x y.
       (length(pair(x,y)) = WHOLE 2) /\
       (!n.
         elt(WHOLE n)(pair(x,y)) =
         ((WHOLE n) <+ (WHOLE 2) => ((n = 0) => x | y) | (@x'. T)))
pair_TERM
    |- !x y. TERM(pair(x,y))
pair_first
    |- !x y. first(pair(x,y)) = x
pair_last
    |- !x y. last(pair(x,y)) = y
abort_pair
|- !x y.
    (length(abort_pair(x,y)) = FRAG 2) /\
    (!n.

      elt(WHOLE n)(abort_pair(x,y)) =
      ((WHOLE n) <+ (FRAG 2) => ((n = 0) => x | y) | (@x'. T)))
abort_pair_ABORT
    |- !x y. ABORT(abort_pair(x,y))
abort_pair_first
    |- !x y. first(abort_pair(x,y)) = x

3.4.2 A complete partial ordering

exseq_subseq
    |- !e d.
        e <=| d =
        (length e) <-+ (length d) /\
        (!n.
          (WHOLE n) <+ (length e) ==>
          (elt(WHOLE n)e = elt(WHOLE n)d))
exseq_subseq_strict
    |- !e d. e <| d = e <=| d /\ ~(e = d)
exseq_po
    |- partial_order $<=|
lengths
    |- !C. lengths C = (\n. length(C n))
length_chain
    |- !C. chain $<=| C ==> chain $<-+(lengths C)
exseq_subseq_as_length
    |- !C.
        chain $<=| C ==>
        (!i j. (length(C i)) <-+ (length(C j)) =
        (C i) <=| (C j))
lub_fn
    |- !C n.
        lub_fn C n =
        (@x. ?j.
             (x = elt(WHOLE n)(C j)) /\
             (WHOLE n) <+ (length(C j)))
lub_exseq
    |- !C.
        lub_exseq C =
        mk_exseq(lub_fn C,lub $<-+(lengths C))
lub_exseq_thm
    |- !C.
        chain $<=| C ==>

(length(lub_exseq C) = lub $<-+(lengths C)) /\
(!n.
  elt(WHOLE n)(lub_exseq C) =
  ((WHOLE n) <+ (length(lub_exseq C)) =>
   lub_fn C n | (@x. T)))
exseq_cpo
|- cpo $<=|
exseq_lub_elts
|- !Ch.
chain $<=| Ch ==>
(!n.
  elt(WHOLE n)(lub $<=| Ch) =
  ((WHOLE n) <+ (length(lub $<=| Ch)) =>
   lub_fn Ch n | (@x. T)))
exseq_lub_length
|- !Ch.
chain $<=| Ch ==>
(length(lub $<=| Ch) = lub $<-+(lengths Ch))

3.4.3 Arithmetic

splice
|- !x y.
splice x y =
(\n.
  ((WHOLE n) <+ (length x) =>
   elt(WHOLE n)x |
   elt((WHOLE n) -- (PR(length x)))y))
join_f
|- !x y.
(length(join_f x y) = (length x) ++ (PR(length y))) /\
(!n.
  elt(WHOLE n)(join_f x y) =
  ((WHOLE n) <+ ((length x) ++ (PR(length y))) =>
     splice x y n |
     (@x'. T)))
join
|- !x y.
TERM x ==>
(first y = last x) ==>
(x <*> y = x join_f y)
join_length

|- !x y.
TERM x ==>
(first y = last x) ==>
(length(x <*> y) = (length x) ++ (PR(length y)))
join_elts
|- !x y.
TERM x ==>
(first y = last x) ==>
(!n.
  elt(WHOLE n)(x <*> y) =
  ((WHOLE n) <+ (length x) =>
   elt(WHOLE n)x |
   ((WHOLE n) <+ (length(x <*> y)) =>
    elt((WHOLE n) -- (PR(length x)))y |
    (@q. T))))
join_TERM
|- !x y.
(first y = last x) ==>
TERM x ==>
(TERM y = TERM(x <*> y))
join_ABORT
|- !x y.
(first y = last x) ==>
TERM x ==>
(ABORT y = ABORT(x <*> y))
join_first
|- !x y.
TERM x ==>
(first y = last x) ==>
(first(x <*> y) = first x)
join_last
|- !x y.
(first y = last x) ==>
TERM x ==>
TERM y ==>
(last(x <*> y) = last y)
join_assoc
|- !e d f.
TERM e ==>
TERM d ==>
(first d = last e) ==>
(first f = last d) ==>
(e <*> (d <*> f) = (e <*> d) <*> f)

join_cancel
|- !e d f.
TERM e ==>
(first d = last e) ==>
(first f = last e) ==>
((e <*> d = e <*> f) = (d = f))
exseq_subtract
|- !e d.
d // e =
mk_exseq
((\n. elt((WHOLE n) ++ (PR(length e)))d),
 (length d) -- (PR(length e))
exseq_subtract_join
|- !e d. e <| d ==> (e <*> (d // e) = d)
join_inc
|- !e d.
 TERM e ==>
 (first d = last e) ==>
 e <| (e <*> d)
exseq_subseq_strict_join_cancel
|- !e d f.
TERM e ==>
(first d = last e) ==>
(first f = last e) ==>
((e <*> d) <| (e <*> f) = d <| f)
exseq_subseq_join_cancel
|- !e d f.
TERM e ==>
(first d = last e) ==>
(first f = last e) ==>
((e <*> d) <=| (e <*> f) = d <=| f)
exseq_subseq_join_subtract
|- !e d k.
TERM e ==>
(first d = last e) ==>
e <| k ==>
((e <*> d) <=| k = d <=| (k // e))
join_distrib_lub
|- !e Ch.
chain $<=| Ch ==>
TERM e ==>
(first(Ch 0) = last e) ==>
(e <*> (lub $<=| Ch) =

lub $<=|(\i. e <*> (Ch i)))

21

Commands

4.1 Partial Commands and recursion

Commands are sets of execution sequences. This allows partial commands, introduced by [Nel89, Mor88]. As there is no restriction on the sets, nondeterminism may be unbounded. A version of Dijkstra’s ‘guarded command’ language [DS90] is constructed by combining partial commands using unary and binary operators. The language is extended to include recursion and random assignment.

Commands are represented as a conservative extension of the logic, appearing as terms of the logic itself. This simplifies proofs involving programs but complicates reasoning about the language represented and its properties. This can be remedied by using a ‘meaning’ function in the denotational style, defined recursively over the structure of the language.

4.2 Predicates

Predicates are sets of states, where sets are identified with their membership predicates. Logical operators are ‘lifted’ to the predicate level, and a Dijkstra- style ‘everywhere’ function is defined.

NONE
   |- false = (\s. F)
ALL
   |- true = (\s. T)
NOT

   |- !b. NOT b = (\s. ~b s)
OR
   |- !b b'. b OR b' = (\s. b s \/ b' s)
AND
   |- !b b'. b AND b' = (\s. b s /\ b' s)
IMPLIES
   |- !b b'. b IMPLIES b' = (\s. b s ==> b' s)
EWR
   |- !p. EWR p = (!t. p t)
SW
   |- !p. SW p = (?t. p t)
bnd
   |- !x s value.
       bnd value x s = (\z. ((z = x) => value | s z))
forevery
   |- !P x. forevery x P = (\s. !val. P(bnd val x s))
forsome
   |- !P x. forsome x P = (\s. ?val. P(bnd val x s))
subs  |- !exp x P. subs exp x P = (\s. P(bnd(exp s)x s))

4.3 Semantics of commands

Definitions of atomic commands and unary and binary operators for combining commands.

grd
    |- !c s. grd c s = (?e. c e /\ (first e = s))
total
    |- !c. total c = (grd c = true)
det
    |- !c.
        det c =
        (!p1 p2.
          c p1 ==>
          c p2 ==>
          (first p2 = first p1) ==>
          (p1 = p2))
skip
    |- !p. skip p = (?s s'. p = pair(s',s'))
skip_grd
    |- grd skip = true

empty
    |- !e. empty e = F
empty_grd
    |- grd empty = false
abort
    |- !e. abort e = (?s. e = abort_pair(s,s))
abort_grd =
    |- grd abort = true
havoc
    |- havoc = (\e. TERM e)
havoc_grd =
    |- grd havoc = true
assign
    |- !x exp.
        x := exp =
        (\p. ?s s'. (p = pair(s,s')) /\
         (s' = bnd(exp s)x s))
assign_grd
    |- !exp x. grd(x := exp) = true
update
    |- !x s e.
        update x e =
        (?s' val. e = pair(s',bnd val x s'))
update_grd =
    |- !x. grd(update x) = true
choose
    |- !c1 c2. c1 || c2 = (\p. c1 p \/ c2 p)
choose_grd
    |- !c1 c2.
        grd(c1 || c2) = (grd c1) OR (grd c2)
orelse
    |- !c1 c2 e.
        (c1 |X| c2)e =
        c1 e \/ ~grd c1(first e) /\ c2 e
orelse_grd
    |- !c1 c1.
        grd(c1 |X| c2) = (NOT(grd c1)) IMPLIES (grd c2)
seq
    |- !c1 c2 e.
        (c1 ;; c2)e =
        c1 e /\ ~TERM e \/
        (?e1 e2.
          c1 e1 /\

          TERM e1 /\
          c2 e2 /\
          (first e2 = last e1) /\
          (e = e1 <*> e2))
seq_grd_total
    |- !c1 c2. total c2 ==> (grd c1 = grd(c1 ;; c2))
seq_assoc
    |- !c1 c2 c3.
        (c1 ;; c2) ;; c3 = c1 ;; (c2 ;; c3)
gcom
    |- !P c. P --> c = (\e. P(first e) /\ c e)
gcom_grd
    |- !P c. grd(P --> c) = P AND (grd c)
If_fI
    |- !c. If_fI c = c |X| abort
If_fI_grd
    |- !c. grd(If_fI c) = true
TTseq
    |- (!Seq. TTseq Seq 0 = Seq 0) /\
       (!Seq n. TTseq Seq(SUC n) =
         (TTseq Seq n) <*> (Seq(n + 1)))
TTseq_chain
    |- !Seq.
        (!n. TERM(Seq n) /\
             (first(Seq(n + 1)) = last(Seq n))) ==>
        chain $<=|(TTseq Seq)
iter
    |- (!c. c ^^0 = c) /\
       (!c n. c ^^(SUC n) = c ;; (c ^^n))
iter_swop
    |- !n c. (c ^^n) ;; c = c ;; (c ^^n)
next
    |- !c e e'.
        next c e e' =
        TERM e /\ c e' /\ (first e' = last e)
rec
    |- !c e.
        rec c e =
        (?Seq.
          c(Seq 0) /\
          ((?m.
             (!n. n < m ==> next c(Seq n)(Seq(SUC n))) /\
             (!e'. ~next c(Seq m)e') /\

(e = TTseq Seq m)) \/
(!n. next c(Seq n)(Seq(SUC n))) /\
(e = lub $<=|(TTseq Seq))))
rec_grd
|- !c. grd c = grd(rec c)
do_od
|- !c. do_od c = (rec c) |X| skip

Programming Logics

5.1 Weakest Preconditions

Dijkstra’s weakest (liberal) precondition operator is defined. The healthiness conditions on the two predicate transformers are derived from the semantics. The axiomatic semantics of the language, in terms of predicate transformers, is derived. Throughout non-determinism is unbounded. The semantics derived is due to [Heh79] and [Nel89], whose semantics extends that of Dijkstra to include recursion and partial commands

5.1.1 Predicate transformers

wp
    |- !c R s.
        wp c R s =
(!e. c e ==>
             (first e = s) ==>
             TERM e /\ R(last e))
wlp
    |- !c R s.
        wlp c R s =
(!e. c e ==>
             (first e = s) ==>
             TERM e ==>
             R(last e))
wp_wlp_pairing
    |- !c R. wp c R = (wlp c R) AND (wp c true)

5.1.2 Healthiness conditions

excluded_miracle
    |- !c.
        (grd c = true) ==> (wp c false = false)
conjunctivity_wp
    |- !c Q R.
        (wp c Q) AND (wp c R) = wp c(Q AND R)
conjunctivity_wlp
    |- !c Q R.
        (wlp c Q) AND (wlp c R) = wlp c(Q AND R)
disjunctivity_wp
    |- !c Q R.
        EWR(((wp c Q) OR (wp c R)) IMPLIES
            (wp c(Q OR R)))
disjunctivity_wlp
    |- !c Q R.
        EWR(((wlp c Q) OR (wlp c R)) IMPLIES
             (wlp c(Q OR R)))
det_disjunctivity_wp
    |- !c Q R.
        det c ==>
        ((wp c Q) OR (wp c R) = wp c(Q OR R))
det_disjunctivity_wlp
    |- !c Q R.
        det c ==>
        ((wlp c Q) OR (wlp c R) = wlp c(Q OR R))

5.1.3 Semantics of guarded commands

skip_wp
    |- !R. wp skip R = R
skip_wlp
    |- !R. wlp skip R = R
empty_wp
    |- !R. wp empty R = true
empty_wlp
    |- !R. wlp empty R = true
abort_wp
    |- !R. wp abort R = false
abort_wlp
    |- !R. wlp abort R = true

havoc_wp
    |- !R. wp havoc R = (\s. EWR R)
havoc_wlp
    |- !R. wlp havoc R = (\s. EWR R)
assign_wp
    |- !R x exp. wp(x := exp)R = subs exp x R
assign_wlp
    |- !R x exp. wlp(x := exp)R = subs exp x R
update_wp
    |- !x P. wp(update x)P = forevery x P
update_wlp
    |- !x P. wlp(update x)P = forevery x P
choose_wp
    |- !c1 c2 R.
        wp(c1 || c2)R = (wp c1 R) AND (wp c2 R)
choose_wlp
    |- !c1 c2 R.
        wlp(c1 || c2)R = (wlp c1 R) AND (wlp c2 R)
orelse_wp
    |- !c1 c2 R.
        wp(c1 |X| c2)R =
        (wp c1 R) AND ((grd c1) OR (wp c2 R))
orelse_wlp
    |- !c1 c2 R.
        wlp(c1 |X| c2)R =
        (wlp c1 R) AND ((grd c1) OR (wlp c2 R))
seq_wp
    |- !c1 c2 R. wp(c1 ;; c2)R = wp c1(wp c2 R)
seq_wlp
    |- !c1 c2 R. wlp(c1 ;; c2)R = wlp c1(wlp c2 R)
gcom_wp
    |- !c P R. wp(P --> c)R = P IMPLIES (wp c R)
gcom_wlp
    |- !c P R. wlp(P --> c)R = P IMPLIES (wlp c R)
If_fI_wp
    |- !c R.
        wp(if_fi c)R = (wp c R) AND (grd c)
If_fI_wlp
    |- !c R.
        wlp(if_fi c)R = (wlp c R) AND (grd c)
gcom_If_fI_wp =
    |- !c1 c2 P1 P2 R.
        total c1 /\ total c2 ==>

        (wp(If_fI((P1 --> c1) || (P2 --> c2)))R =
        (P1 OR P2) AND
        ((P1 IMPLIES (wp c1 R)) AND
         (P2 IMPLIES (wp c2 R))))
gcom_If_fI_wlp =
    |- !c1 c2 P1 P2 R.
        total c1 /\ total c2 ==>
        (wlp(If_fI((P1 --> c1) || (P2 --> c2)))R =
        (P1 IMPLIES (wlp c1 R)) AND (P2 IMPLIES (wlp c2 R)))
conseq
    |- !c1 c2.
        c1 <o> c2 =
        (c1 ;; c2) || (c1 <-- (NOT(grd c2)))
rec_fixed  |- !c. c <o> (rec c) = rec c
skip_right_id_wp  |- !c R. wp(c ;; skip)R = wp c R
skip_right_id_wlp  |- !c R. wlp(c ;; skip)R = wlp c R
do_od_total
    |- !c. total(do_od c)
grd_seq_total
    |- !c1 c2. total c2 ==> (grd c1 = grd(c1 ;; c2))
right_grd
    |- !c P e.
        (c <-- P)e = c e /\ TERM e /\ P(last e)
orelse_seq
    |- !c1 c2 c3.
        c1 ;; (c2 |X| c3) =
(c1 ;; c2) || ((c1 <-- (NOT(grd c2))) ;; c3)
fix
    |- !c R pt P.
        fix pt c R P =
        (P = (pt c P) AND ((grd c) OR R))
rec_fixed_wp
    |- !c R. wp(rec c)R = wp(c ;; ((rec c) |X| skip))R
do_od_wp_fix
    |- !c R. fix wp c R(wp(do_od c)R)
do_od_wp_strongest_fix
    |- !P c R. fix wp c R P ==> (!s. wp(do_od c)R s ==> P s)
rec_fixed_wlp
    |- !c R. wlp(rec c)R = wlp(c ;; ((rec c) |X| skip))R
do_od_wlp_fix
    |- !c R. fix wlp c R(wlp(do_od c)R)
do_od_wlp_weakest_fix

    |- !P c R. fix wlp c R P ==> (!s. P s ==> wlp(do_od c)R s)

5.2 Hoare Logic

A Hoare logic for partial correctness is derived. This is a natural adaptation of the logic for total commands including unbounded nondeterminism, given by [Apt84], to partial commands with recursion.

In addition, a Hoare logic for total correctness is derived. The proof rule for termination of recursion uses well-founded sets to cover unbounded nondeterminism. This is analogous to Apt’s use of ordinals in [Apt84].

5.2.1 Partial correctness

spec
    |- !P Q c.
        spec P c Q =
        (!e. c e ==>
             P(first e) ==>
             TERM e ==>
             Q(last e))
spec_as_wlp
    |- !P Q c. spec P c Q = (!s. P s ==> wlp c Q s)
skip_spec
    |- !P. spec P skip P
abort_spec
    |- !P. spec true abort P
havoc_spec
    |- !P. spec(\s. EWR P)havoc P
assign_spec
    |- !P Q x e. spec(subs e x P)(x := e)P
update_spec
    |- !x P. spec(forevery x P)(update x)P
seq_spec
    |- !P Q R c1 c2.
        spec P c1 Q /\ spec Q c2 R ==> spec P(c1 ;; c2)R
gcom_spec
    |- !P Q b c. spec(P AND b)c Q ==> spec P(b --> c)Q
choose_spec
    |- !P Q c1 c2.
        spec P c1 Q /\

spec P c2 Q ==>
spec P(c1 || c2)Q
orelse_spec
|- !P Q c1 c2.
spec P c1 Q /\
spec(P AND (NOT(grd c1)))c2 Q ==>
spec P(c1 |X| c2)Q
If_fI_spec
|- !P Q c. spec P c Q ==> spec P(If_fI c)Q
weaken_spec
|- !P1 Q1 P Q.
(!s. P s ==> P1 s) /\
(!s. Q1 s ==> Q s) /\
spec P1 c Q1 ==>
spec P c Q
gcom_If_fI_spec
|- !P Q b1 b2 c1 c2.
spec(P AND b1)c1 Q ==>
spec(P AND b2)c2 Q ==>
spec P(If_fI((b1 --> c1) || (b2 --> c2)))Q
rec_spec
|- !c P.
spec P c P ==> spec P(rec c)(P AND (NOT(grd c)))
do_od_spec
|- !c P.
spec P c P ==> spec P(do_od c)(P AND (NOT(grd c)))

5.2.2 Total correctness

halts
|- !P c.
halts P c =
(!e. c e ==> P(first e) ==> TERM e)
total_spec
|- !c P Q.
total_spec P c Q = spec P c Q /\ halts P c
halts_as_wp
|- !P c. halts P c = (!s. P s ==> wp c true s)
total_spec_as_wp
|- !P Q c. total_spec P c Q = (!s. P s ==> wp c Q s)
skip_halts
|- !P. halts P skip

skip_total_spec
    |- !P. total_spec P skip P
abort_halts
    |- halts false abort
abort_total_spec
    |- !P. total_spec false abort P
havoc_halts
    |- !P. halts P havoc
havoc_total_spec
    |- !P. total_spec(\s. EWR P)havoc P
empty_halts
    |- halts true empty
empty_total_spec
    |- !P. total_spec true empty P
assign_halts
    |- !P x e. halts P(x := e)
assign_total_spec
    |- !P x e. total_spec(subs e x P)(x := e)P
update_halts
    |- !P x. halts P(update x)
update_total_spec
    |- !P x. total_spec(forevery x P)(update x)P
seq_halts
    |- !P Q c1 c2.
        halts P c1 ==>
        spec P c1 Q ==>
        halts Q c2 ==> halts P(c1 ;; c2)
seq_total_spec
    |- !P Q R c1 c2.
        total_spec P c1 Q /\ total_spec Q c2 R ==>
        total_spec P(c1 ;; c2)R
gcom_halts
    |- !P b c. halts(P AND b)c ==> halts P(b --> c)
gcom_total_spec
    |- !P Q b c.
        total_spec(P AND b)c Q ==>
        total_spec P(b --> c)Q
choose_halts
    |- !P c1 c2.
        halts P c1 /\
        halts P c2 ==>
        halts P(c1 || c2)
choose_total_spec

|- !P Q c1 c2.
total_spec P c1 Q /\
total_spec P c2 Q ==>
total_spec P(c1 || c2)Q
orelse_halts
|- !P c1 c2.
halts P c1 /\
halts(P AND (NOT(grd c1)))c2 ==>
halts P(c1 |X| c2)
orelse_total_spec
|- !P Q c1 c2.
total_spec P c1 Q /\
total_spec(P AND (NOT(grd c1)))c2 Q ==>
total_spec P(c1 |X| c2)Q
If_fI_halts
|- !P c.
(!s. P s ==> grd c s) ==>
halts P c ==> halts P(If_fI c)
If_fI_total_spec
|- !P Q c.
(!s. P s ==> grd c s) /\
total_spec P c Q ==>
total_spec P(If_fI c)Q
weaken_halts
|- !P P1.
(!s. P s ==> P1 s) /\
halts P1 c ==>
halts P c
weaken_total_spec
|- !P1 Q1 P Q.
(!s. P s ==> P1 s) /\
(!s. Q1 s ==> Q s) /\
total_spec P1 c Q1 ==>
total_spec P c Q
gcom_If_fI_total_spec
|- !P Q b1 b2 c1 c2.
(!s. P s ==>
     ((b1 AND (grd c1)) OR (b2 AND (grd c2)))s) /\
total_spec(P AND b1)c1 Q /\
total_spec(P AND b2)c2 Q ==>
total_spec P(If_fI((b1 --> c1) || (b2 --> c2)))Q
do_od_total_spec
|- !W R c P t.

wfp W R ==>
(!s. P s /\ grd c s ==> W(t s)) ==>
(!val.
  total_spec
  (P AND (\s. t s = val))c(P AND (\s. R(t s)val))) ==>
total_spec P(do_od c)(P AND (NOT(grd c)))

5.3 Invariant Relations

The presence in the semantics of information about intermediate states is exploited by constructing a logic for proving the invariance of relations. This connects with temporal logic, in the formulation of safety and liveness properties using modal operators. These invariants can be used to prove properties of potentially nonterminating programs, and show the usefulness of distinguishing abortion from nontermination.

exseq_inv
|- !e R.
exseq_inv e R =
~ABORT e /\
(!n.
  (WHOLE n) <+ (PR(length e)) ==>
  R(elt(WHOLE n)e,elt(WHOLE(SUC n))e))
exseq_inv_join
|- !e1 e2 R1 R2.
(first e2 = last e1) ==>
TERM e1 ==>
exseq_inv e1 R1 ==>
exseq_inv e2 R2 ==>
exseq_inv(e1 <*> e2)(R1 OR R2)
exseq_inv_join_single
|- !e1 e2 R.
(first e2 = last e1) ==>
TERM e1 ==>
exseq_inv e1 R ==>
exseq_inv e2 R ==>
exseq_inv(e1 <*> e2)R
lub_exseq_inv
|- !C R.
chain $<=| C ==>
(!n. exseq_inv(C n)R) ==>
exseq_inv(lub $<=| C)R

dom
    |- !R s. dom R s = (?t. R(s,t))
ran
    |- !R t. ran R t = (?s. R(s,t))
rinv
    |- !R c P.
        c rinv (P,R) =
        (!e. c e ==> P(first e) ==> exseq_inv e R)
dom_OR
    |- !R1 R2. dom(R1 OR R2) = (dom R1) OR (dom R2)
OR_sym
    |- !R1 R2. R1 OR R2 = R2 OR R1
exseq_inv_OR
    |- !e R1 R2. exseq_inv e R1 ==> exseq_inv e(R1 OR R2)
exseq_inv_ran
    |- !e. TERM e ==> exseq_inv e R ==> ran R(last e)
skip_rinv
    |- !P R. (!s. P s ==> R(s,s)) ==> skip rinv (P,R)
empty_rinv
    |- !P R. empty rinv (P,R)
abort_rinv
    |- !P R. (P = false) ==> abort rinv (P,R)
havoc_rinv
    |- !P R. (!s t. R(s,t)) ==> havoc rinv (P,R)
gcom_rinv
    |- !c P R. c rinv (b AND P,R) ==> (b --> c) rinv (P,R)
assign_rinv
    |- !P R x exp.
        (!s. P s ==> R(s,bnd(exp s)x s)) ==>
        (x := exp) rinv (P,R)
update_rinv
    |- !P R x.
        (!s val. P s ==> R(s,bnd val x s)) ==>
        (update x) rinv (P,R)
seq_rinv
    |- !c1 c2 P R.
        c1 rinv (P,R) ==>
        c2 rinv (ran R,R) ==>
       (c1 ;; c2) rinv (P,R)
choose_rinv
    |- !c1 c2 R P.

c1 rinv (P,R) /\
c2 rinv (P,R) ==>
(c1 || c2) rinv (P,R)
orelse_rinv
|- !c1 c2 R P.
c1 rinv (P,R) /\
c2 rinv ((NOT(grd c1)) AND P,R) ==>
(c1 |X| c2) rinv (P,R)
If_fI_rinv
|- !c P R.
c rinv (P,R) /\
(!s. P s ==> grd c s) ==>
(If_fI c) rinv (P,R)
rec_rinv
|- !c R.
c rinv (P,R) /\
(!s. ran R s ==> P s) ==>
(rec c) rinv (P,R)
do_od_rinv
|- !R c P.
(!s. ran R s ==> P s) /\
c rinv (P,R) /\
(!s. ((NOT(grd c)) AND P)s ==> R(s,s)) ==>
(do_od c) rinv (P,R)

5.4 Temporal Logic

The axioms for the temporal logic DX described in [Pnu81] are derived, with an additional distinction between abortion and nontermination.

let wff = define_type `wff`
`wff =   START
| TFINAL
| AFINAL
| ASSERT (state->bool)
| CONJ wff wff
| DISJ wff wff
| EQ wff wff
| NEG wff

| IMP wff wff
| NEXT wff
| ALL wff
| SOME wff`;;
  holds
    |- (!e i. holds e i START = (i = 0)) /\
       (!e i. holds e i TFINAL =
TERM e /\ (WHOLE i = PR(length e))) /\
       (!e i. holds e i AFINAL =
ABORT e /\ (WHOLE i = PR(length e))) /\
       (!e i P.
         holds e i(ASSERT P) =
         ((WHOLE i) <+ (length e) =>
P(elt(WHOLE i)e) | P(last e))) /\
       (!e i fmla. holds e i(NEG fmla) = ~holds e i fmla) /\
       (!e i fmla1 fmla2.
         holds e i(IMP fmla1 fmla2) =
         holds e i fmla1 ==> holds e i fmla2) /\
       (!e i fmla1 fmla2.
         holds e i(CONJ fmla1 fmla2) =
         holds e i fmla1 /\ holds e i fmla2) /\
       (!e i fmla1 fmla2.
         holds e i(DISJ fmla1 fmla2) =
         holds e i fmla1 \/ holds e i fmla2) /\
       (!e i fmla1 fmla2.
         holds e i(EQ fmla1 fmla2) =
(holds e i fmla1 = holds e i fmla2)) /\
       (!e i fmla. holds e i(NEXT fmla) =
holds e(SUC i)fmla) /\
       (!e i fmla.
         holds e i(ALL fmla) =
(!j. i <= j ==> holds e j fmla)) /\
       (!e i fmla.
         holds e i(SOME fmla) =
(?j. i <= j /\ holds e j fmla))
  sat  |- !fmla. |= fmla = (!e i. holds e i fmla)
  csat  |- !c f. c |== f = (!e i. c e ==> holds e i f)
  ALL_ALL  |- !fmla. |=(EQ(ALL(ALL fmla))(ALL fmla))
  SOME_SOME  |- !fmla. |=(EQ(SOME(SOME fmla))(SOME fmla))
  ALL_once  |- !fmla. |=(IMP(ALL fmla)fmla)
  NEXT_NEG  |- !fmla. |=(EQ(NEXT(NEG fmla))(NEG(NEXT fmla)))

ALL_over_imp
  |- !fmla1 fmla2.
      |=(IMP(ALL(IMP fmla1 fmla2))
(IMP(ALL fmla1)(ALL fmla2)))
NEXT_over_imp
  |- !fmla1 fmla2.
      |=(IMP(NEXT(IMP fmla1 fmla2))
(IMP(NEXT fmla1)(NEXT fmla2)))
ALL_NEXT  |- !fmla. |=(IMP(ALL fmla)(NEXT fmla))
ALL_NEXT_ALL  |- !fmla. |=(IMP(ALL fmla)(NEXT(ALL fmla)))
ALL_imp_NEXT_ALL
  |- !fmla. |=(IMP(ALL(IMP fmla(NEXT fmla)))
(IMP fmla(ALL fmla)))
SOME_as_ALL  |- !fmla. |=(EQ(SOME fmla)(NEG(ALL(NEG fmla))))
modus_ponens  |- !f1 f2. |= f1 /\ |=(IMP f1 f2) ==> |= f2
generalize  |- !f. |= f ==> |=(ALL f)
sat_csat  |- !f. |= f ==> (!c. c |== f)
spec_as_temp
  |- !c P Q.
      spec P c Q =
      c |== (IMP(CONJ(ASSERT P)START)
(ALL(IMP TFINAL(ASSERT Q))))
total_spec_as_temp
  |- !c P Q.
      total_spec P c Q =
      c |== (IMP(CONJ(ASSERT P)START)
(SOME(CONJ TFINAL(ASSERT Q))))

Conclusion and further work

The document has shown that programming logics can be mechanized in HOL using execution sequences, forming a conservative extension of the logic. The higher-order nature of the logic makes the mechanization natural, as the expressiveness of the logic can be exploited. In particular polymorphism and higher-order variables facilitate the mechanization.

Moreover, extensions to existing logics for reasoning about partial commands and properties of potentially nonterminating programs, can be made in a sound way, without fear of introducing inconsistency. This uses HOL for investigating the logics themselves.

Bibliography

[ACG87] T.F. Melham A.J. Camilleri and M.J.C. Gordon. Hardware verification using Higher-Order Logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 43–67. Proceedings of the IFIP WG 10.2 Working Conference, Grenoble, September 1986, North-Holland, 1987.

[Age92] Sten Agerholm. Mechanizing program verification in HOL. Technical Report DAIMI IR - 111, Aarhus University, April 1992.

[And86] P.B. Andrews. An Introduction to Mathematical Logic and Type Theory: to Truth through Proof. Computer Science and Applied Mathematics Series. Academic Press, 1986.

[AP86] K.R. Apt and G. Plotkin. Countable nondeterminism and random assignment. Communications of the ACM, 33(4):724–767, October 1986.

[Apt84] K.R. Apt. Ten years of Hoare’s logic: a survey - part II: Nondeterminism. Theoretical Computer Science, 28:83–109, 1984.

[Bac92] R.J.R. Back. Refinement calculus, lattices and Higher Order Logic. Nato Advanced Study Institute, Program Design Calculi, International Summer School, Marktoberdorf, August 1992. Working Material.

[Bli87] A. Blikle. Proving programs by sets of computations. volume 375 of Lecture Notes in Computer Science, pages 333–358. Springer-Verlag, 1987.

[BM79] R.S. Boyer and J.S. Moore. A Computational Logic. ?, 1979.

[BM81] R.S. Boyer and J.S. Moore. Metafunctions: Proving them correct and using them efficiently as new proof procedures. In R.S. Boyer and J.S. Moore, editors, The Correctness Problem in Computer Science. Academic Press, New York, 1981.

[BR91] C. Brink and I. Rewitzky. Modelling the algebra of weakest preconditions. pages 242–261. Proceedings of the 6th Southern African Computer Symposium, Caledon, 2-3 July 1991, 1991. Also to appear in the South African Computer Journal.

[BvW90] R.J.R. Back and J. von Wright. Refinement concepts formalised in Higher Order Logic. Formal Aspects of Computing, 2(3):247–272, July-September 1990.

[Cam90] A.J. Camilleri. Mechanizing CSP trace theory in Higher Order Logic. IEEE Transactions on Software Engineering, 16(9):993–1004, September 1990.

[Chu40] A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

[Dij76] E.W.D. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

[DS90] E.W.D. Dijkstra and C.S. Scholten. Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer-Verlag, 1990.

[Flo67] R. Floyd. Nondeterministic algorithms. Journal of the ACM, 4:636–644, 1967.

[Gor88] M.J.C. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwistle and P.A. Subrahmanyan, editors, VLSI Specification, Verification and Synthesis, Kluwer International Series in Engineering and Computer Science, pages 73–128. Kluwer Academic Publishers, Boston, 1988.

[Gor89] M.J.C. Gordon. Mechanizing programming logics in Higher Order Logic. In G. Birtwistle and P.A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem-Proving, pages 387–439. Springer-Verlag, 1989.

[Gri81] D. Gries. The Science of Programming. Springer-Verlag, 1981.

[Heh79] E.C.R. Hehner. do considered od: a contribution to the programming calculus. Acta Informatica, 11, 1979.

[Lei69] A. Leisenring. Mathematical Logic and Hilbert’s ϵ-Symbol. University Mathematical Series. Macdonald & Co. Ltd., London, 1969.

[Mad92] R.D. Maddux. Relational calculus and program semantics: The derivation of the Dijkstra-Scholten predicate transformer semantics from Tarski’s axioms for the Peirce-Schröder calculus of relations. Lecture Notes, Workshop on Formal Aspects of Computer Science, University of Cape Town, 6–17 July 1992, July 1992.

[MC80] M.E. Majster-Cederbaum. A simple relation between relational and predicate transformer semantics for nondeterministic programs. Information Processing Letters, 11(4-5):190–192, December 1980.

[Mel] T.F. Melham. A mechanized theory of the π-calculus in HOL. In G. Huet and G.D. Plotkin, editors, Proceedings of the 2nd Esprit BRA Workshop on Logical Frameworks. ?, ? to appear.

[Mel89] T.F. Melham. Automating recursive type definitions in Higher Order Logic. In G. Birtwistle and P.A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341–386. Springer-Verlag, 1989.

[MGW79] R. Milner M.J.C. Gordon and C.P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

[Mil78] R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978.

[Mil85] R. Milner. The use of machines to assist in rigorous proof. In C. Hoare and J.C. Sheperdson, editors, Mathematical Logic and Programming Languages. Prentice-Hall, 1985.

[Mor88] Carrol Morgan. Data refinement by miracles. Information Processing Letters, 26:243–246, January 1988.

[MP83] Z. Manna and A. Pnueli. How to cook a temporal proof system for your pet language. In Proceedings of the Tenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, pages 141–154, January 1983.

[Nel89] G. Nelson. A generalization of Dijkstra’s calculus. ACM Transactions on Programming Languages and Systems, 11(4):517–561, October 1989.

[Pau83] L. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119–149, 1983.

[Pau87] L. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge Tracts in Theoretical Computer Science 2. Cambridge University Press, 1987.

[Plo79] Gordon Plotkin. Dijkstra’s predicate transformers and Smyth’s powerdomains. In D. Bjørner, editor, Abstract Software Specifications, Lecture Notes in Computer Science 86, pages 527–553. Springer, 1979.

[Pnu81] A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45–60, 1981.

[Rew91] I.M. Rewitzky. Modelling the algebra of weakest preconditions. Master’s thesis, Department of Mathematics, University of Cape Town, Rondebosch, 7700, South Africa, September 1991.