HOL-UNITY

A Theory for UNITY

in

The Cambridge HOL System

PRELIMINARY VERSION

Flemming Andersen

October 30, 1992

Contents

Preface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

1 Introduction 3 1.1 Predicate Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2 Safety Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.3 Progress Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.4 Compositionality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.5 Representing Programs in HOL-UNITY . . . . . . . . . . . . . . . . 7 1.6 The Structure of the HOL-UNITY Theory Files . . . . . . . . . . . . 8

2 Applications of the Mechanized UNITY System 9 2.1 Defining State and Program . . . . . . . . . . . . . . . . . . . . . . . 10 2.2 Mutual Exclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

2.2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.2.2 UNITY Specification . . . . . . . . . . . . . . . . . . . . . . . 13 2.2.3 Specification in HOL-UNITY . . . . . . . . . . . . . . . . . . 15

2.3 The readers/writers Problem . . . . . . . . . . . . . . . . . . . . . . . 23 2.3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.3.2 A readers/writers Program with writers Progress . . . . . . . 24 2.3.3 Verifying User Properties using HOL-UNITY . . . . . . . . . 25 2.3.4 Defining a Program Representation . . . . . . . . . . . . . . . 26 2.3.5 Proving Program Properties . . . . . . . . . . . . . . . . . . . 29

2.4 A 2-Arbiter . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2.4.1 Specifying the System . . . . . . . . . . . . . . . . . . . . . . 37 2.4.2 A 2-Arbiter Program and its Verification . . . . . . . . . . . . 41 2.4.3 The 2-Arbiter in HOL-UNITY . . . . . . . . . . . . . . . . . . 51

Appendix A UNITY - Theorems and Corollaries 55 Appendix B HOL-UNITY - Definitions and Theorems 61

ii

Preface

This report contains preliminary documentation of the present HOL-UNITY theory.^{1} The report is intended to be turned into a manual with guide lines for using the HOL-UNITY system.

The report contains a brief introduction to a number of theories defined in the Cambridge HOL system [Gor87a, Gor87b]. Collectively these theories completely formal define the UNITY theory, less formally put forward in [CM88], using the higher order logic notation supported by the HOL system. Three examples apply the HOL-UNITY theories for obtaining a mechanized verification of specified UNITY properties.

To read this document, knowledge of the HOL system and its notation is required. More verbose presentations of the HOL-UNITY theories and the three examples using HOL-UNITY are also presented in [And92].

1This work was supported partly by The Technical University, Lyngby, Denmark and partly by TFL.

2

Chapter 1

Introduction

UNITY is a theory for proving properties ascribed to concurrent programs. The theory defines a logic for describing safety and progress properties of programs, and includes a simple programming language for specifying algorithms which implement the behavior required by given properties. By implementing the UNITY theory in the HOL system, a mechanized theorem prover for UNITY has been developed with a rather general applicability. The resulting UNITY theory, called HOL-UNITY, is a complete definition of the theory in [CM88] with all definitions, theorems, corollaries and induction principles included. At the present time, the syntactical representation of UNITY properties and programs must be given in HOL terms. This problem may be overcome by implementing a syntactic interface to the present system, but has been postponed in this project. HOL-UNITY is defined as a conservative extension of the existing higher order logic supported by the HOL theorem prover. This way of defining the UNITY theory guarantees that the resulting theory is sound and consistent. However, although the HOL logic is relatively complete, the HOL-UNITY theory, defined here, is not complete, since it is defined in terms of pre- post conditions [Hoa69, Dij76], meaning that the logic is defined as a universally quantified proof theory which range over all possible states dependent only of the variable (polymorphic) type of the state. The price paid for this approach is the lack of the substitution theorem. To get a HOL-UNITY theory including the substitution theorem (i.e., a complete theory), the definitions of the properties have to be restricted to the reachable states of the program for which the relations must hold. The present theory may be modified to suit this requirement by restricting the quantification over states by a predicate which returns only program states. In [San91, Mis90, And92] suggestions are presented on how to redefine the unless and ensures properties to meet the completeness requirement.

The HOL-UNITY theory is defined as a collection of HOL theories. As a result, all the theorems and corollaries presented in [CM88] are proved as HOL theorems derived from the HOL definitions of the logic properties given in [CM88]. Appendix A and B contains an overview of the theorems and definitions in the HOL-UNITY theories.

The defined theories are briefly introduced in the following sections.

1.1 Predicate Logic

First a predicate logic theory is defined with the usual operators of conjunction, disjunction, etc. The predicate logic is needed because the UNITY properties unless, stable, invariant, ensures and leadsto are relations between predicates dependent on program states. The predicate logic operators are denoted by their usual symbols postfixed by an asterisk (∗). That is, e.g. logic conjunction:

p ∧ q

becomes

p ∧_{∗} q = λs. p s ∧ q s

The other operators are defined in a similar way. Several theorems known from traditional logic which are used in the later theories are proved for the defined predicates in the theory.

1.2 Safety Properties

This section defines the safety properties unless, stable and invariant as described in [CM88]:

• p unless q in P r whenever P r reaches a state in which p holds, all transitions must preserve p or make q hold.

• p stable in P r is the special unless relation p unless false in P r. Whenever P r reaches a state in which p holds, all transitions must preserve p.

• q invariant in (P r, P r_{init}) q must hold in the initial states given by the predicate P r_{init}, and all state transitions must preserve p.

Formally, these properties are defined by:

• p unless q in P r

\begin{matrix}= & ∀st ∈ P r: \{p ∧ ¬q\} st \{p ∨ q\} \\ = & ∀st ∈ P r: ∀s: p s ∧ ¬q s ⇒ p (st s) ∨ q (st s) \end{matrix}

• p stable in P r

= p unless false in P r

• p invariant in (p_{init}, P r)

= (∀s: p_{init} s ⇒ p s) ∧ p unless false in P r

in higher order logic.

1.3 Progress Properties

This section describes the definition of the progress properties ensures and leadsto:

• p ensures q in P r whenever P r reaches a state in which p holds, all transitions must preserve p until q hold. And (at least) one transition, from a state satisfying p, exists which makes q hold.

• p leadsto q in P r The smallest transitive and disjunctive closure of ensures properties.

Formally, these properties are defined by:

• p ensures q in P r

= p unless q in P r ∧

∃st ∈ P r: ∀s: p s ∧ ¬q s ⇒ q (st s)

• Define leadsto as least fixed point of

p ensures q  ⇒ p leadsto q
(∃r : p leadsto r ∧ r leadsto q)  ⇒ p leadsto q
(∃P : (p = ⋃ P) ∧ (∀r ∈ P : r leadsto q)) ⇒ p leadsto q

in higher order logic. In the definition of leadsto, ⋃ P is the least upper bound (lub) of a set P of state dependent predicates.

The leadsto Induction principles

From the definition of leadsto as the least fixed point we may derive the two theorems below. These theorems are derived from the definition of leadsto as the minimal fixed point [And92]. Hence, they are the mathematical foundation of the leadsto induction principles used in [CM88].

∀X: (∀p q P r: p ensures q in P r ⇒ X p q P r) ∧ (∀p q r P r:

p leadsto r in P r ∧ X p r P r ∧ r leadsto q in P r ∧ X r q P r ⇒ X p q P r) ∧

(∀p q P P r: (p = (⋃ P)) ∧ (∀r ∈ P: X r q in P r) ∧ (∀r ∈ P: r leadsto q in P r) ⇒ X p q P r)

⇒ (∀p q P r: p leadsto q in P r ⇒ X p q P r)

∀X: (∀p q P r: p ensures q in P r ⇒ X p q P r) ∧ (∀p q r P r:

p ensures r in P r ∧ X p r P r ∧ r leadsto q in P r ∧ X r q P r ⇒ X p q P r) ∧

(∀p q P P r: (p = (⋃ P)) ∧ (∀r ∈ P: X r q in P r) ∧ (∀r ∈ P: r leadsto q in P r) ⇒ X p q P r)

⇒ (∀p q P r: p leadsto q in P r ⇒ X p q P r) Notice that the only difference between the two theorems lies in the assumption of the existence of a transitive closure step. The definition of leadsto as the least fixed point and the proof of the two induction theorems are based on a fixed point theory described in [AP91, And92], originally proposed in [Tar55].

1.4 Compositionality

In [CM88] a simple compositionality principle is defined. This compositionality principle is easily proved to be satisfied as theorems in higher order logic derived from the above definitions of unless and ensures. An unless property is satisfied by the composed program (P_{1} ⋃ P_{2}) if and only if it is satisfied by each of the components P_{1} and P_{2}.

• unless Compositionality

p unless q in (P_{1} ⋃ P_{2})

= (p unless q in P_{1} ∧ p unless q in P_{2})

An ensures property is satisfied by the composed program (P_{1} ⋃ P_{2}) if and only if unless is satisfied by the one component and ensures is satisfied by the other.

• ensures Compositionality

p ensures q in (P_{1} ⋃ P_{2})

= (p ensures q in P_{1} ∧ p unless q in P_{2}) ∨
(p ensures q in P_{2} ∧ p unless q in P_{1})

1.5 Representing Programs in HOL-UNITY

In the present version of HOL-UNITY, a UNITY program is represented as a list of state transitions. This decision was made because a set theory was not available in HOL at the beginning of this project. The list representation is however still valid since no definition or theorem makes use of any particular ordering of state transitions of a program. The validity of the representation is proved by theorems in the theory defining compositionality. These theorems prove for every UNITY property (unless, stable, invariant, ensures and leadsto) that the set of program statements represented as a list of state transitions does not affect the validity of a property already satisfied even if the state transitions in the list are reordered. The transformation of a UNITY program into a list of state transitions is explained in [And92]. However, the last two examples on using HOL-UNITY in this report also presents the used methods for representing a program as a list of conditional state transitions expressed as lambda expressions.

1.6 The Structure of the HOL-UNITY Theory

Files

aux definitions Defines some new special symbols needed to introduce the state ab-

stracted logical operators, and defines some tactics and ML functions used. l unity Load this file into your HOL system and you are working in the defined

UNITY theory. mk state logic Defines state abstracted logical predicates and theorems used in the

HOL-UNITY theory. mk unless Defines the UNITY safety properties: UNLESS, STABLE and INVARI-

ANT and proves the theorems and corollaries presented in [CM88]. mk ensures Defines the basic progress property: ENSURES and proves the theorems

and corollaries presented in [CM88]. mk gen induct Proves the theorem of generalized induction on the natural numbers

(used in the leadsto theory). mk leadsto Defines the progress property: LEADSTO and proves the theorems and

corollaries presented in [CM88]. leadsto induct0 Defines a LEADSTO induction tactic. mk comp unity Proves the UNITY composition principle and the theorems and

corollaries of [CM88] to be satisfied. mk until This theory currently only contains the definition of the UNTIL property. examples/mk example01 The mutual exclusion example in [CM88] page 168-170. examples/mk example02 The readers/writers example in [CM88] page 139-140. examples/mk example03 An example of a 2-arbiter (description in the program file).

Chapter 2

Applications of the Mechanized UNITY System

Since the mechanized UNITY theory HOL-UNITY is implemented as a theory using the HOL theorem prover, working with HOL-UNITY is just like working with the HOL system having the UNITY definitions and theorems available as proved theorems in the HOL logic. A more user friendly mechanization of UNITY would require a syntactic interface, but to implement a syntax analyzer although not difficult has not been a goal of this work. In this chapter some guide lines for using the HOL-UNITY are presented. For a complete understanding of this chapter knowledge of the HOL system is required. However, in order to support understanding the examples in HOL-UNITY notation, these examples are related by page references to their respective presentation in UNITY. Using UNITY as described in [CM88] an appropriate state space of a specification may simply be assumed. However, the mechanized UNITY theory requires for each specification a formal definition of the state space needed to represent the objects and a representation of a program as a list of state transitions in which every state transition represents a UNITY assign statement. Hence to use HOL-UNITY, these extra definitions must be elaborated and defined explicitly. The next section describes in general terms how a state and how the transformation from usual UNITY program notation into state transitions may be defined for any UNITY specification. These methods are then applied in three examples. The presentation is mainly in the notation used earlier, since the pure HOL examples are also found as a UNITY contribution to the HOL system. Section 2.2 explains how to make a composed specification. Section 2.3 presents a method for proving the specified properties satisfied by the given program. And the example shows how it is possible to prove derived program properties by assuming some of the properties satisfied. Section 2.4 is a complete example on how to specify a 2-Arbiter and user component by mutually assuming certain properties satisfied by the environment. It is proved that the presented 2-Arbiter program Arb satisfies the environment dependent properties. This example further presents a method towards automating the proof of the basic UNITY properties unless, stable and ensures.

2.1 Defining State and Program

As explained, HOL-UNITY requires a definition of the state representing the variables in a UNITY specification and a state transition representation of a program. This section presents a method for defining the state and program representation. Every UNITY specification consists of a set of safety- and progress properties that are to be satisfied. These properties are expressed as relations between ordered state dependent predicates. The ordering is given by the state transitions possible by the statements of the UNITY program which satisfies the given properties. If only general safety- and progress properties are specified, the state of the specification may often be defined as the undefined polymorphic type *. Most specifications however describe properties between objects or variables that must be satisfied by the specified system. Since such a system is always assumed to contains finitely many individual objects or variables, it is always possible to define an enumerated type which represents all individuals in a specification. The state of the system may then be defined by the union of mapping every individual onto its value. However, to define a type of this state, the value domain in the mapping must be the union type of all value types given by the individuals. Formally, let

Ind_{tp} = Ind_{rep1} | Ind_{rep2} | ... | Ind_{repn}

be the type representing all individuals. And let

V al_{tp} = V al_{tp1} ⋃ V al_{tp2} ⋃ ... ⋃ V al_{tpn}

be the union type of all individuals value types. Then the state is defined as by the type

State_{tp} = Ind_{tp} →V al_{tp}

An individual Ind_{i} is then defined by the state dependent value

Ind_{i} = λσ:State_{tp}. s−V al_{tpi} (σ Ind_{repi})

notice that the value type of Ind_{i} is explicitly selected. In this way it is also possible to represent any kind of individuals, tex. an indexed by choosing the appropriate index value type.

Other state representations are possible like tuples [BA90], but for the present, the mapping method seems to be the most convenient. The specification of a UNITY program has to be transformed into a list of state transitions to fit into HOL-UNITY. The basic idea of the transformation may be explained by the example of a simple assignment of a variable v to the value of a conditional expression. The value of v is left unchanged if the condition in the expression evaluates to false otherwise v will have the value of the expression after the assignment. Let the example assignment be:

v := expr if bool-expr

in which bool-expr and expr are state dependent values. The assignment is then transformed into the equivalent state transition:

λσ : State_{tp}. (λv′. [[bool-expr]]_{σ} ∧ (v = v′) → [[expr]]_{σ} | [[v′]]_{σ}) | σ

More details on the program representation as lambda expressions are described in [And92]. Here is just noticed that the shown representations of state and programs as state transitions are easily written in HOL notation as will be seen in the following examples.

This completes the introduction on how to meet requirements of the HOL-UNITY system. The following three examples intends to elaborate the application of the system as explained above.

2.2 Mutual Exclusion

The intention of this example is to illustrate how one may specify and compose specifications using the HOL-UNITY theorem prover. The example is similar to the one found in ([CM88], pg. 168-170). However, whereas the example in [CM88] is informal at certain points, the example presented here is a complete rigorous specification using HOL-UNITY notation. This includes beside the specification as found in [CM88] the definition of types, state and proofs of all used properties. The full HOL-UNITY details of the example may be found as part of the HOL-UNITY package distributed together with the HOL system. The chosen example describes a version of the mutual exclusion problem. The formal specification of the problem is given in two parts:

• Users part, called User

• Shared resource part, G

of which every part again has a conditional and unconditional part. From the specified properties, new properties of the composed system are derived using the composition rules valid in HOL-UNITY.

To make the example self contained, a short description of the mutual exclusion problem is informally given. Next the specification is given as presented in [CM88], and finally the complete formal specification using HOL-UNITY is given followed by proofs of composed properties derived as consequences of the two specified parts of the system.

2.2.1 Introduction

Informally, a simple version of the mutual exclusion problem may be explained as follows. A user u making use of the shared resource G may be viewed as being either: EATING, THINKING, or HUNGRY, depending on whether it has got the resource, does not need it, or is waiting for it. Maintaining this picture of a user u, a HUNGRY user u asks G to get the resource. Unfortunately, the shared resource may only be used by a single EATING user u at a time, but it is assumed that the resource allocating is fair such that a HUNGRY user u will get the resource when possible and in a fair way. If no user is EATING, a HUNGRY user gets the resource immediately, otherwise the user has to wait until another user already EATING finishes his dining. User’s do have a finite stomach capacity. Hence, an EATING user u will become satisfied after a while and hence THINKING again. As expected, THINKING user’s may become

HUNGRY again.

This means that the behavior of a user u follows the rules:

• A THINKING user u may become HUNGRY

• A HUNGRY user u eventually becomes EATING

• An EATING user u becomes satisfied after a while of eating and then THINKING again.

Additionally, once a user has become HUNGRY he will stay HUNGRY until it will be

EATING.

From this description, it is evident that the following equivalences hold for any user

u:

   ¬(u = THINKING) = (u = HUNGRY) ∨ (u = EATING) (EQ1)
   ¬(u = HUNGRY) = (u = EATING) ∨ (u = THINKING) (EQ2)
   ¬(u = EATING) = (u = THINKING) ∨ (u = HUNGRY) (EQ3)

Further, the resource allocator guarantees that if an EATING user u becomes satisfied within finite time then any HUNGRY user u will eventually get the shared resource. The description above may be viewed as two parts of a total system. The one consists of the user’s and the other of the resource allocator. Obtaining this view, a specification may be formally given in UNITY.

2.2.2 UNITY Specification

In [CM88], the specification of the above given behavior is given using the terminology that user’s are represented by a set of user’s u in the component User and the resource allocator by the component G. The specification of the properties are here given by:

Properties given for a User component

∀u : (thinking u) unless (hungry u) in User (U1)
∀u : (hungry u) stable  in User (U2)
∀u : (eating u) unless (thinking u) in User (U3)

Properties given for a G component

∀u : (thinking u) stable in G (G1)
∀u : ¬(thinking u) stable in G (G2)
∀u : (eating u)  stable in G (G3)
∀u : ¬(eating u) stable in G (G4)

Conditional G Properties

∀u_{i} u_{j} IC : ¬(u_{i} = u_{j}) ⇒

¬((eating u_{i}) ∧ (eating u_{j})) invariant in (IC, G) (CG1)

Conditional User Properties

∀u G : (CG1) ⇒ (eating u) leadsto (thinking u) in User (CU1)

Properties for the Composed System (User [] G)

∀u_{i} u_{j} IC : ¬(u_{i} = u_{j}) ⇒

¬((eating u_{i}) ∧_{∗} (eating u_{j})) invariant in (IC, (User [] G)) (CS1)
∀u : (hungry u) leadsto (eating u) in (User [] G)  (CS2)

Proof of Derived Properties

From the specification of User and G we may prove some derived properties of the composed system. These proofs may also be found in [CM88]).

The first property we prove is a property of User:

∀u : ¬(eating u) stable in User (thm1)

proof:

∀u : (thinking u) unless (hungry u) in User

from specification of User  (1)

∀u : (hungry u) stable in User

from specification of User  (2)

∀u : ((thinking u) ∨_{∗} (hungry u)) unless (false) in User

applying cancellation to (1) and (2)  (3)

∀u : ((thinking u) ∨_{∗} (hungry u)) = ¬(eating u)

any user u is in one of three states  (4)

∀u : ¬(eating u) stable in User

from (3) and (4)  (thm1)

Next we prove a property of the composed system (User [] G):

∀u : (thinking u) unless (hungry u) in (User [] G) (thm2)

proof:

∀u : (thinking u) unless (hungry u) in User

from specification of User  (1)

∀u : (thinking u) stable in G

from specification of G  (2)

∀u : (thinking u) unless (hungry u) in (User [] G)

union theorem on (1) and (2)  (thm2)

Then we prove another property of the composed system (User [] G):

∀u : (hungry u) unless (eating u) in (User [] G) (thm3)

proof:

∀u : (hungry u) stable in User

from specification of User  (1)

∀u : ¬(thinking u) stable in G

from specification of G  (2)

∀u : ¬(thinking u) = ((hungry u) ∨_{∗} (eating u))

any user u is in one of three states  (3)

∀u : ((hungry u) ∨_{∗} (eating u)) stable in G

from (2) and (3)usingsubstitution  (4)

∀u : (hungry u) unless ¬(hungry u) in G

from the unless antireflexivity rule  (5)

∀u : (hungry u) unless (eating u) in G)

conjunction on (4) and (5)  (6)

∀u : (hungry u) unless (eating u) in (User [] G)

union theorem on (1) and (6)  (thm3)

And finally we prove property:

∀u : (eating u) unless (thinking u) in (User [] G) (thm4)

of the composed system. proof:

∀u : (eating u) unless ¬(thinking u) in User

from the specification of User  (1)

∀u : (eating u) stable in G

from specification of G  (2)

∀u : (eating u) unless (thinking u) in (User [] G)

union theorem on (1) and (2)  (thm4)

This ends the description in UNITY. The given specification will now be defined in the HOL-UNITY notation and the derived proofs are proven within the mechanized HOL-UNITY theorem proving system.

2.2.3 Specification in HOL-UNITY

To make a specification in the HOL-UNITY system, we need to define a new uniquely named theory to avoid collapse with existing theories. Assuming we may use the theory name example01, we remove a potentially old example theory:

system `/bin/rm example01.th`;;

Now the UNITY theories may be loaded into the HOL system:

loadt`l_unity`;;

Hence from now on, we are working in HOL-UNITY. Open a new theory named example01 for elaborating the UNITY example.

new_theory`example01`;;

Now we are ready to start the work on the example.

To make the specification in the HOL-UNITY notation, we must explicitly define a state for book keeping of the current activity of all users u in the User component. As mentioned a user activity in any state may be asked by the predicates eating, thinking, and hungry which takes a user u as argument and returns the boolean value of the respective predicate in a given state. Notice that all UNITY names and terms are written as names and terms in HOL-UNITY notation. To reflect the given description in the HOL-UNITY specification, the type of the state may be defined as a mapping from user’s u onto one of their three possible current activities. Hence, the state may be represented as a function from some unspecified type (i.e. the polymorphic type *) of the user to a dine type representing the actual activity in a given state:

   s:*->dine

in which the dine type may be expressed by an enumerated type:

   dine = EATING | THINKING | HUNGRY

The state definition is a necessity to meet the requirements of a HOL-UNITY specification. But as will be seen in a later example, we may choose other state representations more natural when working with programs.

Defining the Type dine in HOL

In the current HOL system, enumerated types like dine is best defined by using the type definition package [Mel88]. The function define type may be used for defining types:

let dine_Axiom = define_type `dine_Axiom` `dine = EATING | THINKING | HUNGRY`;;

It returns the theorem:

dine_Axiom =
|- !e0 e1 e2.
    ?! fn. (fn EATING = e0) /\ (fn THINKING = e1) /\ (fn HUNGRY = e2)

expressing that for any values e0, e1, e2 of some unspecified but equal type there exists a unique function fn which when applied to one of the three dine values EATING, THINKING, HUNGRY is equal to the respectively chosen values e0, e1, e2. To prove properties of this type we may conveniently introduce an induction theorem for the dine type. This may be defined by:

let dine_Induct = prove_induction_thm dine_Axiom;;

The HOL system uses tactics as a tool for facilitate the proving. Hence, we define a tactic supporting use of the induction theorem:

let dine_INDUCT_TAC = INDUCT_THEN dine_Induct ASSUME_TAC;;

Now we are ready to define the state predicates for expressing the activity of user’s.

Defining the dine Predicates

First the eating predicate. The predicate takes a user u as arguments and returns a state abstracted predicate which ask whether the given user u is EATING in state

s.
let eating = new_definition
   (`eating`,
    "eating (u:*) = (\s:*->dine. (s u) = EATING)");;

The predicates thinking and hungry are defined similarly.

let thinking = new_definition
(`thinking`,
 "thinking (u:*) = (\s:*->dine. (s u) = THINKING)");;
let hungry = new_definition
(`hungry`,
 "hungry (u:*) = (\s:*->dine. (s u) = HUNGRY)");;

We may now prove the needed equalities EQ1, EQ2, EQ3 between the predicates

thinking, eating, hungry.

Equalities between dine Predicates

To prove the needed properties, we must have some additionally information about the type, as expressed above. From the dine Axiom we get two theorems:

let exists_dine_thm1 = prove_rec_fn_exists dine_Axiom
   "(f EATING = T) /\ (f THINKING = F) /\ (f HUNGRY = F)";;
let exists_dine_thm2 = prove_rec_fn_exists dine_Axiom
   "(f EATING = F) /\ (f THINKING = T) /\ (f HUNGRY = F)";;

Now we are able to prove some trivial theorems about the type dine, which are needed to prove the used equalities in the example.

We need to know that all dine values are distinct. Unfortunately this is not supported by the current version of the type package. We may prove this knowledge by using the selected theorems exists dine thm1, exists dine thm2. An example on how to prove this is given:

let dine_thm1 = TAC_PROOF
(([], "~(EATING = THINKING)"),
DISCH_TAC THEN
ASSUME_TAC exists_dine_thm1 THEN
UNDISCH_TAC "?f. (f EATING = T) /\ (f THINKING = F) /\ (f HUNGRY = F)" THEN
ASM_REWRITE_TAC [] THEN
REPEAT STRIP_TAC THEN
RES_TAC);;

Having proven all possible combinations of different dine values, we may prove the theorem:

let dine_thm0 = TAC_PROOF
(([],
"~(EATING   = THINKING) /\ ~(THINKING   = EATING) /\
 ~(EATING   = HUNGRY)   /\ ~(HUNGRY     = EATING) /\
 ~(THINKING = HUNGRY)   /\ ~(HUNGRY     = THINKING)"),
REWRITE_TAC [dine_thm1;dine_thm2;dine_thm3;
             dine_thm4;dine_thm5;dine_thm6]);;

Having proven dine thm0, it is possible to prove the following equality theorem informally stated above as (EQ3):

let dine_thm7 = TAC_PROOF
  (([],
   "!u:dine. ~(u = EATING) = ((u = THINKING) \/ (u = HUNGRY))"),
   dine_INDUCT_TAC THENL
     [REWRITE_TAC [DE_MORGAN_THM;dine_thm0];
      REWRITE_TAC [DE_MORGAN_THM;dine_thm0];
      REWRITE_TAC [DE_MORGAN_THM;dine_thm0]]);;

In the above proving we used the equality:

   ~eating u = thinking u \/ hungry u

was used.

This may be proven by first deriving the following theorem from theorem dine thm7:

   !u s. ~(s u = EATING) = (s u = THINKING) \/ (s u = HUNGRY)
let dine_thm8 = GEN "u:*" (GEN "s:*->dine" (SPEC "(s:*->dine) u" dine_thm7));;

Theorem dine thm8 may now be used for proving the wanted inequality valid:

let dine_thm9 = TAC_PROOF
  (([], "!u:*. (~* (eating u)) = ((thinking u) \/* (hungry u))"),
   REWRITE_TAC [eating;thinking;hungry] THEN
   REWRITE_TAC [~*;\/*] THEN
   CONV_TAC (DEPTH_CONV BETA_CONV) THEN
   GEN_TAC THEN
   STRIP_ASSUME_TAC (MK_ABS (SPEC "u:*" dine_thm8)));;

The equality:

   ~thinking u = hungry u \/ eating u

was also used, and is proven in a similar way.

This completes the introductory work needed in order to establish the state environment for the specification and the used inequalities for proving the properties derived from the specification.

The Property Specification

The method used here is an attempt to bind specified properties to a certain component. This way of specifying may be changed if a better idea turns up.

As specified above we define the presented properties but now as HOL-UNITY properties. The defined properties are given names corresponding to the component of which they belong.

Specifying Properties given for the user component

Specifying the properties (U1), (U2) and (U3):

let user_safe1 = new_definition (`user_safe1`,
   "user_safe1 user = !u:*. ((thinking u) UNLESS (hungry u)) user");;
let user_safe2 = new_definition (`user_safe2`,
   "user_safe2 user = !u:*. (hungry u) STABLE user");;
let user_safe3 = new_definition (`user_safe3`,
   "user_safe3 user = !u:*. ((eating u) UNLESS (thinking u)) user");;

Specifying Properties given for the G component

Specifying the properties (G1), (G2), (G3) and (G4):

let G_safe1    =  new_definition (`G_safe1`,
   "G_safe1 G = !u:*. (thinking u) STABLE G");;
let G_safe2    =  new_definition (`G_safe2`,
   "G_safe2 G = !u:*. (~*(thinking u)) STABLE G");;
let G_safe3    =  new_definition
  (`G_safe3`, "G_safe3 G = !u:*. (eating u) STABLE G");;
let G_safe4    =  new_definition
  (`G_safe4`, "G_safe4 G = !u:*. (~* (eating u)) STABLE G");;

Specifying Conditional G Properties component

Specifying the conditional property (CG1):

let G_cond =  new_definition (`G_cond`,
   "G_cond G IC = !(ui:*) uj. ~(ui = uj) ==>
                (~*((eating ui) /\* (eating uj))) INVARIANT (IC, G)");;

Specifying Conditional user Properties component

Specifying the conditional property (CU1):

let user_live1 = new_definition (`user_live1`,
   "user_live1 user IC =
      !(u:*) (G:((*->dine)->(*->dine))list).
          G_cond G IC ==> ((eating u) LEADSTO (thinking u)) user");;

These were the properties specified for each of the components user and G. Now the wanted properties that must be satisfied by the composed system are given.

Specifying Properties for the Composed System

Specifying the composed properties (CS1) and (CS2):

let comp_safe1 = new_definition (`comp_safe1`,
"comp_safe1 G user IC =
 !(ui:*) uj. ~(ui = uj) ==>
 (~*((eating ui) /\* (eating uj))) INVARIANT (IC, (APPEND user G))");;
let comp_live1 = new_definition (`comp_live1`,
"comp_live1 G user =
   !u:*. ((hungry u) LEADSTO (eating u)) (APPEND user G)");;

Finally, we prove the derived properties as presented above, but this time using the HOL-UNITY theorem prover.

Proving Derived Properties of the Specification

Given properties user safe1, user safe2, user safe3, we may prove that all users satisfy:

!user u. user_safe1 user /\ user_safe2 user /\ user_safe3 user ==>
         ~eating u is stable in user

Notice, that the assumed properties are given explicitly, since the HOL-UNITY system does not support an environment of specified properties, as one may conveniently do by manually proving.

This proof is similar to the proof of (thm1) on page 13.

let user_thm1 = TAC_PROOF
(([], "!user (u:*).
        user_safe1 user /\ user_safe2 user /\ user_safe3 user ==>
            (~* (eating u)) STABLE user"),
REPEAT GEN_TAC THEN
REWRITE_TAC [user_safe1;user_safe2;user_safe3] THEN
REPEAT STRIP_TAC THEN
ASSUME_TAC (SPEC "u:*" (ASSUME "!u:*. (hungry u) STABLE user")) THEN
ASSUME_TAC
    (SPEC "u:*" (ASSUME "!u:*. ((thinking u) UNLESS (hungry u)) user")) THEN
UNDISCH_TAC "(hungry (u:*)) STABLE user" THEN
REWRITE_TAC [STABLE] THEN
DISCH_TAC THEN
ASSUME_TAC (UNDISCH_ALL (SPECL
     ["((thinking (u:*)) UNLESS (hungry u))user";
      "((hungry (u:*)) UNLESS FALSE)user"]
      AND_INTRO_THM)) THEN
ASSUME_TAC (UNDISCH_ALL (SPECL
     ["thinking (u:*)";"hungry (u:*)";
      "FALSE:(*->dine)->bool";"user:((*->dine)->(*->dine))list"]
      UNLESS_thm8)) THEN
UNDISCH_TAC "(((thinking (u:*)) \/* (hungry u)) UNLESS FALSE)user" THEN
REWRITE_TAC [SYM (SPEC_ALL dine_thm9)]);;

Given properties user safe1 and G safe1, we may prove that all user’s u and G components satisfy:

!user G u. user_safe1 user /\ G_safe1 G ==>
         (thinking u) unless (hungry u) in (user [] G)

in the composed system.

This proof is similar to the proof of (thm2) on page 14.

let comp_thm1 = TAC_PROOF
(([], "!user G (u:*). user_safe1 user /\ G_safe1 G ==>
            ((thinking u) UNLESS (hungry u)) (APPEND user G)"),
REPEAT GEN_TAC THEN
REWRITE_TAC [user_safe1;G_safe1] THEN
REPEAT STRIP_TAC THEN
ASSUME_TAC (SPEC_ALL (ASSUME
     "!u:*. ((thinking u) UNLESS (hungry u))user")) THEN
ASSUME_TAC (SPEC_ALL (ASSUME "!u:*. (thinking u) STABLE G")) THEN
ASSUME_TAC (UNDISCH_ALL (SPECL
    ["((thinking (u:*)) UNLESS (hungry u))user";
     "(thinking (u:*)) STABLE G"]
     AND_INTRO_THM)) THEN
REWRITE_TAC [UNDISCH_ALL (SPECL
    ["thinking (u:*)";"hungry (u:*)";"user:((*->dine)->(*->dine))list";
     "G:((*->dine)->(*->dine))list"] COMP_UNITY_cor2)]);;

Given properties user safe2 and G safe2, we may prove that all user’s and G components satisfy:

!user G u. user_safe2 user /\ G_safe2 G ==>
         (hungry u) unless (eating u) in (user [] G)

for any user u in the composed system.

The rewriting of boolean expressions are tedious. For a future use, we need to invent something better.

This proof is similar to the proof of (thm3) on page 14.

let comp_thm2 = TAC_PROOF
(([], "!(u:*) user G. user_safe2 user /\ G_safe2 G ==>
                  ((hungry u) UNLESS (eating u)) (APPEND G user)"),
REWRITE_TAC [user_safe2;G_safe2] THEN
REPEAT STRIP_TAC THEN
ASSUME_TAC (SPEC_ALL (ASSUME "!u:*. (~*(thinking u)) STABLE G")) THEN
ASSUME_TAC (SPEC_ALL (ASSUME "!u:*. (hungry u) STABLE user")) THEN
UNDISCH_TAC "(~*(thinking (u:*))) STABLE G" THEN
REWRITE_TAC [dine_thm12] THEN
ASSUME_TAC (SPECL
     ["hungry (u:*)";"G:((*->dine)->(*->dine))list"] UNLESS_thm2) THEN

REWRITE_TAC [STABLE] THEN
ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
DISCH_TAC THEN
ASSUME_TAC (UNDISCH_ALL (SPECL
     ["((hungry (u:*)) UNLESS (~*(hungry u)))G";
      "(((eating (u:*)) \/* (hungry u)) UNLESS FALSE)G"]
      AND_INTRO_THM)) THEN
ASSUME_TAC (UNDISCH_ALL (SPECL
     ["hungry (u:*)";"~* (hungry (u:*))";
      "(eating (u:*)) \/* (hungry u)";"FALSE:(*->dine)->bool";
      "G:((*->dine)->(*->dine))list"] UNLESS_thm4)) THEN
UNDISCH_TAC
      "(((hungry u) /\* ((eating u) \/* (hungry u))) UNLESS
        ((((hungry (u:*)) /\* FALSE) \/*
         (((eating u) \/* (hungry u)) /\* (~*(hungry u)))) \/*
        ((~*(hungry u)) /\* FALSE))) G" THEN
REWRITE_TAC [AND_FALSE_lemma] THEN
REWRITE_TAC [OR_FALSE_lemma] THEN
ONCE_REWRITE_TAC [SPECL
     ["FALSE:(*->dine)->bool";
      "((eating (u:*)) \/* (hungry u)) /\* (~*(hungry u))"]
      OR_COMM_lemma] THEN
REWRITE_TAC [OR_FALSE_lemma] THEN
ONCE_REWRITE_TAC [SPECL
     ["hungry (u:*)";"eating (u:*)";"hungry (u:*)"]
      AND_OR_DISTR_lemma] THEN
REWRITE_TAC [AND_AND_lemma] THEN
ONCE_REWRITE_TAC [SPECL
     ["hungry (u:*)";"eating (u:*)"] AND_COMM_lemma] THEN
REWRITE_TAC [P_AND_Q_OR_Q_lemma] THEN
ONCE_REWRITE_TAC [AND_COMM_lemma] THEN
ONCE_REWRITE_TAC [SPECL
     ["~* (hungry (u:*))";"eating (u:*)";"hungry (u:*)"]
      AND_OR_DISTR_lemma] THEN
ONCE_REWRITE_TAC [AND_COMM_lemma] THEN
REWRITE_TAC [P_AND_NOT_P_lemma] THEN
REWRITE_TAC [OR_FALSE_lemma] THEN
DISCH_TAC THEN
ASSUME_TAC (SPECL
     ["eating (u:*)";"~* (hungry (u:*))"]
      SYM_AND_IMPLY_WEAK_lemma) THEN
ASSUME_TAC (UNDISCH_ALL (SPECL
     ["((hungry (u:*)) UNLESS ((eating u) /\* (~*(hungry u))))G";
      "!s:*->dine. ((eating u) /\* (~*(hungry u)))s ==> eating u s"]
      AND_INTRO_THM)) THEN
ASSUME_TAC (UNDISCH_ALL (SPECL
     ["hungry (u:*)";"(eating (u:*)) /\* (~*(hungry u))";
      "eating (u:*)";"G:((*->dine)->(*->dine))list"]
      UNLESS_thm3)) THEN
ASSUME_TAC (UNDISCH_ALL (SPECL
     ["((hungry (u:*)) UNLESS (eating u))G";
      "(hungry (u:*)) STABLE user"]
      AND_INTRO_THM)) THEN
STRIP_ASSUME_TAC (UNDISCH_ALL (SPECL

        ["hungry (u:*)";"eating (u:*)";"G:((*->dine)->(*->dine))list";
         "user:((*->dine)->(*->dine))list"] COMP_UNITY_cor2)));;

Given properties user safe3 and G safe3, we may prove that all users and G components satisfy:

  !user G u. user_safe3 user /\ G_safe3 G ==>
               (eating u) unless (thinking u) in (user [] G)

for any user u in the composed system.

This proof is similar to the proof of (thm4) on page 14.

let comp_thm3 = TAC_PROOF
  (([],
   "!user G (u:*). user_safe3 user /\ G_safe3 G ==>
                  ((eating u) UNLESS (thinking u)) (APPEND user G)"),
   REWRITE_TAC [user_safe3;G_safe3] THEN
   REPEAT STRIP_TAC THEN
   ASSUME_TAC (SPEC_ALL (ASSUME "!u:*. (eating u) STABLE G")) THEN
   ASSUME_TAC (SPEC_ALL (ASSUME
        "!u:*. ((eating u) UNLESS (thinking u))user")) THEN
   ASSUME_TAC (UNDISCH_ALL (SPECL
        ["((eating (u:*)) UNLESS (thinking u))user";
         "(eating (u:*)) STABLE G"]
         AND_INTRO_THM)) THEN
   STRIP_ASSUME_TAC (UNDISCH_ALL (SPECL
        ["eating (u:*)";"thinking (u:*)";"user:((*->dine)->(*->dine))list";
         "G:((*->dine)->(*->dine))list"] COMP_UNITY_cor2)));;

This ends the example on the mutual exclusion problem.

2.3 The readers/writers Problem

The purpose of this example is to show how programs may be represented in the HOL-UNITY theorem prover and how it is proven that a given program meets its property specification.

A subgoal is also to show how one may represent and work with programs containing variables of different type and represent such variables all having the natural number type.

The section first presents the program and some of the properties using the notation [CM88], then the specification and proofs in HOL-UNITY notation are given. The HOL-UNITY presentation simulates a HOL session. Hence, this example may be used as user’s guideline for working with the HOL-UNITY theorem proving system.

2.3.1 Introduction

The chosen example is a slightly modified version of the example page 139-140 [CM88]. It is a small (rudimentary) example of the well known readers/writers problem. The given program has the important property that it guarantees progress for writers. Notice that the example still has to be completed with the proof of the two (U7) and (U8) program properties, but for the purpose of the example it is sufficient. To ease proving, one statement was changed in the program given on page 139 [CM88]. The boolean variable B is represented as a variable having the state dependent value 0 (zero) for FALSE and the value 1 for TRUE. The modification was made in the assignment {set-b} such that this statement assigns the variable B to 1 if the condition is true and 0 otherwise. Hence, also the statement {startwrite} had to be changed to assign the value 0 to B. The representation of the variable B makes the state definition of the program simpler, since all variables are now of type natural numbers.

2.3.2 A readers/writers Program with writers Progress

The program implementing the required behavior of readers and writers:

program User

declare

B, NR, NW , NQ  : number

initially

B, NR, NW , NQ  = 0, 0, 0, 0

always

t  = N − (NR + N ∗ NW)

assign

{startread} NR  := NR + 1  if t ≥ 1 ∧ ¬(B = 1)
[] {endread}  NR  := NR − 1
[] {startwrite} NW , NQ, B := NW + 1, NQ − 1, 0 if t ≥ N ∧ NQ ≥ 0
[] {endwrite}  NW  := NW − 1
[] {set −b}  B  := 1  if NQ > 0
∼ 0

end

Some important properties that must be satisfied by the User program:

∀k : (NR = k ∧ k > 0) leadsto ¬(NW = 1) in User  (U4)
(NQ > 0) ensures (NW = 1 ∨ B = 1) in User  (U7)
(B = 1 ∧ NR = 0) ensures (NW = 1) in User  (U8)
∀k : (B = 1 ∧ NR = k ∧ k > 0) unless (B = 1 ∧ NR < k) in User (U9)

These are later proven valid during the session using the HOL-UNITY system.

Using the presented properties, it is possible to prove that:

(NQ > 0) leadsto (NW = 1) in User  (U5)

proof:

∀k : (B = 1 ∧ NR = k ∧ k > 0) leadsto (B = 1 ∧ NR < k) in User

using PSP theorem on (U4) and (U9)  (1)

(B = 1) leadsto (B = 1 ∧ NR = 0) in User

applying induction on (1)  (2)

(B = 1) leadsto (NW = 1) in User

transitivity on (2) and (U8)  (3)

(NQ > 0) leadsto (NW = 1) in User

cancellation on (U7) and (3)  (U5)

Now, we want to prove that theorem (U5) holds for the User program by using the HOL-UNITY. This means, assuming (U4) as done in the example [CM88] we must prove that (U7), (U8) and (U9) holds for the program User. Having proved these properties, we may prove that assuming (U4)) the property (U5) is satisfied by User.

2.3.3 Verifying User Properties using HOL-UNITY

Like before, we need to define a new uniquely named theory to avoid collapse with existing theories. Assuming we may use the theory name example02, we remove a potentially old example theory:

system `/bin/rm example02.th`;;

Load the UNITY theories into the HOL system:

loadt`l_unity`;;

Hence from now on, we are working in HOL-UNITY. Now, opening a new theory named example02 for elaborating the UNITY example

new_theory`example02`;;

we are ready to start working on the example. As mentioned before, this example will not be complete, but only contain enough details and proofs to give an introductory understanding of how to work with the current HOL-UNITY prototype system. First we define a HOL representation of the User program variables, the we prove a lemma needed for the defined variables, next we define a representation of a UNITY program, and finally we define the specified program. We prove that one of the assumed safety properties (U9) and is really satisfied by the given program. From this and assuming (u4), (U7) and (U8) we end the example by proving the progress property (U10). These steps in the example are supposed to represent a way of working with the present HOL-UNITY prototype system.

2.3.4 Defining a Program Representation

In this section variables name are written with capital letters NAME. To make the specification in HOL-UNITY of a program, we need to define a representation of the program variables and the statements in the program must be defined as state transition functions.

Program Variables

We start by defining an enumerated like type representing the variables NR, NW, NQ and B as named constants in the program.

let Vtype_Axiom = define_type `Vtype_Axiom` `Vtype = NR | NW | NQ | B`;;

To prove the needed properties, we must have some additionally information about the type. We prove that a function f exists, which maps the enumerated constants

NR, NW, NQ, B onto the values 0, 1, 2, 3:
let exists_Vtype_thm = prove_rec_fn_exists Vtype_Axiom
      "(f NR = 0) /\ (f NW = 1) /\ (f NQ = 2) /\ (f B = 3)";;

Now we are able to prove the trivial Vtype theorem, that all program variables represented by the enumerated constants NR, NW, NQ, B are distinct.

let Vtype_thm1 = TAC_PROOF
  (([],

   "~(NR = NW) /\ ~(NW = NR) /\ ~(NR = NQ) /\ ~(NQ = NR) /\
    ~(NR =  B) /\ ~(B  = NR) /\ ~(NW = NQ) /\ ~(NQ = NW) /\
    ~(NW =  B) /\ ~(NQ = NW) /\ ~(NQ =  B) /\ ~(B  = NQ)"),
   STRIP_ASSUME_TAC exists_Vtype_thm THEN
   REPEAT STRIP_TAC THEN
   POP_ASSUM (\thm. MP_TAC
     (CONJ (REWRITE_RULE [thm] (ASSUME "(f:Vtype->num) NR = 0"))
     (CONJ (REWRITE_RULE [thm] (ASSUME "(f:Vtype->num) NW = 1"))
     (CONJ (REWRITE_RULE [thm] (ASSUME "(f:Vtype->num) NQ = 2"))
           (REWRITE_RULE [thm] (ASSUME "(f:Vtype->num) B  = 3")))))) THEN
   ASM_REWRITE_TAC [num_CONV "3";num_CONV "2";num_CONV "1"] THEN
   REWRITE_TAC [INV_SUC_EQ] THEN
   REWRITE_TAC [NOT_SUC] THEN
   REWRITE_TAC [ONCE_REWRITE_RULE [EQ_SYM_EQ] NOT_SUC]);;

The enumerated constants and the proven property that all variables are distinct enables us to represent the program variables of the User program. But we still need a representation of program statements. A method which suits the semantic of UNITY programs are given in the next section.

Program Representation

In order to be able to define a UNITY program as a set (list representation) of state transitions, we need to define every conditional assignment in terms of a state transition function.

Having defined such a function MK COND, we may represent a UNITY program as a list of such functions.

We define the state transition function ST, which updates a variable nm to a value given by the state dependent expression val. The value of val is defined by the old state s. ST returns the state s' that is defined by s' except that the variable nm is given the value of val in the old state s.

let ST = new_definition
  (`ST`, "ST ((nm:Vtype),(val:(Vtype->num)->num)) s s' =
             (\n. (n = nm) => (val s) | (s' n))");;

Both states s and s' are needed, since we want to able to represent a set of updates in which all expressions are evaluated in the state s. The state s' then contains the accumulated updates of variables.

We may now define the function STL, which reflects the state transition as a result of a set (list representation) of assignments by recursively using the ST function for the state transition given by each assignment.

let STL = new_recursive_definition false list_Axiom `STL`
  "(STL (s:Vtype->num) s' [] = s') /\
   (STL s s' (CONS (as:(Vtype#((Vtype->num)->num))) asl) =
                          (STL s (ST as s s') asl))";;

Finally, we represent a UNITY assignment as a conditional state transition MK COND defined by a state dependent enabling condition c and a list of parallel, but interleaved assignments. Actually there is no concept of conditional statements in UNITY (see [CM88] pg 24). However, since side effects are not possible by evaluating expressions in UNITY, we may move the condition of a conditional expression in front of an assignment if there is no optional values in the expression. This presented approach was taken to show how HOL-UNITY may also be used to verify ST (Synchronized Transitions [GGS88]) programs. Using pure UNITY expressions [CM88], no statement enabling condition is present, hence the values val must be represented by state dependent conditional expression values alone. An example of such a conditional expression is found in the representation of the User program Prog in the last MK COND statement representing the set b statement.

let MK_COND = new_definition (`MK_COND`,
   "MK_COND (c, asl) (s:Vtype->num) = ((c s) => (STL s s asl) | s)");;

To complete the description of the program representation we prove that the claimed equivalence between the two representations is actually satisfied. This ends the description on how to represent programs in HOL-UNITY. The wanted program User is defined as Prog in the next section.

Defining the Program User

An additional feature in UNITY is the always definitions. An always definition defines a shorthand for a complicated expression in the program, i.e. such a definition does not have a semantic itself. In HOL-UNITY this feature is achieved in an elegant way by using the possibility of referring to the contents of an ML defined term in another term. We explain this feature by the example:

let v1 = "3 + 7";;
let v2 = "v1 = ^v1 * 2 + 9";;

The result of the term v2 is:

let v2 = "v1 = (3 + 7) * 2 + 9";;

This feature in HOL is obviously equal to the always in UNITY. Hence, we may define t in the User program by:

let t = "\s:Vtype->num. N - ((s NR) + (N * (s NW)))";;

This allows us to define the example program User by:

let Prog =
 "[MK_COND((\s:Vtype->num. (^t s) >= 1 /\ ~((s B) = 1)),
     [NR, (\s. (s NR) + 1)]);
   MK_COND(TRUE, [NR, (\s. (s NR) - 1)]);
   MK_COND((\s. ((^t s) >= N) /\ (s NQ) > 0),
      [(NW, (\s. (s NW) + 1));(NQ, (\s. (s NQ) - 1));(B, (\s. 0))]);
   MK_COND(TRUE, [NW, (\s. (s NW) - 1)]);
   MK_COND(~* (\s. s B = 1), [B,  (\s. (s NQ) > 0 => 1 | 0)])]";;

The reader may convince himself that the program Prog is equal to User.

Now we may prove the properties given in the specification satisfied by the program

Prog.

2.3.5 Proving Program Properties

To make the proving of the program properties easier, we first prove some lemmas. These lemmas are obvious to the reader but unfortunately currently not easy to prove in HOL.

We may prove the following lemmas in HOL. The lemmas are needed in for proving properties satisfied in the specification.

U9_lemma1 = !k. k > 0 ==> (k - 1) < k
U9_lemma2 = !N M. ~((N - M) > N)
U9_lemma3 = !(n:num) m. ((SUC n) - (SUC m)) = (n - m)
U9_lemma4 = !n m. (n - m) < (SUC n)
U9_lemma5 = !(N:num) k. (k > 0) ==> (N > 0) ==> ((N - (k + (N * (s NW)))) < N)
U9_lemma6 = !n m. (n < m) = ~(n >= m)
U9_lemma7 = |- !N k. k > 0 ==> N > 0 ==> ~(N - (k + (N * (s NW)))) >= N

Proving the Program Satisfying a Safety Property

Let us prove that the safety property, labeled U9:

(B = 1) /\ (NR = k) /\ (k > 0) unless (B = 1) /\ (NR < k) in Pr

holds for the defined program Prog.

The property is proven in six steps. 5 proofs, one for each state transition in the program and one proof using the 5 proofs to prove that the property of the entire program holds.

let U9_tr1_thm1 = TAC_PROOF
  (([],
   "!N. (N > 0) ==>
     (!k:num.
      (((\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0))) UNLESS
       ((\s. s B = 1) /\* (\s. s NR < k))) [^startwrite])"),

REPEAT GEN_TAC THEN
REWRITE_TAC [UNLESS;UNLESS_STMT;MK_COND;STL;ST;/\*;\/*;~*;TRUE_DEF] THEN
BETA_TAC THEN
REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC []);;
let U9_tr2_thm1 = TAC_PROOF
(([],
"!N. (N > 0) ==>
  (!k:num.
   (((\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0))) UNLESS
    ((\s. s B = 1) /\* (\s. s NR < k))) [^endwrite])"),
REPEAT GEN_TAC THEN
REWRITE_TAC [UNLESS;UNLESS_STMT;MK_COND;STL;ST;/\*;\/*;~*;TRUE_DEF] THEN
BETA_TAC THEN
REPEAT STRIP_TAC THEN
BETA_TAC THEN
ASM_REWRITE_TAC [Vtype_thm1;ONCE_REWRITE_RULE [EQ_SYM_EQ] Vtype_thm1] THEN
DISJ2_TAC THEN
ACCEPT_TAC (MP (SPEC_ALL U9_lemma1) (ASSUME "k > 0")));;
let U9_tr3_thm1 = TAC_PROOF
(([],
"!N. (N > 0) ==>
  (!k:num.
   (((\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0))) UNLESS
    ((\s. s B = 1) /\* (\s. s NR < k))) [^startread])"),
REPEAT GEN_TAC THEN
REWRITE_TAC [UNLESS;UNLESS_STMT;MK_COND;STL;ST;/\*;\/*;~*;TRUE_DEF] THEN
BETA_TAC THEN
REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC [] THEN
REPEAT COND_CASES_TAC THENL
  [ % 2 Subgoals %
   MP_TAC (REWRITE_RULE
     [ASSUME "(N - (k + (N * (s NW)))) >= N /\ (s NQ) > 0"]
       (MP (MP (SPEC_ALL U9_lemma7) (ASSUME "k > 0"))
           (ASSUME "N > 0"))) THEN
   REWRITE_TAC []
  ;
   ASM_REWRITE_TAC []
  ]);;
let U9_tr4_thm1 = TAC_PROOF
(([],
"!N. (N > 0) ==>
  (!k:num.
   (((\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0))) UNLESS
    ((\s. s B = 1) /\* (\s. s NR < k))) [^endread])"),
REPEAT STRIP_TAC THEN
REWRITE_TAC [UNLESS;UNLESS_STMT;MK_COND;STL;ST;/\*;\/*;~*;TRUE_DEF] THEN
BETA_TAC THEN
REPEAT STRIP_TAC THEN
BETA_TAC THEN

ASM_REWRITE_TAC [Vtype_thm1;ONCE_REWRITE_RULE [EQ_SYM_EQ] Vtype_thm1]);;
let U9_tr5_thm1 = TAC_PROOF
(([],
"!N. (N > 0) ==>
  (!k:num.
   (((\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0))) UNLESS
    ((\s. s B = 1) /\* (\s. s NR < k))) [^set_b])"),
REPEAT STRIP_TAC THEN
REWRITE_TAC [UNLESS;UNLESS_STMT;MK_COND;STL;ST;/\*;\/*;~*;
             TRUE_DEF;FALSE_DEF] THEN
BETA_TAC THEN
REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC []);;

Now we may prove that the property (U9) holds for the given program

let U9 = TAC_PROOF
(([],
"!N. (N > 0) ==>
  (!k:num.
   (((\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0))) UNLESS
    ((\s. s B = 1) /\* (\s. s NR < k))) ^Prog)"),
REPEAT STRIP_TAC THEN
ASM_REWRITE_TAC [UNLESS] THEN
REWRITE_TAC
 [UNDISCH_ALL (REWRITE_RULE [UNLESS] (SPEC_ALL U9_tr1_thm1));
  UNDISCH_ALL (REWRITE_RULE [UNLESS] (SPEC_ALL U9_tr2_thm1));
  UNDISCH_ALL (REWRITE_RULE [UNLESS] (SPEC_ALL U9_tr3_thm1));
  UNDISCH_ALL (REWRITE_RULE [UNLESS] (SPEC_ALL U9_tr4_thm1));
  UNDISCH_ALL (REWRITE_RULE [UNLESS] (SPEC_ALL U9_tr5_thm1))]);;

The claimed theorems (U7) and (U8) may proven in a similar way. Since these two properties are ensures properties, it is necessary to prove both the unless property of the ensures and the existence of a statement which satisfies the transition from a state satisfying the first predicate to one satisfying the last. But apart from this the proving method is equal to the shown for (U9). Hence, assuming we have proven the two properties (U7) and (U8):

let U7 =
"((\s. s NQ > 0) ENSURES ((\s. s NW = 1) \/* (\s. s B = 1))) ^Prog";;
let U8 =
"(((\s. s B = 1) /\* (\s. s NR = 0)) ENSURES ((\s. s NW = 1))) ^Prog";;

satisfied by the program Prog. We may prove (U5) assuming the property (U4):

let U4 =
"!k. (((\s. s NR = k) /\* (\s. k > 0)) LEADSTO (~* (\s. s NR = k))) ^Prog";;

We want to prove the progress property:

(U5)
  |- !N. (N > 0) ==> (U4) /\ (U7) /\ (U8)
       ==> ((\s. s NQ > 0) LEADSTO (\s. s NW = 1)) Prog

satisfied.

To prove this it turns out again that a couple of useful lemmas are needed. In all we prove seven lemmas before we get to the proof of (U5) as presented above. First we prove a simple equivalence.

let U5_lemma1 = TAC_PROOF
(([],
"!s. (((\s. s NR = k) /\*  (\s. k > 0)) /\*
      ((\s. s  B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0)))) s
    =
     ((\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0))) s"),
REWRITE_TAC [/\*] THEN
BETA_TAC THEN
GEN_TAC THEN
EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);;

Since the proof above was valid for all states s we may rewrite the equivalence into one with state abstracted predicates. This lemma will be used to simplify a predicate appearing in the proof of (U5). In proving manually such equivalences are simply assumed satisfied, but using HOL-UNITY they must be proven explicitly.

|- ((\s. s NR = k) /\*  (\s. k > 0)) /\*
  ((\s. s  B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0)))
 =
  (\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0))
let U5_lemma2 = REWRITE_RULE [ETA_AX] (MK_ABS U5_lemma1);;

Another simplifying equivalence is needed. We proceed as before.

let U5_lemma3 = TAC_PROOF
(([],
"!s. (((~*(\s. s NR = k)) /\*
        ((\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0)))) \/*
       ((\s. s B = 1) /\* (\s. (s NR) < k))) s
    =
     ((\s. s B = 1) /\* (\s. (s NR) < k)) s"),
REWRITE_TAC [/\*;\/*;~*] THEN
BETA_TAC THEN
GEN_TAC THEN
EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] THEN
RES_TAC);;

Also this state abstracted equivalence will be used for simplification of an appearing predicate.

|- ((~*(\s. s NR = k)) /\*
((\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0)))) \/*
((\s. s B = 1) /\* (\s. (s NR) < k))
=
(\s. s B = 1) /\* (\s. (s NR) < k)
let U5_lemma4 = REWRITE_RULE [ETA_AX] (MK_ABS U5_lemma3);;

The UNITY leadsto property satisfies that from any valid state abstracted implication we may conclude the leadsto property satisfied for the non-empty program. That is we may deduce:

!p q st Pr. (!s. p s ==> q s) ==> (p LEADSTO q) (CONS st Pr)

We use this deduction rule to prove the next lemma.

|- (((\s. s B = 1) /\* (\s. s NR = 0)) LEADSTO
(((\s. s B = 1) /\* (\s. (s NR) < 0)) \/*
((\s. s B = 1) /\* (\s. s NR = 0))))
(CONS st Pr)
let U5_lemma5 =
(REWRITE_RULE
[(ISPECL ["(\s. s B = 1) /\* (\s. s NR = 0)";
          "(\s. s B = 1) /\* (\s. (s NR) < 0)"] SYM_OR_IMPLY_WEAK_lemma);
 (SPEC_ALL (ISPECL ["(\s. s B = 1) /\* (\s. s NR = 0)"] LEADSTO_thm12))]
   (ISPECL ["(\s. s B = 1) /\* (\s. s NR = 0)";
            "(\s. s B = 1) /\* (\s. s NR = 0)";
            "((\s. s B = 1) /\* (\s. (s NR) < 0)) \/*
             ((\s. s B = 1) /\* (\s. s NR = 0))";
            "CONS (st:(Vtype->num)->(Vtype->num)) Pr"]
            LEADSTO_cor9));;

This lemma will be needed in the proof of the lemma below. Next we prove by induction that the LEADSTO property satisfied for any natural number constant k greater than 0 implies the LEADSTO property satisfied for any natural number constant m.

let U5_lemma6 = TAC_PROOF
(([],
"(!k. (((\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0))) LEADSTO
    ((\s. s B = 1) /\* (\s. (s NR) < k))) (CONS st Pr))
==>
(!m. (((\s. s B = 1) /\* (\s. s NR = m)) LEADSTO
   (((\s. s B = 1) /\* (\s. (s NR) < m)) \/*
    ((\s. s B = 1) /\* (\s. s NR = 0)))) (CONS st Pr))"),
DISCH_TAC THEN
INDUCT_TAC THENL
[
REWRITE_TAC [U5_lemma5]
;

  ACCEPT_TAC (REWRITE_RULE [(REWRITE_RULE
   [GREATER;LESS_0;REWRITE_RULE [TRUE_DEF] AND_TRUE_lemma] (SPEC "SUC m"
     (ASSUME
       "!k. (((\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0))) LEADSTO
             ((\s. s B = 1) /\* (\s. (s NR) < k))) (CONS st Pr)")));
         (ISPECL ["((\s. s B = 1) /\* (\s. (s NR) < (SUC m)))";
                "((\s. s B = 1) /\* (\s. s NR = 0))"]
                 OR_IMPLY_WEAK_lemma)]
     (SPEC_ALL (ISPECL ["(\s. s B = 1) /\* (\s. (s NR) = (SUC m))";
                 "(\s. s B = 1) /\* (\s. (s NR) < (SUC m))";
                 "((\s. s B = 1) /\* (\s. (s NR) < (SUC m))) \/*
                  ((\s. s B = 1) /\* (\s. s NR = 0))";
                 "CONS (st:(Vtype->num)->(Vtype->num)) Pr"]
                 LEADSTO_cor9)))
 ]);;

We use this lemma for proving the next lemma needed in the proof of (U5). Finally we prove by induction on the program size, that the LEADSTO property satisfied for any natural number constant k greater than 0 implies a weakened LEADSTO property satisfied for any natural number constant m and for any program Pr including the empty.

let U5_lemma7 = TAC_PROOF
(([],
"!Pr. (!k. (((\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0))) LEADSTO
           ((\s. s B = 1) /\* (\s. (s NR) < k))) Pr)
   ==>
      (!m. (((\s. s B = 1) /\* (\s. s NR = m)) LEADSTO
           (((\s. s B = 1) /\* (\s. (s NR) < m)) \/*
            ((\s. s B = 1) /\* (\s. s NR = 0)))) Pr)"),
LIST_INDUCT_TAC THENL
 [
  REWRITE_TAC [LEADSTO_thm10]
 ;
  X_GEN_TAC "st:(Vtype->num)->(Vtype->num)" THEN
  REWRITE_TAC [U5_lemma6]
 ]);;

This lemma will be used in the proof of theorem (U5).

Finally we may prove that assuming the properties (U4), (U7) and (U8) the property (U5) is satisfied. Notice that the proof follows the outline given in the specification section on page 25, but we now use the proved lemmas above to avoid the proof being too detailed.

let U5 = TAC_PROOF
(([],
"!N. (N > 0) ==> (^Prog = Pr) ==> ^U4 /\ ^U7 /\ ^U8 ==>
   ((\s. s NQ > 0) LEADSTO (\s. s NW = 1)) ^Prog"),
GEN_TAC THEN
DISCH_TAC THEN
DISCH_TAC THEN
MP_TAC (UNDISCH_ALL (SPEC_ALL U9)) THEN

   ASM_REWRITE_TAC [] THEN
   REPEAT STRIP_TAC THEN
   IMP_RES_TAC LEADSTO_thm0 THEN
   ASSUME_TAC (GEN "k:num" (REWRITE_RULE
    [U5_lemma2;U5_lemma4] (REWRITE_RULE
      [ASSUME "!k.
       (((\s. s NR = k) /\* (\s. k > 0)) LEADSTO (~*(\s. (s NR) = k))) Pr";
       ASSUME "!k.
       (((\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0))) UNLESS
        ((\s. s B = 1) /\* (\s. (s NR) < k))) Pr"] (ISPECL
          ["(\s. s NR = k) /\* (\s. k > 0)";"~*(\s:Vtype->num. (s NR) = k)";
           "(\s. s B = 1) /\* ((\s. s NR = k) /\* (\s. k > 0))";
           "(\s. s B = 1) /\* (\s. (s NR) < k)";
           "Pr:((Vtype->num)->(Vtype->num))list"] LEADSTO_thm29)))) THEN
   ASSUME_TAC (UNDISCH_ALL (SPEC_ALL U5_lemma7)) THEN
   ASSUME_TAC (UNDISCH_ALL (BETA_RULE (ISPECL
    ["\s. s B = 1";"(\s. s B = 1) /\* (\s. s NR = 0)";
     "Pr:((Vtype->num)->(Vtype->num))list";"\s:Vtype->num. s NR"]
     (REWRITE_RULE [EQmetric;LESSmetric] LEADSTO_thm32)))) THEN
   IMP_RES_TAC LEADSTO_thm1 THEN
   IMP_RES_TAC LEADSTO_thm28 THEN
   ACCEPT_TAC (REWRITE_RULE [OR_OR_lemma] (ASSUME
    "((\s. (s NQ) > 0) LEADSTO ((\s. s NW = 1) \/* (\s. s NW = 1)))Pr")));;

To complete the example also the properties (U7) and (U8) must be proven, but are left out in this presentation. Finally, the HOL-UNITY theory work is ended by closing the HOL session.

close_theory( );;

2.4 A 2-Arbiter

Informally an arbiter may be described as a device which is supposed to grant exclusive access to a shared resource in an arbitrary way. A 2-Arbiter is an arbiter which is restricted to allow only two users to request the resource simultaneously.

If the above explanation is unfamiliar to the reader, the 2-Arbiter may also be viewed as a device for guaranteeing mutual exclusion between only two processes sharing a critical region.

The 2-Arbiter is part of a larger system in which users makes request to the arbiter when wanting a grant of the resource that is supervised. This enables viewing the 2-Arbiter as a component with a certain behavior and the environment of the 2arbiter as the other component. In this system, the arbiter may only guarantee to behave as required if the environment, that is, the users behave as required by the arbiter, and the users of the the arbiter may determine to put restrictions on the behavior of the 2-Arbiter before they guarantee to behave as required by the arbiter. In this way the system consisting of the 2-Arbiter and its users will have a behavior of which the guaranteed behavior of each component is relying on the behavior of the other component. Such specifications are also called rely/guarantee specifications (see also [Sta85, GQNL90]). The behavior of the components may informally be described by the following conditions. The 2-Arbiter must unconditionally guarantee that at most one grant is given at any time, and that grant is only given on request. Further the arbiter must satisfy that any request is eventually satisfied and that a request which has been granted and is not wanted any more is eventually removed. The last two properties are however only guaranteed if the users maintain their request until a grant is given and that a user never makes a new request until an old grant is removed by the arbiter. In addition the arbiter requires that only this device may decide to give and take grants as requested by the users. The users of the 2-Arbiter must mutually guarantee, that if the arbiter guarantees access of only one user at a time, that only users may decide to make request and remove request, and that a given grant is kept until not requested any more then a granted request is eventually satisfied by its requester. It is noticed that this behavior is a description of the well-known four-phase- or handshaking protocol. The next section presents a specification of the described behavior of the 2-Arbiter component and the required behavior of the users in the UNITY notation. Some properties derived from the composition of the two specifications are proved to be satisfied. In the following section, a UNITY program is presented which is claimed to satisfy the properties as specified for the 2-Arbiter component. Finally, it is proved that the required properties are actually satisfied by the program. In the last section, it is briefly shown how the 2-Arbiter program may be defined using the HOL-UNITY system, and a tactic for proving all needed basic safety- and progress properties is defined. The proofs in HOL-UNITY are not presented here, since they are equivalent to the proofs given in UNITY.

The 2-Arbiter specification and program used in this example was originally developed by

Jørgen Staunstrup and Hans Henrik Løvengreen Department of Computer Science, Technical University of Denmark

for teaching students at the university in using UNITY.

Some proofs and a conditional progress property of the arbiter that were missing in the original example have however been added in this presentation to complete the verification of the 2-Arbiter program properties.

2.4.1 Specifying the System

We want to specify a System using a shared resource as the composition of a 2-Arbiter Arb and some users Users of the arbiter as described above. The entire system is then the composition of the two components:

System = (Arb []Users)

We may graphically describe the composed system by:

Figure 2.1: The 2-Arbiter system and its users

The task of the Arb component is as described to ensure exclusive access to one of possibly two users, who wants to get access to a shared resource, and the Arb component must guarantee grant gr_{i} is eventually given on request rq_{i}. However as described, we only require the Arb component to satisfy these demands if the users Users of the arbiter behaves as required.

The Arb Component

Unconditional Properties

Independent of how the environment behaves Arb guarantees.

At most one grant at a time.

¬(gr_{1} ∧ gr_{2}) invariant in Arb  (A1)

Arb never changes the value of rq_{i}.

∀i : rq_{i} stable in Arb  (A2)
∀i : ¬rq_{i} stable in Arb  (A3)

grant gr_{i} is maintained unless request rq_{i} disappears.

∀i : gr_{i} unless ¬rq_{i} in Arb  (A4)

Conditional Properties

If the assumptions holds, the Arb component guarantees that a reguest rq_{i} leads to a grant gr_{i} in the composed System.

{(U1), (U2), (U3), (U4), (∀i : gr_{i} leadsto ¬rq_{i} in System)}

⊢ ∀i : rq_{i} leadsto gr_{i} in System  (CA1)

If the assumptions holds, the Arb component guarantees that a given grant of a satisfied reguest rq_{i} is eventually removed. in the composed System.

{(U1), (U2), (U3), (U4), (∀i : gr_{i} leadsto ¬rq_{i} in System)}

⊢ ∀i : (¬rq_{i} ∧ gr_{i}) leadsto ¬gr_{i} in System  (CA2)

The Users Component

Unconditional Properties

No matter how the environment behaves Users guarantees.

No grant variable gr_{i} is changed by Users.

∀i : gr_{i} stable in Users  (U1)
∀i : ¬gr_{i} stable in Users  (U2)

A request value rq_{i} (¬rq_{i}) is stable unless the respective grant value gr_{i} (¬gr_{i}) is set by the Arb.

∀i : rq_{i} unless gr_{i} in Users  (U3)
∀i : ¬rq_{i} unless ¬gr_{i} in Users  (U4)

Conditional Properties

If the assumed properties holds in the environment, Users guarantees that a satisfied grant gr_{i} leads to a state in which request rq_{i} is set to false.

{(A2), (A3), (A4), ¬(gr_{1} ∧ gr_{2}) invariant in System}

⊢ ∀i : gr_{i} leadsto ¬rq_{i} in System  (CU1)

Derived Properties Satisfied by System

We want to prove that the invariant property (A1) is satisfied by the composed system.

¬(gr_{1} ∧ gr_{2}) invariant in (IC, Users[]Arb)  (thm 2.1)

Proof:

¬(gr_{1} ∧ gr_{2}) invariant in (IC, Arb)  (1)

from (A1)

¬gr_{1} stable in Users  (2)

from (U1)

¬gr_{2} stable in Users  (3)

from (U1)

¬(gr_{1} ∧ gr_{2}) stable in Users  (4)

disj. of (2), (3), and rewrite

¬(gr_{1} ∧ gr_{2}) invariant in (IC, Users[]Arb)  (5)

composition corollary 3 on (1) and (4) □

We also prove that a given grant eventually leads to a satisfied request, i.e. the request is removed in the composed system.

∀i : gr_{i} leadsto ¬rq_{i} in (Users[]Arb)  (thm 2.2)

Proof: {(A2), (A3), (A4), ¬(gr_{1} ∧ gr_{2}) invariant in (IC, Users[]Arb)}

⊢ ∀i : gr_{i} leadsto ¬rq_{i} in (Users[]Arb)  (1)

from (CU1)

∀i : gr_{i} leadsto ¬rq_{i} in (Users[]Arb)  (2)

from thm 2.1 and spec. (A2), (A3), and (A4) □

And a request eventually leads to a grant in the system:

∀i : rq_{i} leadsto gr_{i} in (Users[]Arb)  (thm 2.3)

Proof: {(U1), (U2), (U3), (U4), ∀i : gr_{i} leadsto ¬rq_{i} in (Users[]Arb)}

⊢ ∀i : rq_{i} leadsto gr_{i} in (Users[]Arb)  (1)

from (CA1)

∀i : rq_{i} leadsto gr_{i} in (Users[]Arb)  (2)

from thm 2.2 and spec. (U1), (U2), (U3), and (U4) □

Now, prove that a request leads to not request in the composed system:

∀i : rq_{i} leadsto ¬rq_{i} in (Users[]Arb)  (thm 2.4)

Proof:

∀i : rq_{i} leadsto ¬rq_{i} in (Users[]Arb)  (1)

from transitivity on thm 2.2 and thm 2.3 □

Prove the that no longer request and still grant eventually leads to not grant in the composed system:

∀i : (¬rq_{i} ∧ gr_{i}) leadsto ¬gr_{i} in (Users[]Arb)  (thm 2.5)

Proof:

{(U1), (U2), (U3), (U4), ∀i : gr_{i} leadsto ¬rq_{i} in (Users[]Arb)}

⊢ ∀i : (¬rq_{i} ∧ gr_{i}) leadsto ¬gr_{i} in (Users[]Arb)  (1)

from (CA2)

∀i : (¬rq_{i} ∧ gr_{i}) leadsto ¬gr_{i} in (Users[]Arb)  (2)

from thm 2.1, and spec. (U1), (U2), (U3), and (U4)

□

Prove the evident fact that not grant without request maintains the not grant:

∀i : (¬rq_{i} ∧ ¬gr_{i}) leadsto ¬gr_{i} in (Users[]Arb)  (thm 2.6)

Proof:

∀i : (¬rq_{i} ∧ ¬gr_{i}) leadsto ¬gr_{i} in (Users[]Arb)  (1)

from reflexivity of leads to and weakening

□

Finally we prove that the system satisfies the property that from a state without request the system eventually reaches a state without grant:

∀i : ¬rq_{i} leadsto ¬gr_{i} in (Users[]Arb)  (thm 2.7)

Proof:

∀i : ¬rq_{i} leadsto ¬gr_{i} in (Users[]Arb)  (1)

from leads to corollary 2 on thm 2.5 and thm 2.6

□

Proving the derived properties verifies that the composed system has the wanted properties of guaranteeing request eventually leading to grant and not request eventually leading to not grant. Hence we may conclude that the specification satisfies the required progress properties. The next step is to develop a 2-Arbiter program which satisfies the required properties as specified above.

2.4.2 A 2-Arbiter Program and its Verification

We start by claiming that the following program Arb satisfies the required behavior specified for the 2-Arbiter.

program { Arb }

initially  gr_{1} = gr_{2} = rq_{1} = rq_{2} = false (ps0)

begin

gr_{1}  := true  if rq_{1} ∧ ¬gr_{2}  (ps1)
[] gr_{2}  := true  if ¬rq_{1} ∧ rq_{2} ∧ ¬gr_{1} (ps2)
[] gr_{1}, gr_{2} := false, rq_{2}  if ¬rq_{1} ∧ gr_{1}  (ps3)
[] gr_{2}  := false  if ¬rq_{2} ∧ gr_{2}  (ps4)

end Initially the program requires that all variables are set to false. Actually this means that Arb must set gr_{i} to false and the Users environment must set rq_{i} to false. The program then has four statements that are executed in a fair interleaved way. The statements (ps1) and (ps2) give grants on request whereas (ps3) and (ps4) remove grants when requests are satisfied, i.e. they have become false. Notice however, that (ps3) may also give grant on request rq_{2}. It is also important to notice that the fair behavior of the program is guaranteed through the asymmetry built into the statements. We now want to prove that the Arb program does indeed satisfy the behavior specified above for the 2-Arbiter.

Verifying the Properties of the Arb Program

The goal is to prove that the given program Arb satisfies the specification such that, assuming the required behavior of the users Users, we may conclude that a request rq_{i} leads to a satisfied grant gr_{i}. We may write the wanted property as:

∀Users : {(U1), (U2), (U3), (U4), (∀i : gr_{i} leadsto ¬rq_{i} in (Arb []Users))}
⊢ ∀i : rq_{i} leadsto gr_{i} in (Arb []Users)

We may convince ourselves by inspection that the program Arb does actually satisfy the specified properties (A1), (A2), (A3), and (A4). In the later section on using HOL-UNITY such properties are easily proven by use of the system applying a tactic defined for this purpose.

We start by proving two useful theorems satisfied by the unless and the stable relation. The first proves a strengthened unless property assuming a stable and an unless property:

{p unless ¬q in Pr, q stable in Pr}

⊢ p unless p ∧ ¬q in Pr  (thm 2.8)

Proof:

p unless ¬q in Pr  (1)

from assumption of thm 2.8

q stable in Pr  (2)

from assumption of thm 2.8

p ∧ q unless false in Pr  (3)

stable def. and conj. of (1) and (2)

p ∧ ¬q unless p ∧ ¬q in Pr  (4)

reflexivity of unless

p unless ¬(p ∧ q) ∧ (p ∧ ¬q)in Pr  (5)

disj. on (3) and (4)

p unless p ∧ ¬q in Pr  (6)

rewrite of (5) □

and the second also assumes a stable and an unless property but this theorem concludes a strengthened stable property: {p unless q in Pr, ¬q stable in Pr}

⊢ p ∧ ¬q stable in Pr  (thm 2.9)

Proof:

p unless ¬q in Pr  (1)

from assumption of thm 2.9

¬q stable in Pr  (2)

from assumption of thm 2.9

p ∧ ¬q unless false in Pr  (3)

stable def. and conj. of (1) and (2)

p ∧ ¬q stable in Pr  (4)

stable def. on (3) □

These two theorems will be used for proving the required progress property satisfied. Progress of a program may be represented by an oriented graph or lattice in which the nodes are marked with the present values in the state of the program. The outgoing arcs then represent the possible state transitions. Inspecting the Arb program using this method described in details in [OL82] would reveal the behavior graph of Arb. This method was used in the original teaching example to cover the one branch progress:

rq_{2} leadsto gr_{2} in (Users []Arb)

of the Arb program. However, the UNITY theory supports a theorem which allows for proving progress in a way similar to this method. The theorem:

p ∧ b leadsto q, p ∧ ¬ b leadsto q

(CaseThm)

p leadsto q

which is presented as a corollary in [CM88] may be used for case analysis of a program extending the precondition of a leadsto property until it is strong enough to secure the progress of the program. This theorem will be used to prove the second progress branch

rq_{1} leadsto gr_{1} in (Users []Arb)

of the Arb program.

In the following we often write System in place of the more verbose (Users [] Arb). We start by proving a progress property which leads from a state in which the request rq_{2} occurs while the grant gr_{1} is still given from the 2-Arbiter program Arb. We have proven that the composed system satisfies the theorem thm 2.2 which guarantees that a grant gr_{i} will eventually be satisfied, i.e. rq_{i} will be false. Using this property we may prove that the system either reaches a state in which the request is satisfied with grant gr_{2} or in a state in which we still have request rq_{2} and grant gr_{1} but without request rq_{1}. Formally we may prove:

rq_{2} ∧ gr_{1} leadsto ¬rq_{1} ∧ gr_{1} ∧ rq_{2} ∨ gr_{2} in System  (thm 2.10)

Proof:

gr_{1} unless ¬rq_{1} in Arb  (1)

from spec (A4)

rq_{1} stable in Arb  (2)

from spec (A2)

gr_{1} unless ¬rq_{1} ∧ gr_{1} in Arb  (3)

from thm 2.8 on (1) and (2)

gr_{1} stable in Users  (4)

from spec (U1)

gr_{1} unless ¬rq_{1} ∧ gr_{1} in (Users[]Arb)  (5)

comp. corollary 2 on (3) and (4)

gr_{1} leadsto ¬rq_{1} in System  (6)

from thm 2.2

gr_{1} leadsto ¬rq_{1} ∧ gr_{1} in System  (7)

PSP theorem on (5) and (6)

rq_{2} unless gr_{2} in System  (8)

comp. corollary 2 on (U3) and (A2)

rq_{2} ∧ gr_{1} leadsto ¬rq_{1} ∧ gr_{1} ∧ rq_{2} ∨ gr_{2} in System  (9)

PSP theorem on (7) and (8) □ We wanted to prove the property

rq_{2} ∧ gr_{1} leadsto gr_{2} in System

but the theorem thm 2.10 above did not guarantee a final state with satisfied the grant gr_{2}. Fortunately UNITY provides the leads to cancellation theorem

p leadsto q ∨ b, b leadsto r

(CancelThm)

p leadsto q ∨ r

Hence, we prove

rq_{2} ∧ gr_{1} ∧ ¬rq_{1} leadsto gr_{2} in System  (thm 2.11)

Proof:

rq_{2} ∧ gr_{1} ∧ ¬rq_{1} ensures gr_{2} in Arb  (1)

satisfied by the program

rq_{2} ∧ gr_{1} ∧ ¬rq_{1} unless gr_{2} in Users  (2)

from lemma thm 2.12

rq_{2} ∧ gr_{1} ∧ ¬rq_{1} ensures gr_{2} in System  (3)

by the union theorem 1

rq_{2} ∧ gr_{1} ∧ ¬rq_{1} leadsto gr_{2} in System  (4)

basic leads to inference rule □ to use the cancellation theorem. We used the lemma thm 2.12 in the proof of theorem thm 2.11:

rq_{2} ∧ gr_{1} ∧ ¬rq_{1} unless gr_{2} in System  (thm 2.12)

Proof:

gr_{1} stable in Users  (1)

from spec. (U1)

¬rq_{1} unless ¬gr_{1} in Users  (2)

from spec. (U4)

gr_{1} ∧ ¬rq_{1} stable in Users  (3)

theorem thm 2.9 on (1) and (2)

rq_{2} unless gr_{2} in Users  (4)

from spec. (U3)

rq_{2} ∧ gr_{1} ∧ ¬rq_{1} unless gr_{2} in System  (5)

simple conj. on (3) and (4)

□

Using the cancellation theorem we get

rq_{2} ∧ gr_{1} leadsto gr_{2} in System  (thm 2.13)

Proof:

rq_{2} ∧ gr_{1} leadsto gr_{2} in System  (1)

cancellation on theorem thm 2.10 and thm 2.11

□

This completes the proof of the first progress property. Now to prove

rq_{2} leadsto gr_{2} in System

we may prove

rq_{2} ∧ ¬gr_{1} leadsto gr_{2} in System

and use the above mentioned theorem for case analysis. It turns out that proving this progress property is more complicated. The precondition (rq_{2} ∧ ¬gr_{1}) is not strong enough to guarantee progress of the Arb program. This means, we have to apply case analysis again. If we strengthen the precondition with the condition gr_{2} we get two proofs. The first is trivially satisfied:

rq_{2} ∧ ¬gr_{1} ∧ gr_{2} leadsto gr_{2} in System  (thm 2.14)

Proof:

rq_{2} ∧ ¬gr_{1} gr_{2} leadsto gr_{2} in System  (1)

trivially by leads to implication theorem □ Hence, now we need to prove the property:

rq_{2} ∧ ¬gr_{1} ∧ ¬gr_{2} leadsto gr_{2} in System

But again we need more information to prove the property. We present the two proofs needed and apply the case analysis theorem to prove the wanted property. The first proof with rq_{1}:

rq_{1} ∧ ¬gr_{1} ∧ rq_{2} ∧ ¬gr_{2} leadsto gr_{2} in System  (thm 2.15)

Proof:

rq_{1} ∧ ¬gr_{1} ∧ rq_{2} ∧ ¬gr_{2} ensures gr_{1} ∧ rq_{2} in Arb  (1)

satisfied by program Arb

gr_{1} ∧ ¬rq_{1} stable in Users  (2)

theorem thm 2.9 on (U1) and (U4)

gr_{2} ∧ ¬rq_{2} stable in Users  (3)

theorem thm 2.9 on (U1) and (U4)

rq_{1} ∧ ¬gr_{1} ∧ rq_{2} ∧ ¬gr_{2} stable in System  (4)

conj. on (2) and (3)

rq_{1} ∧ ¬gr_{1} ∧ rq_{2} ∧ ¬gr_{2} ensures gr_{1} ∧ rq_{2} in System  (5)

union corollary 4 on (4) and (1)

gr_{1} leadsto ¬rq_{1} ∧ gr_{1} in System  (6)

from line (7) in theorem thm 2.10

rq_{2} unless gr_{2} in System  (7)

union corollary 1 on (U3) and (A2) from spec.

rq_{2} ∧ gr_{1} leadsto ¬rq_{1} ∧ gr_{1} ∧ rq_{2} ∨ gr_{2} in System  (8)

PSP theorem on (6) and (7)

gr_{1} ∧ ¬rq_{1} ∧ rq_{2} unless gr_{2} in Users  (9)

stable def. and conj. on (2) and (U3)

gr_{1} ∧ ¬rq_{1} ∧ rq_{2} ensures gr_{2} in Arb  (10)

satisfied by program Arb

gr_{1} ∧ ¬rq_{1} ∧ rq_{2} ensures gr_{2} in System  (11)

union theorem 1 on (9) and (10)

rq_{2} ∧ gr_{1} leadsto gr_{2} in System  (12)

cancellation theorem on (8) and (11)

rq_{1} ∧ ¬gr_{1} ∧ rq_{2} ∧ ¬gr_{2} leadsto gr_{2} in System  (13)

transitivity on (5) and (12)

□ Then the proof with ¬rq_{1}:

¬rq_{1} ∧ ¬gr_{1} ∧ rq_{2} ∧ ¬gr_{2} leadsto gr_{2} in System  (thm 2.16)

Proof:

¬rq_{1} ∧ ¬gr_{1} ∧ rq_{2} ∧ ¬gr_{2} ensures gr_{2} in Arb  (1)

satisfied by program Arb

¬rq_{1} unless rq_{1} in Users  (2)

antireflexivity of unless

¬gr_{1} unless false in Users  (3)

from spec. (U2) and stable def.

¬rq_{1} ∧ ¬gr_{1} unless rq_{1} ∧ ¬gr_{1} in Users  (4)

conj. on (2) and (3)

¬gr_{2} unless gr_{2} in Users  (5)

antireflexivity of unless

¬rq_{1} ∧ ¬gr_{1} ∧ ¬gr_{2} unless rq_{1} ∧ ¬gr_{1} ∧ ¬gr_{2} ∨ gr_{2} in Users  (6)

conj. on (4) and (5)

rq_{2} unless gr_{2} in Users  (7)

from spec (U3)

¬rq_{1} ∧ ¬gr_{1} ∧ rq_{2} ∧ ¬gr_{2} unless rq_{1} ∧ ¬gr_{1} ∧ rq_{2} ∧ ¬gr_{2} ∨ gr_{2}
in Users  (8)

conj. on (6) and (7)

¬rq_{1} ∧ ¬gr_{1} ∧ rq_{2} ∧ ¬gr_{2} ensures rq_{1} ∧ ¬gr_{1} ∧ rq_{2} ∧ ¬gr_{2} ∨ gr_{2}
in System  (9)

union theorem on (8) and (1)

¬rq_{1} ∧ ¬gr_{1} ∧ rq_{2} ∧ ¬gr_{2} leadsto gr_{2} in System  (10)

cancellation on (9) and theorem thm 2.15 □ Hence we may now prove:

rq_{2} ∧ ¬gr_{1} leadsto gr_{2} in System  (thm 2.17)

Proof:

rq_{2} ∧ ¬gr_{1} leadsto gr_{2} in System  (1)

(CaseThm) on theorems thm 2.14, thm 2.15 and thm 2.16 □ And finally

rq_{2} leadsto gr_{2} in System  (thm 2.18)

Proof:

rq_{2} leadsto gr_{2} in System  (1)

(CaseThm) on theorems thm 2.13 and thm 2.17

□

This completes the verification of the 2-Arbiter program Arb satisfying the required progress property of grant gr_{2} on request rq_{2}. To complete the verification of the Arb program, we need to prove the second progress property

rq_{1} leadsto gr_{1} in System

satisfied. Again we may use the theorem (CaseThm) for case analysis. We start by proving the progress property of the case with the precondition (rq_{1} ∧ ¬gr_{2}) satisfied, since this is easily proved.

rq_{1} ∧ ¬gr_{2} leadsto gr_{1} in System  (thm 2.19)

Proof:

rq_{1} ∧ ¬gr_{2} ensures gr_{1} in Arb  satisfied by program Arb  (1)
rq_{1} unless gr_{1} in Users  from spec. (U3)  (2)
¬gr_{2} unless false in Users  from spec. (U2) and stable def.  (3)
rq_{1} ∧ ¬gr_{2} unless gr_{1} in Users  conj. on (2) and (3) and weakening  (4)
rq_{1} ∧ ¬gr_{2} ensures gr_{1} in System  union theorem 1 on (1) and (4)  (5)
rq_{1} ∧ ¬gr_{2} leadsto gr_{1} in System  (6)

basic leads to theorem on (5)

□

Hence, we just need to prove

rq_{1} ∧ gr_{2} leadsto gr_{1} in System

which as above requires case analysis. If we strengthen the precondition with the condition gr_{1} we get two proofs. The first is trivially satisfied:

rq_{1} ∧ gr_{1} ∧ gr_{2} leadsto gr_{1} in System  (thm 2.20)

Proof:

rq_{1} ∧ gr_{1} ∧ gr_{2} leadsto gr_{1} in System  (1)

trivially by leads to implication theorem □

Hence, now we need to prove the property:

rq_{2} ∧ ¬gr_{1} ∧ gr_{2} leadsto gr_{1} in System

But again we need strengthening the preconditions. We present the two last proofs needing program progress:

rq_{1} ∧ ¬gr_{1} ∧ ¬rq_{2} ∧ gr_{2} leadsto gr_{1} in System  (thm 2.21)

Proof:

rq_{1} ∧ ¬gr_{1} ∧ ¬rq_{2} ∧ gr_{2} ensures rq_{1} ∧ ¬gr_{1} ∧ ¬gr_{2} in Arb  (1)

satisfied by Arb program

rq_{1} ∧ ¬gr_{1} unless false in Users  (2)

theorem thm 2.9 on (U1) and (U4)

¬rq_{2} unless ¬gr_{2} in Users  (3)

from spec. (U4)

gr_{2} unless false in Users  (4)

from spec. (U1) and stable def.

¬rq_{2} ∧ gr_{2} unless false in Users  (5)

conj. on (3) and (4)

rq_{1} ∧ ¬gr_{1} ∧ ¬rq_{2} ∧ gr_{2} unless false in Users  (6)

conj. on (2) and (5)

rq_{1} ∧ ¬gr_{1} ∧ ¬rq_{2} ∧ gr_{2} ensures rq_{1} ∧ ¬gr_{1} ∧ ¬gr_{2} in System  (7)

union corollary 4 on (1) and (6)

¬gr_{2} unless false in Users  (8)

from spec. (U2) and stable def.

rq_{1} ∧ ¬gr_{1} ∧ ¬gr_{2} unless false in Users  (9)

conj. on (2) and (8)

rq_{1} ∧ ¬gr_{1} ∧ ¬gr_{2} ensures gr_{1} in Arb  (10)

satisfied by program Arb

rq_{1} ∧ ¬gr_{1} ∧ ¬gr_{2} ensures gr_{1} in System  (11)

union corollary 4 on (9) and (10)

rq_{1} ∧ ¬gr_{1} ∧ ¬rq_{2} ∧ ¬gr_{2} leadsto gr_{1} in System  (12)

transitivity on (1) and (11)

□ It turns out that using theorem thm 2.21 we may prove the last progress property without proving first

rq_{1} ∧ ¬gr_{1} ∧ rq_{2} ∧ gr_{2} leadsto gr_{1} in System

We directly get:

rq_{1} ∧ ¬gr_{1} ∧ gr_{2} leadsto gr_{1} in System  (thm 2.22)

Proof:

gr_{2} leadsto ¬rq_{2} in System  (1)

from theorem thm 2.2

rq_{1} ∧ ¬gr_{1} unless false in Users  (2)

theorem thm 2.9 on (U1) and (U4)

gr_{2} unless false in Users  (3)

from spec. (U1)

rq_{1} ∧ ¬gr_{1} ∧ gr_{2} unless false in Users  (4)

conj. on (2) and (3)

rq_{1} unless false in Arb  (5)

from spec. (A2)

¬gr_{1} unless gr_{1} in Arb  (6)

antireflexivity of unless

rq_{1} ∧ ¬gr_{1} unless gr_{1} in Arb  (7)

conj. on (5) and (6)

gr_{2} unless ¬gr_{2} in Arb  (8)

antireflexivity of unless

rq_{1} ∧ ¬gr_{1} ∧ gr_{2} unless rq_{1} ∧ ¬gr_{1} ∧ ¬gr_{2} ∨ gr_{1} in Arb  (9)

conj. on (7) and (8)

rq_{1} ∧ ¬gr_{1} ∧ gr_{2} unless rq_{1} ∧ ¬gr_{1} ∧ ¬gr_{2} ∨ gr_{1} in System  (10)

union corollary 2 on (4) and (9)

rq_{1} ∧ ¬gr_{1} ∧ gr_{2} leadsto rq_{1} ∧ ¬gr_{1} ∧ ¬rq_{2} ∧ ¬gr_{2} ∨ rq_{1} ∧ ¬gr_{2} ∨ gr_{1}
in System  (11)

PSP theorem on (1) and (10)

rq_{1} ∧ ¬gr_{1} ∧ gr_{2} leadsto gr_{1} in System  (12)

cancellation theorem on (11), thm 2.21, thm 2.19 □ We may now prove:

rq_{1} ∧ gr_{1} leadsto gr_{1} in System  (thm 2.23)

Proof:

rq_{1} ∧ gr_{1} leadsto gr_{1} in System  (1)

(CaseThm) on theorems thm 2.20 and thm 2.22

□

And

rq_{1} leadsto gr_{1} in System  (thm 2.24)

Proof:

rq_{1} leadsto gr_{1} in System  (1)

(CaseThm) on theorems thm 2.19 and thm 2.23

□

This completes the verification of the 2-Arbiter program Arb satisfying the required progress property of grant gr_{1} on request rq_{1}. This means, from theorem thm 2.18 and theorem thm 2.24 we may conclude that the 2-Arbiter program Arb composed with Users satisfies:

∀i : rq_{i} leadsto gr_{i} in System

which was exactly what was required in the specification by the property (CA1). The proof of the progress property (CA2) is left to the reader.

The 2-Arbiter specification and the program may of course be defined using the HOL-UNITY system. In this way the shown proofs may be mechanized. The next section briefly describes how the specification can be defined and how the program may be represented.

2.4.3 The 2-Arbiter in HOL-UNITY

As described in the previous examples and in the introduction to the chapter, we need to define a state which reflects the specification before we are able to define anything in the HOL-UNITY system. In the section 2.3 describing the readers/writers problem, we defined the state described as a standard method in the introduction to the chapter. However, in this example we want to introduce a state which reflects the specification in a more natural way. In the specification the properties are defined as indexed safety- and progress properties that have to be satisfied for each of two requests rq_{i} and grants gr_{i}. Properties that have to be satisfied by either the 2-Arbiter or the users. We may define a state which is a mapping from the two entries onto a pair of variables. This is, the type of the state will be a mapping of an enumerated type with two elements onto a pair of boolean type representing each of the boolean variables.

Defining a state for the 2-Arbiter in HOL-UNITY

The enumerated type could be defined as:

users = (U1, U2)

and the state by:

state = ((i : users)→(bool, bool))

The four predicate variables rq_{1}, gr_{1} and rq_{2}, gr_{2} may then be defined by the indexed variables:

\begin{matrix}rq i = (λ(s : state). fst (s i)) \\ gr i = (λ(s : state). snd (s i)) \end{matrix}

With a state like the presented and the definition of the variables we may make a specification in HOL-UNITY.

Defining a state for the 2-Arbiter in HOL-UNITY

To define the 2-Arbiter program Arb we need to transform each assignment into a state transition and define the program as the list of these state transitions.

We define the first assign statement gr U1 := true if rq U1 ∧ ¬(gr U2)

by the state transition which only change the state if the user is U1. Further the variable gr U1 is only changed if the condition is true in the given state. All other values are let unchanged in the new state. The following lambda expression defines the wanted state transition reflecting the perhaps more readable assignment given above:

λs. λi. (i = U1) ∧ rq U1 s ∧ ¬(gr U2 s) =≻ (rq U1 s, true) | s i

Similarly the assignment gr U2 := true if ¬(rq U1) ∧ ¬(gr U1) ∧ rq U2

is defined by:

\begin{matrix}λs. λi. (i = U2) ∧ ¬(rq U1 s) ∧ ¬(gr U1 s) ∧ rq U2 s \\ =≻ (rq U2 s, true) | s i \end{matrix}

In the assignment gr U1, gr U2 := false, rq U2 if ¬(rq U1) ∧ gr U1 two variables are changed. Hence, we must define the assignment as the state transition changing both (gr U1) and (gr U2). Notice that both values need a state satisfying the enabling condition before it may be changed. The following lambda expression defines the wanted transition and change of values in the state:

\begin{matrix}λs.λi.¬(rq U1) ∧ gr U1 =≻ \\ (i = U1) =≻ (rq U1 s, false) | (i = U2) =≻ (rq U2 s, rq U2 s) | s i \end{matrix}

Finally the assignment gr U2 := false if ¬(rq U2) ∧ gr U2

is defined by:

λs. λi. (i = U2) ∧ (¬(rq U2) ∧ gr U2) =≻ (rq U2s, false) | s i

These definitions enable us to define the wanted program as a list of the four state transitions. Since the presented specification may immediately be transformed into HOL notation just like the previous examples we completely leave out the more verbose HOL-UNITY proofs. The detailed proof may be found as part of the UNITY contribution to the HOL system. The example is completed by showing the possibility of automating the proof that the program meets the specified unless, stable and ensures properties.

Automated proof of basic Arb program properties

Since this example with the Arb program is a finite state example, the proving of the unless, stable and ensures properties may be made almost automatically by the HOL theorem prover. We just need to define a tactic which rewrites all definitions into HOL terms, does beta reduction and case analysis. It turned out that the tactic needed some extra theorems like the information that all the defined program variables are different and the explicit information about the excluded middle and de Morgan rules. And the proof of ensures properties is currently limited to proving the existence of a state transition which guarantees the post condition to be fulfilled. Further it turned out that case analysis and beta reduction although not surprising had to be performed in as many levels as the nesting of the conditional state transitions. The defined tactic is presently only a hack. But it is believed that a general method for developing tactics may be developed for examples with finite state space only.

The tactic defined below is the one used to prove the claimed safety properties (unless, stable) and the basic progress property ensures in the HOL-UNITY version of the 2-Arbiter example.

let PROVE_PROG_TAC =
   REWRITE_TAC

 [UNLESS;UNLESS_STMT;EXIST_TRANSITION;ENSURES;STABLE;INVARIANT;
  ~*;/\*;\/*;TRUE_DEF;FALSE_DEF;req;gr;user_thm1;user_thm2] THEN
BETA_TAC THEN
REWRITE_TAC
  [NOT_CLAUSES;AND_CLAUSES;OR_CLAUSES;
   DE_MORGAN_THM;EXCLUDED_MIDDLE] THEN
REPEAT STRIP_TAC THEN
(ASM_REWRITE_TAC [] THEN
 BETA_TAC THEN ASM_REWRITE_TAC [user_thm1] THEN RES_TAC THEN
 UNDISCH_ONE_TAC THEN
 ASM_REWRITE_TAC [] THEN
 BETA_TAC THEN ASM_REWRITE_TAC [user_thm1] THEN RES_TAC) THEN
STRIP_TAC THEN
REPEAT COND_CASES_TAC THEN BETA_TAC THEN REWRITE_TAC [] THEN
BETA_TAC THEN
ASM_REWRITE_TAC [user_thm1;user_thm2;EXCLUDED_MIDDLE] THEN
UNDISCH_ONE_TAC THEN REPEAT COND_CASES_TAC THEN BETA_TAC THEN
ASM_REWRITE_TAC [user_thm1;user_thm2;EXCLUDED_MIDDLE];;

This completes the last example on how to make UNITY specifications in HOL-UNITY.

Appendix A

UNITY - Theorems and Corollaries

In this appendix all UNITY theorems and corollaries found in [CM88] are listed. The listing is sorted by starting with unless and stable properties followed by ensures and leadsto and ending with the compositionality properties. Every theorem and corollary is given a naming as in [CM88] and is additionally labeled with the theorem naming in the HOL-UNITY theory. A brief listing of these definitions and theorems are given in appendix B.

unless theorems

reflexivity

p unless p in Pr (UNLESS thm1)

antireflexivity

p unless ¬p in Pr (UNLESS thm2)

consequence weakening

\begin{matrix}p unless q in Pr, & q ⇒ r \\ p unless r \end{matrix} (UNLESS thm3)

conjunction

\begin{matrix}p unless q in Pr, & p’ unless q’ in Pr \\ (p ∧ p’) unless (p ∧ q’) ∨ (p’ ∧ q) ∨ (q ∧ q’) in Pr \end{matrix} (UNLESS thm4)

disjunction

\begin{matrix}p unless q in Pr, & p’ unless q’ in Pr \\ (p ∨ p’) unless (¬p ∧ q’) ∨ (¬p’ ∧ q) ∨ (q ∧ q’) in Pr \end{matrix} (UNLESS thm5)

simple conjunction

\begin{matrix}p unless q in Pr, & p’ unless q’ \\ p ∧ p’ unless q ∨ q’ in Pr \end{matrix} (UNLESS thm6)

simple disjunction

\begin{matrix}p unless q in Pr, & p’ unless q’ in Pr \\ p ∨ p’ unless q ∨ q’ in Pr \end{matrix} (UNLESS thm7)

cancellation

\begin{matrix}p unless q in Pr, & q unless r in Pr \\ p ∨ q unless r in Pr \end{matrix} (UNLESS thm8)

unless corollaries

unless introduction

\begin{matrix}p ⇒ q \\ p unless q in Pr \end{matrix} (UNLESS cor1)

unless introduction

\begin{matrix}¬p ⇒ q \\ p unless q in Pr \end{matrix} (UNLESS cor2) p unless q ∨ r in Pr = p ∧ ¬q unless q ∨ r in Pr (UNLESS cor3)

\begin{matrix}p ∨ q unless r \\ p unless q ∨ r in Pr \end{matrix} (UNLESS cor4) p unless true in Pr (UNLESS cor5) true unless p in Pr (UNLESS cor6) false unless p in Pr (UNLESS cor7)

\begin{matrix}p ∧ ¬q ⇒ p’ ⇒ p ∨ q \\ p unless q in Pr = p’ unless q in Pr \end{matrix} (UNLESS cor8)

generalized cancellation

\begin{matrix}p ∨ p’ unless q ∨ r in Pr, & q ∨ q’ unless p ∨ r’ in Pr \\ (p ∨ p’ ∨ q ∨ q’) unless ((p ∧ q) ∨ r ∨ r’ in Pr \end{matrix} (UNLESS cor9)

\begin{matrix}p ∨ q stable in Pr \\ p unless q in Pr \end{matrix} (UNLESS cor10)

\begin{matrix}p unless q in Pr, q unless p in Pr, & ¬(p ∧ q) \\ (p ∨ q) stable in Pr ((p ∧ q) ∨ r ∨ r’ in Pr \end{matrix} (UNLESS cor13)

ensures theorems

empty ensures

p ensures q in { } = false (ENSURES thm0)

reflexivity

p ensures p in ({st} ⋃ Pr) (ENSURES thm1)

consequence weakening

\begin{matrix}p ensures q in Pr, & q ⇒ r \\ p ensures r in Pr \end{matrix} (ENSURES thm2)

impossibility

\begin{matrix}p ensures false in Pr \\ ¬p \end{matrix} (ENSURES thm3)

conjunction

\begin{matrix}p unless q in Pr, & p’ ensures q’ in Pr \\ (p ∧ p’) ensures(p ∧ q’) ∨ (p’ ∧ q) ∨ (q ∧ q’) in Pr \end{matrix} (ENSURES thm4)

disjunction

\begin{matrix}p ensures q in Pr \\ (p ∨ r) ensures q ∨ r in Pr \end{matrix} (ENSURES thm5)

ensures corollaries

ensures implication

\begin{matrix}p ⇒ q \\ p ensures q in Pr \end{matrix} (ENSURES cor1)

or elimination

\begin{matrix}p ∨ q ensures r in Pr \\ p unless q ∨ r in Pr \end{matrix} (ENSURES cor3)

leadsto theorems

implication theorem

\begin{matrix}p ⇒ q \\ p leadsto q in (\{st\} ⋃ Pr) \end{matrix} (LEADSTO thm25)

impossibility

\begin{matrix}p leadsto false in Pr \\ ¬p \end{matrix} (LEADSTO thm30)

disjunction (general)

For any set well-founded set W:

\begin{matrix}⟨∀m : m ∈ W :: p_{m}leadsto q_{m} in P r⟩ \\ ⟨∃m : m ∈ W :: p_{m}⟩leadsto ⟨∃m : m ∈ W :: q_{m}⟩ in P r \end{matrix} (LEADSTO thm3a)

This theorem is derived by weakening of the disjunctive closure property which in HOL-UNITY is proved as the theorem (LEADSTO thm3). cancellation

\begin{matrix}p leadsto q ∨ b in Pr, & b leadsto r in Pr \\ p leadsto q ∨ r in Pr \end{matrix} (LEADSTO thm28)

PSP (Progress-Safety-Progress)

\begin{matrix}p leadsto q in Pr, & r unless b in Pr \\ p ∧ r leadsto (q ∧ r) ∨ b in Pr \end{matrix} (LEADSTO thm29)

completion For any finite set of predicates p_{i}, q_{i}, 0 ≤ i < N:

\begin{matrix}⟨∀i :: p_{i}leadsto q_{i}∨ b in P r⟩, & ⟨∀i :: q_{i}unless b in P r⟩ \\ ⟨∧ i :: p_{i}⟩leadsto ⟨∧ i :: q_{i}∨ b in P r⟩ \end{matrix} (LEADSTO cor13)

metric induction For any set well-founded set W:

\begin{matrix}⟨∀m : m ∈ W : p ∧ (M =_{∗} m) leadsto (p ∧ M <_{∗} m) ∨ q in Pr ⟩ \\ p leadsto q in Pr \end{matrix} (LEADSTO thm36)

leadsto corollaries

finite disjunction

\begin{matrix}p leadsto q in Pr, & p’ leadsto q’ in Pr \\ p ∨ p’ leadsto q ∨ q’ in Pr \end{matrix} (LEADSTO thm27)

weakening disjunction

\begin{matrix}p ∧ b leadsto q in Pr, & p ∧ ¬b leadsto q in Pr \\ p leadsto q in Pr \end{matrix} (LEADSTO cor1)

stable PSP

\begin{matrix}p leadsto q in Pr, & r stable in Pr \\ p ∧ r leadsto q ∧ r in Pr \end{matrix} (LEADSTO cor2)

compositionality theorems

composed unless property

\begin{matrix}p unless q in (F [] G) = \\ p unless q in F ∧ p unless q in G \end{matrix} (COMP UNLESS thm1)

composed ensures property

\begin{matrix}p ensures q in (F [] G) = \\ (p ensures q in F ∧ p unless q in G) ∨ \\ (p ensures q in G ∧ p unless q in F) \end{matrix} (COMP ENSURES thm1)

program fixed point

FP of (F [] G) = FP of F ∧ FP of G (not proved)

compositionality corollaries

unless, stable deduction

\begin{matrix}p unless q in F, & p stable in G \\ p unless q in (F [] G) \end{matrix} (COMP UNITY cor2)

invariant, stable deduction

\begin{matrix}p invariant in (P r_{init}, F), & p stable in G \\ p invariant in (P r_{init}, F [] G) \end{matrix} (COMP UNITY cor3)

ensures, stable deduction

\begin{matrix}p ensures q in F, & p stable in G \\ p ensures in (F [] G) \end{matrix} (COMP UNITY cor4)

Appendix B

HOL-UNITY - Definitions and Theorems

The Theory state logic

Parents --  HOL
Constants --
/\* ":(* -> bool) -> ((* -> bool) -> (* -> bool))"
\/* ":(* -> bool) -> ((* -> bool) -> (* -> bool))"
==>* ":(* -> bool) -> ((* -> bool) -> (* -> bool))"
<* ":(* -> num) -> ((* -> num) -> (* -> bool))"
>* ":(* -> num) -> ((* -> num) -> (* -> bool))"
<=* ":(* -> num) -> ((* -> num) -> (* -> bool))"
>=* ":(* -> num) -> ((* -> num) -> (* -> bool))"
=* ":(* -> **) -> ((* -> **) -> (* -> bool))"
=>* ":(* -> bool) -> ((* -> **) -> ((* -> **) -> (* -> **)))"
+* ":(* -> num) -> ((* -> num) -> (* -> num))"
-* ":(* -> num) -> ((* -> num) -> (* -> num))"
** ":(* -> num) -> ((* -> num) -> (* -> num))"
ModX ":(* -> num) -> ((* -> num) -> (* -> num))"
DivX ":(* -> num) -> ((* -> num) -> (* -> num))"

ExpX ":(* -> num) -> ((* -> num) -> (* -> num))"
IndX ":(* -> (*1 -> *2)) -> ((* -> *1) -> (* -> *2))"
FALSE ":* -> bool"     TRUE ":* -> bool"
~* ":(* -> bool) -> (* -> bool)"
!* ":(** -> (* -> bool)) -> (* -> bool)"
?* ":(** -> (* -> bool)) -> (* -> bool)"
SucX ":(* -> num) -> (* -> num)"
PreX ":(* -> num) -> (* -> num)"
!<=* ":(num -> (* -> bool)) -> (num -> (* -> bool))"
?<=* ":(num -> (* -> bool)) -> (num -> (* -> bool))"
?<* ":(num -> (* -> bool)) -> (num -> (* -> bool))"
/<=\* ":(num -> (* -> bool)) -> (num -> (* -> bool))"
\<=/* ":(num -> (* -> bool)) -> (num -> (* -> bool))"
/<\* ":(num -> (* -> bool)) -> (num -> (* -> bool))"
\</* ":(num -> (* -> bool)) -> (num -> (* -> bool))"
Infixes --
/\* ":(* -> bool) -> ((* -> bool) -> (* -> bool))"
\/* ":(* -> bool) -> ((* -> bool) -> (* -> bool))"
==>* ":(* -> bool) -> ((* -> bool) -> (* -> bool))"
<* ":(* -> num) -> ((* -> num) -> (* -> bool))"
>* ":(* -> num) -> ((* -> num) -> (* -> bool))"
<=* ":(* -> num) -> ((* -> num) -> (* -> bool))"
>=* ":(* -> num) -> ((* -> num) -> (* -> bool))"
=* ":(* -> **) -> ((* -> **) -> (* -> bool))"
=>* ":(* -> bool) -> ((* -> **) -> ((* -> **) -> (* -> **)))"
+* ":(* -> num) -> ((* -> num) -> (* -> num))"
-* ":(* -> num) -> ((* -> num) -> (* -> num))"
** ":(* -> num) -> ((* -> num) -> (* -> num))"
ModX ":(* -> num) -> ((* -> num) -> (* -> num))"
DivX ":(* -> num) -> ((* -> num) -> (* -> num))"
ExpX ":(* -> num) -> ((* -> num) -> (* -> num))"
IndX ":(* -> (*1 -> *2)) -> ((* -> *1) -> (* -> *2))"
Binders --
!* ":(** -> (* -> bool)) -> (* -> bool)"
?* ":(** -> (* -> bool)) -> (* -> bool)"
Definitions --
FALSE_DEF  |- FALSE = (\s. F)
TRUE_DEF  |- TRUE = (\s. T)
~*  |- !p. ~* p = (\s. ~p s)
/\*  |- !p q. p /\* q = (\s. p s /\ q s)
\/*  |- !p q. p \/* q = (\s. p s \/ q s)
!*  |- !P. $!* P = (\s. !x. P x s)
?*  |- !P. $?* P = (\s. ?x. P x s)
==>*  |- !p q. p ==>* q = (\s. p s ==> q s)
<*  |- !p q. p <* q = (\s. (p s) < (q s))
>*  |- !p q. p >* q = (\s. (p s) > (q s))
<=*  |- !p q. p <=* q = (\s. (p s) <= (q s))
>=*  |- !p q. p >=* q = (\s. (p s) >= (q s))
=*  |- !p q. p =* q = (\s. p s = q s)
=>*  |- !p r1 r2. (p =>* r1)r2 = (\s. (p s => r1 s | r2 s))
+*  |- !p q. p +* q = (\s. (p s) + (q s))
-*  |- !p q. p -* q = (\s. (p s) - (q s))
**  |- !p q. p ** q = (\s. (p s) * (q s))
SucX  |- !p. SucX p = (\s. SUC(p s))

PreX  |- !p. PreX p = (\s. PRE(p s))
ModX  |- !p q. p ModX q = (\s. (p s) MOD (q s))
DivX  |- !p q. p DivX q = (\s. (p s) DIV (q s))
ExpX  |- !p q. p ExpX q = (\s. (p s) EXP (q s))
IndX  |- !a i. a IndX i = (\s. a s(i s))
!<=*  |- !P m. !<=* P m = (\s. !i. i <= m ==> P i s)
?<=*  |- !P m. ?<=* P m = (\s. ?i. i <= m /\ P i s)
?<*  |- !P m. ?<* P m = (\s. ?i. i < m /\ P i s)
/<=\*
  |- (!P. /<=\* P 0 = P 0) /\
     (!i P. /<=\* P(SUC i) = (/<=\* P i) /\* (P(SUC i)))
\<=/*
  |- (!P. \<=/* P 0 = P 0) /\
     (!i P. \<=/* P(SUC i) = (\<=/* P i) \/* (P(SUC i)))
/<\*
  |- (!P. /<\* P 0 = FALSE) /\
     (!i P. /<\* P(SUC i) = (/<\* P i) /\* (P i))
\</*
  |- (!P. \</* P 0 = FALSE) /\
     (!i P. \</* P(SUC i) = (\</* P i) \/* (P i))
Theorems --
IMPLY_WEAK_lemma1
  |- !p q p' q' s.
      (((p /\* q') \/* (p' /\* q)) \/* (q /\* q'))s ==> (q \/* q')s
IMPLY_WEAK_lemma2
  |- !p q p' q' s.
      ((((~* p) /\* q') \/* ((~* p') /\* q)) \/* (q /\* q'))s ==>
      (q \/* q')s
IMPLY_WEAK_lemma3
  |- !p q r s.
      ((((~* p) /\* r) \/* ((~* q) /\* q)) \/* (q /\* r))s ==> r s
IMPLY_WEAK_lemma4
  |- !p q p' q' r r' s.
      ((((~*(p \/* p')) /\* (p \/* r')) \/*
        ((~*(q \/* q')) /\* (q \/* r))) \/*
       ((q \/* r) /\* (p \/* r')))
      s ==>
      ((p /\* q) \/* (r \/* r'))s
IMPLY_WEAK_lemma5
  |- !p q r s.
      ((p /\* r) \/* (((p \/* q) /\* (q \/* r)) \/* r))s ==>
      (q \/* r)s
IMPLY_WEAK_lemma6
  |- !p q b r s.
      ((r /\* q) \/* ((p /\* b) \/* (b /\* q)))s ==>
      ((q /\* r) \/* b)s
IMPLY_WEAK_lemma7
  |- !p q b r s.
      (((r /\* q) \/* ((r /\* p) /\* b)) \/* (b /\* q))s ==>
      ((q /\* r) \/* b)s
AND_COMM_OR_lemma  |- !p q r. (r /\* q) \/* p = (q /\* r) \/* p
AND_OR_COMM_lemma  |- !p q r. p /\* (r \/* q) = p /\* (q \/* r)
OR_COMM_AND_lemma  |- !p q r. (r \/* q) /\* p = (q \/* r) /\* p

OR_COMM_OR_lemma  |- !p q r. (r \/* q) \/* p = (q \/* r) \/* p
OR_OR_COMM_lemma  |- !p q r. p \/* (r \/* q) = p \/* (q \/* r)
AND_COMM_AND_lemma  |- !p q r. (r /\* q) /\* p = (q /\* r) /\* p
AND_AND_COMM_lemma  |- !p q r. p /\* (r /\* q) = p /\* (q /\* r)
OR_AND_COMM_lemma  |- !p q r. p \/* (r /\* q) = p \/* (q /\* r)
NOT_NOT_lemma  |- !p. ~*(~* p) = p
OR_COMM_lemma  |- !p q. p \/* q = q \/* p
OR_OR_lemma  |- !p. p \/* p = p
OR_ASSOC_lemma  |- !p q r. (p \/* q) \/* r = p \/* (q \/* r)
AND_IMPLY_WEAK_lemma  |- !p q s. (p /\* q)s ==> q s
SYM_AND_IMPLY_WEAK_lemma  |- !p q s. (p /\* q)s ==> p s
OR_IMPLY_WEAK_lemma  |- !p q s. p s ==> (p \/* q)s
SYM_OR_IMPLY_WEAK_lemma  |- !p q s. p s ==> (q \/* p)s
IMPLY_WEAK_AND_lemma
  |- !p q r. (!s. p s ==> q s) ==> (!s. (p /\* r)s ==> (q /\* r)s)
IMPLY_WEAK_OR_lemma
  |- !p q r. (!s. p s ==> q s) ==> (!s. (p \/* r)s ==> (q \/* r)s)
AND_AND_lemma  |- !p. p /\* p = p
AND_COMM_lemma  |- !p q. p /\* q = q /\* p
AND_ASSOC_lemma  |- !p q r. (p /\* q) /\* r = p /\* (q /\* r)
AND_TRUE_lemma  |- !p. p /\* TRUE = p
OR_TRUE_lemma  |- !p. p \/* TRUE = TRUE
AND_FALSE_lemma  |- !p. p /\* FALSE = FALSE
OR_FALSE_lemma  |- !p. p \/* FALSE = p
P_OR_NOT_P_lemma  |- !p. p \/* (~* p) = TRUE
P_AND_NOT_P_lemma  |- !p. p /\* (~* p) = FALSE
AND_COMPL_OR_lemma  |- !p q. (p /\* (~* q)) \/* (p /\* q) = p
OR_NOT_AND_lemma  |- !p q. (p \/* q) /\* (~* q) = p /\* (~* q)
P_AND_Q_OR_Q_lemma  |- !p q. (p /\* q) \/* q = q
P_OR_Q_AND_Q_lemma  |- !p q. (p \/* q) /\* q = q
NOT_OR_AND_NOT_lemma  |- !p q. ~*(p \/* q) = (~* p) /\* (~* q)
NOT_AND_OR_NOT_lemma  |- !p q. ~*(p /\* q) = (~* p) \/* (~* q)
NOT_IMPLY_OR_lemma  |- !p q. (!s. ~* p s ==> q s) = (!s. (p \/* q)s)
IMPLY_OR_lemma  |- !p q. (!s. p s ==> q s) = (!s. ((~* p) \/* q)s)
OR_IMPLY_lemma  |- !p q. (!s. (p \/* q)s) = (!s. ~* p s ==> q s)
NOT_OR_IMPLY_lemma  |- !p q. (!s. ((~* p) \/* q)s) = (!s. p s ==> q s)
OR_AND_DISTR_lemma
  |- !p q r. p \/* (q /\* r) = (p \/* q) /\* (p \/* r)
AND_OR_DISTR_lemma
  |- !p q r. p /\* (q \/* r) = (p /\* q) \/* (p /\* r)
NOT_IMPLIES_FALSE_lemma  |- !p. (!s. ~* p s) ==> (!s. p s = FALSE s)
NOT_P_IMPLIES_P_EQ_FALSE_lemma  |- !p. (!s. ~* p s) ==> (p = FALSE)
NOT_AND_IMPLIES_lemma
  |- !p q. (!s. ~*(p /\* q)s) = (!s. p s ==> ~* q s)
NOT_AND_IMPLIES_lemma1
  |- !p q. (!s. ~*(p /\* q)s) ==> (!s. p s ==> ~* q s)
NOT_AND_IMPLIES_lemma2
  |- !p q. (!s. ~*(p /\* q)s) ==> (!s. q s ==> ~* p s)
AND_OR_EQ_lemma  |- !p q. p /\* (p \/* q) = p
AND_OR_EQ_AND_COMM_OR_lemma
  |- !p q. p /\* (q \/* p) = p /\* (p \/* q)
IMPLY_WEAK_lemma  |- !p q. (!s. p s) ==> (!s. (p \/* q)s)
IMPLY_WEAK_lemma_b  |- !p q s. p s ==> (p \/* q)s
ALL_OR_lemma  |- !P i. $?* P = (P i) \/* ($?* P)

ALL_i_OR_lemma  |- !P. (\s. ?i. \<=/* P i s) = $?* P
******************** state_logic ********************

The Theory unless

Parents --  state_logic
Constants --
UNLESS_STMT
  ":(* -> bool) -> ((* -> bool) -> ((* -> *) -> (* -> bool)))"
UNLESS ":(* -> bool) -> ((* -> bool) -> ((* -> *)list -> bool))"
STABLE ":(* -> bool) -> ((* -> *)list -> bool)"
INVARIANT ":(* -> bool) -> ((* -> bool) # (* -> *)list -> bool)"
Infixes --
UNLESS_STMT
  ":(* -> bool) -> ((* -> bool) -> ((* -> *) -> (* -> bool)))"
UNLESS ":(* -> bool) -> ((* -> bool) -> ((* -> *)list -> bool))"
STABLE ":(* -> bool) -> ((* -> *)list -> bool)"
INVARIANT ":(* -> bool) -> ((* -> bool) # (* -> *)list -> bool)"
Definitions --
UNLESS_STMT
  |- !p q st.
      (p UNLESS_STMT q)st = (\s. p s /\ ~q s ==> p(st s) \/ q(st s))
UNLESS
  |- (!p q. (p UNLESS q)[] = T) /\
     (!p q st Pr.
       (p UNLESS q)(CONS st Pr) =
       (!s. (p UNLESS_STMT q)st s) /\ (p UNLESS q)Pr)
STABLE  |- !p Pr. p STABLE Pr = (p UNLESS FALSE)Pr
INVARIANT
  |- !p p0 Pr. p INVARIANT (p0,Pr) = (!s. p0 s ==> p s) /\ p STABLE Pr
Theorems --
UNLESS_STMT_thm0  |- !p st s. (p UNLESS_STMT p)st s
UNLESS_STMT_thm1
  |- !p q r st.
      (!s. (p UNLESS_STMT q)st s) /\ (!s. q s ==> r s) ==>
      (!s. (p UNLESS_STMT r)st s)
UNLESS_STMT_thm2
  |- !p q p' q' st.
      (!s. (p UNLESS_STMT q)st s) /\ (!s. (p' UNLESS_STMT q')st s) ==>
      (!s. ((p \/* p') UNLESS_STMT (q \/* q'))st s)
UNLESS_STMT_thm3
  |- !p q p' q' st.
      (!s. (p UNLESS_STMT q)st s) /\ (!s. (p' UNLESS_STMT q')st s) ==>
      (!s.
        ((p /\* p') UNLESS_STMT
         (((p /\* q') \/* (p' /\* q)) \/* (q /\* q')))
        st
        s)
UNLESS_STMT_thm4
  |- !p q p' q' st.
      (!s. (p UNLESS_STMT q)st s) /\ (!s. (p' UNLESS_STMT q')st s) ==>

(!s.
  ((p \/* p') UNLESS_STMT
   ((((~* p) /\* q') \/* ((~* p') /\* q)) \/* (q /\* q')))
  st
  s)
UNLESS_STMT_thm5
|- !P q st.
(!m s. ((P m) UNLESS_STMT q)st s) ==>
(!s. ((\s. ?n. P n s) UNLESS_STMT q)st s)
UNLESS_thm1  |- !p Pr. (p UNLESS p)Pr
UNLESS_thm2  |- !p Pr. (p UNLESS (~* p))Pr
UNLESS_thm3
|- !p q r Pr. (p UNLESS q)Pr /\ (!s. q s ==> r s) ==> (p UNLESS r)Pr
UNLESS_thm4
|- !p q p' q' Pr.
(p UNLESS q)Pr /\ (p' UNLESS q')Pr ==>
((p /\* p') UNLESS (((p /\* q') \/* (p' /\* q)) \/* (q /\* q')))
Pr
UNLESS_thm5
|- !p q p' q' Pr.
(p UNLESS q)Pr /\ (p' UNLESS q')Pr ==>
((p \/* p') UNLESS
 ((((~* p) /\* q') \/* ((~* p') /\* q)) \/* (q /\* q')))
Pr
UNLESS_thm6
|- !p q p' q' Pr.
(p UNLESS q)Pr /\ (p' UNLESS q')Pr ==>
((p /\* p') UNLESS (q \/* q'))Pr
UNLESS_thm7
|- !p q p' q' Pr.
(p UNLESS q)Pr /\ (p' UNLESS q')Pr ==>
((p \/* p') UNLESS (q \/* q'))Pr
UNLESS_thm8
|- !p q r Pr.
(p UNLESS q)Pr /\ (q UNLESS r)Pr ==> ((p \/* q) UNLESS r)Pr
UNLESS_cor1  |- !p q Pr. (!s. p s ==> q s) ==> (p UNLESS q)Pr
UNLESS_cor2  |- !p q Pr. (!s. ~* p s ==> q s) ==> (p UNLESS q)Pr
UNLESS_cor3
|- !p q r Pr.
((p /\* (~* q)) UNLESS (q \/* r))Pr = (p UNLESS (q \/* r))Pr
UNLESS_cor4
|- !p q r Pr. ((p \/* q) UNLESS r)Pr ==> (p UNLESS (q \/* r))Pr
UNLESS_cor5  |- !p Pr. (p UNLESS TRUE)Pr
UNLESS_cor6  |- !p Pr. (TRUE UNLESS p)Pr
UNLESS_cor7  |- !p Pr. (FALSE UNLESS p)Pr
UNLESS_cor8
|- !p q p' Pr.
(!s. p s /\ ~q s) ==>
(!s. p' s) ==>
(!s. p s \/ q s) ==>
(((p /\* (~* q)) UNLESS q)Pr = ((p' /\* (~* q)) UNLESS q)Pr)
UNLESS_cor9
|- !p q p' q' r r' Pr.
((p \/* p') UNLESS (q \/* r))Pr /\

      ((q \/* q') UNLESS (p \/* r'))Pr ==>
      ((p \/* (p' \/* (q \/* q'))) UNLESS ((p /\* q) \/* (r \/* r')))
      Pr
UNLESS_cor10  |- !p q Pr. (p \/* q) STABLE Pr ==> (p UNLESS q)Pr
UNLESS_cor11  |- !p Pr. (!s. ~* p s) ==> p STABLE Pr
UNLESS_cor12  |- !p Pr. (!s. ~* p s) ==> (~* p) STABLE Pr
UNLESS_cor13
  |- !p q Pr.
      (p UNLESS q)Pr /\ (q UNLESS p)Pr /\ (!s. ~*(p /\* q)s) ==>
      (p \/* q) STABLE Pr
UNLESS_cor14
  |- !p q Pr.
      (p UNLESS (~* q))Pr /\ q STABLE Pr ==>
      (p UNLESS (p /\* (~* q)))Pr
UNLESS_cor15
  |- !P Q Pr.
      (!i. ((P i) UNLESS ((P i) /\* (Q i)))Pr) ==>
      (($!* P) UNLESS (($!* P) /\* ($?* Q)))Pr
UNLESS_cor16
  |- !P Q Pr.
      (!i. ((P i) UNLESS (Q i))Pr) ==>
      (!i. ((/<=\* P i) UNLESS (\<=/* Q i))Pr)
UNLESS_cor17
  |- !P q Pr.
      (!i. ((P i) UNLESS q)Pr) ==> (!i. ((/<=\* P i) UNLESS q)Pr)
UNLESS_cor18
  |- !P q Pr. (!m. ((P m) UNLESS q)Pr) ==> (($?* P) UNLESS q)Pr
UNLESS_cor19  |- !Pr. FALSE STABLE Pr
UNLESS_cor20
  |- !p q Pr. p STABLE Pr /\ q STABLE Pr ==> (p /\* q) STABLE Pr
UNLESS_cor21
  |- !p q Pr. p STABLE Pr /\ q STABLE Pr ==> (p \/* q) STABLE Pr
UNLESS_cor22
  |- !p q r Pr.
      (p UNLESS q)Pr /\ r STABLE Pr ==> ((p /\* r) UNLESS (q /\* r))Pr
******************** unless ********************

The Theory ensures

Parents --  unless
Constants --
EXIST_TRANSITION
  ":(* -> bool) -> ((* -> bool) -> ((* -> *)list -> bool))"
ENSURES ":(* -> bool) -> ((* -> bool) -> ((* -> *)list -> bool))"
Infixes --
EXIST_TRANSITION
  ":(* -> bool) -> ((* -> bool) -> ((* -> *)list -> bool))"
ENSURES ":(* -> bool) -> ((* -> bool) -> ((* -> *)list -> bool))"
Definitions --
EXIST_TRANSITION
  |- (!p q. (p EXIST_TRANSITION q)[] = F) /\
     (!p q st Pr.

       (p EXIST_TRANSITION q)(CONS st Pr) =
       (!s. p s /\ ~q s ==> q(st s)) \/ (p EXIST_TRANSITION q)Pr)
ENSURES
  |- !p q Pr.
      (p ENSURES q)Pr = (p UNLESS q)Pr /\ (p EXIST_TRANSITION q)Pr
Theorems --
EXIST_TRANSITION_thm1
  |- !p q r Pr.
      (p EXIST_TRANSITION q)Pr /\ (!s. q s ==> r s) ==>
      (p EXIST_TRANSITION r)Pr
EXIST_TRANSITION_thm2
  |- !p Pr. (p EXIST_TRANSITION FALSE)Pr ==> (!s. ~* p s)
EXIST_TRANSITION_thm3
  |- !p st Pr. (FALSE EXIST_TRANSITION p)(CONS st Pr)
ENSURES_thm0  |- !p q. (p ENSURES q)[] = F
ENSURES_thm1  |- !p st Pr. (p ENSURES p)(CONS st Pr)
ENSURES_thm2
  |- !p q r Pr.
      (p ENSURES q)Pr /\ (!s. q s ==> r s) ==> (p ENSURES r)Pr
ENSURES_thm3  |- !p Pr. (p ENSURES FALSE)Pr ==> (!s. ~* p s)
ENSURES_thm4
  |- !p q p' q' Pr.
      (p UNLESS q)Pr /\ (p' ENSURES q')Pr ==>
      ((p /\* p') ENSURES
       (((p /\* q') \/* (p' /\* q)) \/* (q /\* q')))
      Pr
ENSURES_thm5
  |- !p q r Pr. (p ENSURES q)Pr ==> ((p \/* r) ENSURES (q \/* r))Pr
ENSURES_cor1
  |- !p q st Pr. (!s. p s ==> q s) ==> (p ENSURES q)(CONS st Pr)
ENSURES_cor2  |- !p q Pr. (p ENSURES q)Pr ==> (p UNLESS q)Pr
ENSURES_cor3
  |- !p q r Pr. ((p \/* q) ENSURES r)Pr ==> (p ENSURES (q \/* r))Pr
ENSURES_cor4
  |- !p q r Pr.
      (p ENSURES (q \/* r))Pr ==> ((p /\* (~* q)) ENSURES (q \/* r))Pr
ENSURES_cor5
  |- !p q r Pr. (p ENSURES q)Pr ==> (p ENSURES (q \/* r))Pr
ENSURES_cor6  |- !p st Pr. (FALSE ENSURES p)(CONS st Pr)
ENSURES_cor7
  |- !p q r Pr.
      (p ENSURES q)Pr /\ r STABLE Pr ==>
      ((p /\* r) ENSURES (q /\* r))Pr
******************** ensures ********************

The Theory gen induct

Parents --  ensures
Theorems --
GEN_INDUCT_lemma1  |- !P. (!m n. n <= m ==> P n) ==> (!m. P m)
GEN_INDUCT_lemma2  |- !m n. n <= m = n < (SUC m)

GEN_INDUCT_lemma3
  |- !P. (!m. (!n. n < m ==> P n) ==> P m) ==> (!m n. n <= m ==> P n)
GEN_INDUCT_thm  |- !P. (!m. (!n. n < m ==> P n) ==> P m) ==> (!m. P m)
******************** gen_induct ********************

The Theory leadsto

Parents --  gen_induct
Constants --
In ":(* -> bool) -> (((* -> bool) -> bool) -> bool)"
LEADSTO ":(* -> bool) -> ((* -> bool) -> ((* -> *)list -> bool))"
EQmetric ":(* -> num) -> (num -> (* -> bool))"
LESSmetric ":(* -> num) -> (num -> (* -> bool))"
LUB ":((* -> bool) -> bool) -> (* -> bool)"
LeadstoRel
  ":((* -> bool) -> ((* -> bool) -> ((* -> *)list -> bool))) ->
    ((* -> *)list -> bool)"
LEADSTO2Fn
  ":((* -> bool) -> ((* -> bool) -> ((* -> *)list -> bool))) ->
    ((* -> bool) -> ((* -> bool) -> ((* -> *)list -> bool)))"
LEADSTO2 ":(* -> bool) -> ((* -> bool) -> ((* -> *)list -> bool))"
LEADSTO2Fam
  ":((* -> bool) -> ((* -> bool) -> ((* -> *)list -> bool))) ->
    ((* -> *)list -> bool)"
Infixes --
In ":(* -> bool) -> (((* -> bool) -> bool) -> bool)"
LEADSTO ":(* -> bool) -> ((* -> bool) -> ((* -> *)list -> bool))"
EQmetric ":(* -> num) -> (num -> (* -> bool))"
LESSmetric ":(* -> num) -> (num -> (* -> bool))"
Definitions --
LUB  |- !P. LUB P = (\s. ?p. P p /\ p s)
In  |- !p P. p In P = P p
LeadstoRel
  |- !R Pr.
      LeadstoRel R Pr =
      (!p q.
        ((p ENSURES q)Pr ==> R p q Pr) /\
        (!r. R p r Pr /\ R r q Pr ==> R p q Pr) /\
        (!P. (p = LUB P) /\ (!p'. p' In P ==> R p' q Pr) ==> R p q Pr))
LEADSTO
  |- !p q Pr. (p LEADSTO q)Pr = (!R. LeadstoRel R Pr ==> R p q Pr)
LEADSTO2Fn
  |- !R.
      LEADSTO2Fn R =
      (\p q Pr.
        (p ENSURES q)Pr \/
        (?r. (p ENSURES r)Pr /\ R r q Pr) \/
        (?P. (p = LUB P) /\ (!p'. p' In P ==> R p' q Pr)))
LEADSTO2
  |- !p q Pr.
      LEADSTO2 p q Pr =
      (!R.

  (!p' q'. LEADSTO2Fn R p' q' Pr ==> R p' q' Pr) ==> R p q Pr)
LEADSTO2Fam
|- !R Pr.
LEADSTO2Fam R Pr =
(!p q.
  ((p ENSURES q)Pr ==> R p q Pr) /\
  (!r. (p ENSURES r)Pr /\ R r q Pr ==> R p q Pr) /\
  (!P. (!p'. p' In P ==> R p' q Pr) ==> R(LUB P)q Pr))
EQmetric  |- !M m. M EQmetric m = (\s. M s = m)
LESSmetric  |- !M m. M LESSmetric m = (\s. (M s) < m)
Theorems --
LEADSTO_thm0  |- !p q Pr. (p ENSURES q)Pr ==> (p LEADSTO q)Pr
LEADSTO_thm1
|- !p r q Pr. (p LEADSTO r)Pr /\ (r LEADSTO q)Pr ==> (p LEADSTO q)Pr
LEADSTO_thm2
|- !p r q Pr. (p ENSURES r)Pr /\ (r LEADSTO q)Pr ==> (p LEADSTO q)Pr
LEADSTO_thm2a
|- !p r q Pr. (p ENSURES r)Pr /\ (r ENSURES q)Pr ==> (p LEADSTO q)Pr
LEADSTO_thm3
|- !p P q Pr.
(p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr) ==>
(p LEADSTO q)Pr
LEADSTO_thm3a
|- !P q Pr.
(!p. p In P ==> (p LEADSTO q)Pr) ==> ((LUB P) LEADSTO q)Pr
LEADSTO_thm3c
|- !P q Pr. (!i. ((P i) LEADSTO q)Pr) ==> (($?* P) LEADSTO q)Pr
LEADSTO_thm4
|- !p1 p2 q Pr.
(p1 LEADSTO q)Pr /\ (p2 LEADSTO q)Pr ==>
((p1 \/* p2) LEADSTO q)Pr
LEADSTO_thm5
|- !p q Pr.
(p ENSURES q)Pr \/
(?r. (p LEADSTO r)Pr /\ (r LEADSTO q)Pr) \/
(?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr)) =
(p LEADSTO q)Pr
LEADSTO_thm6
|- !p q Pr.
(p ENSURES q)Pr \/
(?r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr) \/
(?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr)) =
(p LEADSTO q)Pr
LEADSTO_thm7
|- !p q Pr.
(p ENSURES q)Pr \/
(?r. (p ENSURES r)Pr /\ (r ENSURES q)Pr) \/
(?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr)) =
(p LEADSTO q)Pr
LEADSTO_thm8
|- !p q Pr.
(p ENSURES q)Pr \/
(?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr)) =

(p LEADSTO q)Pr
LEADSTO_thm9
|- !p q Pr.
(?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr)) =
(p LEADSTO q)Pr
LEADSTO_thm11
|- !p q st Pr.
(?r. (p ENSURES r)(CONS st Pr) /\ (r LEADSTO q)(CONS st Pr)) =
(p LEADSTO q)(CONS st Pr)
LEADSTO_thm12  |- !p st Pr. (p LEADSTO p)(CONS st Pr)
LEADSTO_thm13
|- !p q st Pr.
(?r. (p LEADSTO r)(CONS st Pr) /\ (r LEADSTO q)(CONS st Pr)) =
(p LEADSTO q)(CONS st Pr)
LEADSTO_thm14
|- !p q st Pr.
(?r. (p LEADSTO r)(CONS st Pr) /\ (r LEADSTO q)(CONS st Pr)) =
(?r. (p ENSURES r)(CONS st Pr) /\ (r LEADSTO q)(CONS st Pr))
LEADSTO_thm15
|- !p q Pr.
(p ENSURES q)Pr \/
(!r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr) \/
(?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr)) =
(p LEADSTO q)Pr
LEADSTO_thm16
|- !p q Pr.
(!r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr) \/
(?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr)) =
(p LEADSTO q)Pr
LEADSTO_thm17
|- !X p q Pr.
(!p q.
  ((p ENSURES q)Pr ==> X p q Pr) /\
  (!r.
    (p LEADSTO r)Pr /\
    ((p LEADSTO r)Pr ==> X p r Pr) /\
    (r LEADSTO q)Pr /\
    ((r LEADSTO q)Pr ==> X r q Pr) ==>
    (p LEADSTO q)Pr ==>
    X p q Pr) /\
  (!P.
    (!p. p In P ==> (p LEADSTO q)Pr) /\
    (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr) ==>
    ((LUB P) LEADSTO q)Pr ==>
    X(LUB P)q Pr)) ==>
(p LEADSTO q)Pr ==>
X p q Pr
LEADSTO_thm18
|- !X.
(!p q Pr. (p ENSURES q)Pr ==> X p q Pr) /\
(!p r q Pr.
  (p LEADSTO r)Pr /\
  ((p LEADSTO r)Pr ==> X p r Pr) /\
  (r LEADSTO q)Pr /\

((r LEADSTO q)Pr ==> X r q Pr) ==>
(p LEADSTO q)Pr ==>
X p q Pr) /\
(!p P q Pr.
(!p. p In P ==> (p LEADSTO q)Pr) /\
(!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr) ==>
((LUB P) LEADSTO q)Pr ==>
X(LUB P)q Pr) ==>
(!p q Pr. (p LEADSTO q)Pr ==> X p q Pr)
LEADSTO_thm19
|- !X p q Pr.
(!p q.
((p ENSURES q)Pr ==> X p q Pr) /\
(!r.
  (p LEADSTO r)Pr /\ X p r Pr /\ (r LEADSTO q)Pr /\ X r q Pr ==>
  (p LEADSTO q)Pr ==>
  X p q Pr) /\
(!P.
  (!p. p In P ==> (p LEADSTO q)Pr) /\
  (!p. p In P ==> X p q Pr) ==>
  ((LUB P) LEADSTO q)Pr ==>
  X(LUB P)q Pr)) ==>
(p LEADSTO q)Pr ==>
X p q Pr
LEADSTO_thm20
|- !X.
(!p q Pr. (p ENSURES q)Pr ==> X p q Pr) /\
(!p r q Pr.
(p LEADSTO r)Pr /\ X p r Pr /\ (r LEADSTO q)Pr /\ X r q Pr ==>
(p LEADSTO q)Pr ==>
X p q Pr) /\
(!p P q Pr.
(!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr) ==>
((LUB P) LEADSTO q)Pr ==>
X(LUB P)q Pr) ==>
(!p q Pr. (p LEADSTO q)Pr ==> X p q Pr)
LEADSTO_thm21
|- !X p q Pr.
(!p q.
((p ENSURES q)Pr ==> X p q Pr) /\
(!r. X p r Pr /\ X r q Pr ==> X p q Pr) /\
(!P. (p = LUB P) /\ (!p. p In P ==> X p q Pr) ==> X p q Pr)) ==>
(p LEADSTO q)Pr ==>
X p q Pr
LEADSTO_thm22
|- !X.
(!p q Pr. (p ENSURES q)Pr ==> X p q Pr) /\
(!p r q Pr. X p r Pr /\ X r q Pr ==> X p q Pr) /\
(!p P q Pr.
(p = LUB P) /\ (!p. p In P ==> X p q Pr) ==> X p q Pr) ==>
(!p q Pr. (p LEADSTO q)Pr ==> X p q Pr)
LEADSTO_thm23
|- !X Pr.
(!p q.

  ((p ENSURES q)Pr ==> X p q Pr) /\
  (!r.
    (p LEADSTO r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr ==>
    X p q Pr) /\
  (!P.
    (p = LUB P) /\
    (!p. p In P ==> (p LEADSTO q)Pr) /\
    (!p. p In P ==> X p q Pr) ==>
    X p q Pr)) ==>
(!p q. (p LEADSTO q)Pr ==> X p q Pr)
LEADSTO_thm24
|- !X Pr.
(!p q.
  ((p ENSURES q)Pr ==> X p q Pr) /\
  (!r.
    (p LEADSTO r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr ==>
    X p q Pr) /\
  (!P.
    (!p. p In P ==> (p LEADSTO q)Pr) /\
    (!p. p In P ==> X p q Pr) ==>
    X(LUB P)q Pr)) ==>
(!p q. (p LEADSTO q)Pr ==> X p q Pr)
LEADSTO_thm25
|- !p q st Pr. (!s. p s ==> q s) ==> (p LEADSTO q)(CONS st Pr)
LEADSTO_thm26
|- !p q q' st Pr.
(p LEADSTO q)(CONS st Pr) ==> (p LEADSTO (q \/* q'))(CONS st Pr)
LEADSTO_thm27
|- !p q p' q' st Pr.
(p LEADSTO q)(CONS st Pr) /\ (p' LEADSTO q')(CONS st Pr) ==>
((p \/* p') LEADSTO (q \/* q'))(CONS st Pr)
LEADSTO_thm28
|- !p q b r st Pr.
(p LEADSTO (q \/* b))(CONS st Pr) /\ (b LEADSTO r)(CONS st Pr) ==>
(p LEADSTO (q \/* r))(CONS st Pr)
LEADSTO_thm29
|- !p q r b st Pr.
(p LEADSTO q)(CONS st Pr) /\ (r UNLESS b)(CONS st Pr) ==>
((p /\* r) LEADSTO ((q /\* r) \/* b))(CONS st Pr)
LEADSTO_thm30
|- !p st Pr. (p LEADSTO FALSE)(CONS st Pr) ==> (!s. ~* p s)
LEADSTO_cor1
|- !p b q Pr.
((p /\* b) LEADSTO q)Pr /\ ((p /\* (~* b)) LEADSTO q)Pr ==>
(p LEADSTO q)Pr
LEADSTO_cor2
|- !p q r st Pr.
(p LEADSTO q)(CONS st Pr) /\ r STABLE (CONS st Pr) ==>
((p /\* r) LEADSTO (q /\* r))(CONS st Pr)
LEADSTO_cor3
|- !p q st Pr.
(p LEADSTO q)(CONS st Pr) =
((p /\* (~* q)) LEADSTO q)(CONS st Pr)
LEADSTO_cor4

|- !p b q st Pr.
((p /\* b) LEADSTO q)(CONS st Pr) /\
((p /\* (~* b)) LEADSTO ((p /\* b) \/* q))(CONS st Pr) ==>
(p LEADSTO q)(CONS st Pr)
LEADSTO_cor5
|- !p q r st Pr.
((p /\* q) LEADSTO r)(CONS st Pr) ==>
(p LEADSTO ((~* q) \/* r))(CONS st Pr)
LEADSTO_cor6
|- !p q r st Pr.
(p LEADSTO q)(CONS st Pr) /\ (r UNLESS (q /\* r))(CONS st Pr) ==>
((p /\* r) LEADSTO (q /\* r))(CONS st Pr)
LEADSTO_cor7
|- !p q r st Pr.
(p LEADSTO q)(CONS st Pr) /\ (r /\* (~* q)) STABLE (CONS st Pr) ==>
(!s. (p /\* r)s ==> q s)
LEADSTO_cor8
|- !p r q st Pr.
(p LEADSTO r)(CONS st Pr) ==> ((p /\* q) LEADSTO r)(CONS st Pr)
LEADSTO_cor9
|- !p q r st Pr.
(p LEADSTO q)(CONS st Pr) /\ (!s. q s ==> r s) ==>
(p LEADSTO r)(CONS st Pr)
LEADSTO_cor10
|- !P q Pr.
(!i. ((P i) LEADSTO q)Pr) ==> (!i. ((\<=/* P i) LEADSTO q)Pr)
LEADSTO_cor11  |- !p st Pr. (FALSE LEADSTO p)(CONS st Pr)
LEADSTO_cor12
|- !P q st Pr.
(!i. ((P i) LEADSTO q)(CONS st Pr)) ==>
(!i. ((\</* P i) LEADSTO q)(CONS st Pr))
LEADSTO2_thm0  |- !p q Pr. (p ENSURES q)Pr ==> LEADSTO2 p q Pr
LEADSTO2_thm1
|- !p r q Pr. (p ENSURES r)Pr /\ LEADSTO2 r q Pr ==> LEADSTO2 p q Pr
LEADSTO2_thm3
|- !P q Pr. (!p. p In P ==> LEADSTO2 p q Pr) ==> LEADSTO2(LUB P)q Pr
LEADSTO2_thm3a
|- !P q Pr.
(p = LUB P) /\ (!p. p In P ==> LEADSTO2 p q Pr) ==>
LEADSTO2 p q Pr
LEADSTO2_thm4
|- !p1 p2 q Pr.
LEADSTO2 p1 q Pr /\ LEADSTO2 p2 q Pr ==> LEADSTO2(p1 \/* p2)q Pr
LEADSTO2_thm8
|- !X p q Pr.
(!p q.
  ((p ENSURES q)Pr ==> X p q Pr) /\
  (!r. (p ENSURES r)Pr /\ X r q Pr ==> X p q Pr) /\
  (!P. (!p. p In P ==> X p q Pr) ==> X(LUB P)q Pr)) ==>
LEADSTO2 p q Pr ==>
X p q Pr
LEADSTO2_thm2
|- !p r q Pr. LEADSTO2 p r Pr /\ LEADSTO2 r q Pr ==> LEADSTO2 p q Pr
LEADSTO2_thm5

|- !p q Pr.
(p ENSURES q)Pr \/
(?r. LEADSTO2 p r Pr /\ LEADSTO2 r q Pr) \/
(?P. (p = LUB P) /\ (!p. p In P ==> LEADSTO2 p q Pr)) =
LEADSTO2 p q Pr
LEADSTO2_thm6
|- !p q Pr.
(p ENSURES q)Pr \/
(?r. (p ENSURES r)Pr /\ LEADSTO2 r q Pr) \/
(?P. (p = LUB P) /\ (!p. p In P ==> LEADSTO2 p q Pr)) =
LEADSTO2 p q Pr
LEADSTO2_thm7
|- !X p q Pr.
(!p q.
  ((p ENSURES q)Pr ==> X p q Pr) /\
  (!r.
    (p ENSURES r)Pr /\
    LEADSTO2 r q Pr /\
    (LEADSTO2 r q Pr ==> X r q Pr) ==>
    LEADSTO2 p q Pr ==>
    X p q Pr) /\
  (!P.
    (!p. p In P ==> LEADSTO2 p q Pr) /\
    (!p. p In P ==> LEADSTO2 p q Pr ==> X p q Pr) ==>
    LEADSTO2(LUB P)q Pr ==>
    X(LUB P)q Pr)) ==>
LEADSTO2 p q Pr ==>
X p q Pr
LEADSTO_EQ_LEADSTO2  |- !p q Pr. (p LEADSTO q)Pr = LEADSTO2 p q Pr
LEADSTO_thm31
|- !X p q Pr.
(!p q.
  ((p ENSURES q)Pr ==> X p q Pr) /\
  (!r. (p ENSURES r)Pr /\ X r q Pr ==> X p q Pr) /\
  (!P. (!p. p In P ==> X p q Pr) ==> X(LUB P)q Pr)) ==>
(p LEADSTO q)Pr ==>
X p q Pr
LEADSTO_thm32
|- !X.
(!p q Pr. (p ENSURES q)Pr ==> X p q Pr) /\
(!p r q Pr. (p ENSURES r)Pr /\ X r q Pr ==> X p q Pr) /\
(!P q Pr. (!p. p In P ==> X p q Pr) ==> X(LUB P)q Pr) ==>
(!p q Pr. (p LEADSTO q)Pr ==> X p q Pr)
LEADSTO_thm33
|- !X p q Pr.
(!p q.
  ((p ENSURES q)Pr ==> X p q Pr) /\
  (!r.
    (p ENSURES r)Pr /\
    (r LEADSTO q)Pr /\
    ((r LEADSTO q)Pr ==> X r q Pr) ==>
    (p LEADSTO q)Pr ==>
    X p q Pr) /\
  (!P.

    (!p. p In P ==> (p LEADSTO q)Pr) /\
    (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr) ==>
    ((LUB P) LEADSTO q)Pr ==>
    X(LUB P)q Pr)) ==>
(p LEADSTO q)Pr ==>
X p q Pr
LEADSTO_thm34
|- !X.
(!p q Pr. (p ENSURES q)Pr ==> X p q Pr) /\
(!p r q Pr.
  (p ENSURES r)Pr /\
  (r LEADSTO q)Pr /\
  ((r LEADSTO q)Pr ==> X r q Pr) ==>
  (p LEADSTO q)Pr ==>
  X p q Pr) /\
(!P q Pr.
  (!p. p In P ==> (p LEADSTO q)Pr) /\
  (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr) ==>
  ((LUB P) LEADSTO q)Pr ==>
  X(LUB P)q Pr) ==>
(!p q Pr. (p LEADSTO q)Pr ==> X p q Pr)
LEADSTO_thm34a
|- !X Pr.
(!p q. (p ENSURES q)Pr ==> X p q Pr) /\
(!p r q.
  (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ X r q Pr ==> X p q Pr) /\
(!P q.
  (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr) ==>
  X(LUB P)q Pr) ==>
(!p q. (p LEADSTO q)Pr ==> X p q Pr)
LEADSTO_thm34b
|- !X.
(!p q st Pr. (p ENSURES q)(CONS st Pr) ==> X p q(CONS st Pr)) /\
(!p r q st Pr.
  (p ENSURES r)(CONS st Pr) /\
  (r LEADSTO q)(CONS st Pr) /\
  X r q(CONS st Pr) ==>
  X p q(CONS st Pr)) /\
(!P q st Pr.
  (!p. p In P ==> (p LEADSTO q)(CONS st Pr)) /\
  (!p. p In P ==> X p q(CONS st Pr)) ==>
  X(LUB P)q(CONS st Pr)) ==>
(!p q st Pr. (p LEADSTO q)(CONS st Pr) ==> X p q(CONS st Pr))
LEADSTO_thm35
|- !p q p' q' r st Pr.
(p LEADSTO q)(CONS st Pr) /\
(p' LEADSTO q')(CONS st Pr) /\
(q UNLESS r)(CONS st Pr) /\
(q' UNLESS r)(CONS st Pr) ==>
((p /\* p') LEADSTO ((q /\* q') \/* r))(CONS st Pr)
LEADSTO_thm36
|- !p q st Pr M.
(!m.
  ((p /\* (M EQmetric m)) LEADSTO

 ((p /\* (M LESSmetric m)) \/* q))
(CONS st Pr)) ==>
(p LEADSTO q)(CONS st Pr)
LEADSTO_thm37
|- !X p q Pr.
(!p q.
((p ENSURES q)Pr ==> X p q) /\
(!r.
  (p LEADSTO r)Pr /\ X p r /\ (r LEADSTO q)Pr /\ X r q ==>
  X p q) /\
(!P.
  (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q) ==>
  X(LUB P)q)) ==>
(p LEADSTO q)Pr ==>
X p q
LEADSTO_thm38
|- !X.
(!p q Pr. (p ENSURES q)Pr ==> X p q) /\
(!p r q Pr.
(p LEADSTO r)Pr /\ X p r /\ (r LEADSTO q)Pr /\ X r q ==> X p q) /\
(!P q Pr.
(!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q) ==>
X(LUB P)q) ==>
(!p q Pr. (p LEADSTO q)Pr ==> X p q)
LEADSTO_thm39
|- !X p q Pr.
(!p q.
((p ENSURES q)Pr ==> X p q) /\
(!r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ X r q ==> X p q) /\
(!P.
  (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q) ==>
  X(LUB P)q)) ==>
(p LEADSTO q)Pr ==>
X p q
LEADSTO_thm40
|- !X.
(!p q Pr. (p ENSURES q)Pr ==> X p q) /\
(!p r q Pr.
(p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ X r q ==> X p q) /\
(!P q Pr.
(!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q) ==>
X(LUB P)q) ==>
(!p q Pr. (p LEADSTO q)Pr ==> X p q)
LEADSTO_thm41
|- !X.
(!p q Pr. (p ENSURES q)Pr ==> X p q Pr) /\
(!p r q Pr.
(p LEADSTO r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr ==>
X p q Pr) /\
(!p P q Pr.
(p = LUB P) /\
(!p. p In P ==> (p LEADSTO q)Pr) /\
(!p. p In P ==> X p q Pr) ==>
X p q Pr) ==>

(!p q Pr. (p LEADSTO q)Pr ==> X p q Pr)
LEADSTO_thm42
|- !X Pr.
(!p q.
  ((p ENSURES q)Pr ==> X p q Pr) /\
  (!r.
    (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr ==>
    X p q Pr) /\
  (!P.
    (p = LUB P) /\
    (!p. p In P ==> (p LEADSTO q)Pr) /\
    (!p. p In P ==> X p q Pr) ==>
    X p q Pr)) ==>
(!p q. (p LEADSTO q)Pr ==> X p q Pr)
LEADSTO_thm43
|- !X.
(!p q Pr. (p ENSURES q)Pr ==> X p q Pr) /\
(!p r q Pr.
  (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr ==>
  X p q Pr) /\
(!p P q Pr.
  (p = LUB P) /\
  (!p. p In P ==> (p LEADSTO q)Pr) /\
  (!p. p In P ==> X p q Pr) ==>
  X p q Pr) ==>
(!p q Pr. (p LEADSTO q)Pr ==> X p q Pr)
LEADSTO_cor13
|- !P Q r st Pr.
(!i. ((P i) LEADSTO ((Q i) \/* r))(CONS st Pr)) /\
(!i. ((Q i) UNLESS r)(CONS st Pr)) ==>
(!i. ((/<=\* P i) LEADSTO ((/<=\* Q i) \/* r))(CONS st Pr))
LEADSTO_cor14
|- !p q r p' q' st Pr.
(p LEADSTO (q \/* r))(CONS st Pr) /\
(q UNLESS r)(CONS st Pr) /\
(p' LEADSTO (q' \/* r))(CONS st Pr) /\
(q' UNLESS r)(CONS st Pr) ==>
((p /\* p') LEADSTO ((q /\* q') \/* r))(CONS st Pr)
LEADSTO_cor15
|- !p q r b p' q' r' b' st Pr.
(p LEADSTO (q \/* r))(CONS st Pr) /\
(q UNLESS b)(CONS st Pr) /\
(p' LEADSTO (q' \/* r'))(CONS st Pr) /\
(q' UNLESS b')(CONS st Pr) ==>
((p /\* p') LEADSTO
 ((q /\* q') \/* ((r \/* b) \/* (r' \/* b'))))
(CONS st Pr)
LEADSTO_cor16
|- !P Q R B st Pr.
(!i. ((P i) LEADSTO ((Q i) \/* (R i)))(CONS st Pr)) /\
(!i. ((Q i) UNLESS (B i))(CONS st Pr)) ==>
(!i.
  ((/<=\* P i) LEADSTO
   ((/<=\* Q i) \/* ((\<=/* R i) \/* (\<=/* B i))))

  (CONS st Pr))
******************** leadsto ********************

The Theory comp unity

Parents --  leadsto
Theorems --
COMP_UNLESS_thm1
|- !p q FPr GPr.
(p UNLESS q)(APPEND FPr GPr) =
(p UNLESS q)FPr /\ (p UNLESS q)GPr
COMP_ENSURES_thm1
|- !p q FPr GPr.
(p ENSURES q)(APPEND FPr GPr) =
(p ENSURES q)FPr /\ (p UNLESS q)GPr \/
(p ENSURES q)GPr /\ (p UNLESS q)FPr
COMP_ENSURES_cor0
|- !p q FPr GPr.
(p ENSURES q)FPr /\ (p UNLESS q)GPr ==>
(p ENSURES q)(APPEND FPr GPr)
COMP_ENSURES_cor1
|- !p q FPr GPr.
(p ENSURES q)GPr /\ (p UNLESS q)FPr ==>
(p ENSURES q)(APPEND FPr GPr)
COMP_UNITY_cor0
|- !p0 p FPr GPr.
p INVARIANT (p0,APPEND FPr GPr) =
p INVARIANT (p0,FPr) /\ p INVARIANT (p0,GPr)
COMP_UNITY_cor1
|- !p FPr GPr.
p STABLE (APPEND FPr GPr) = p STABLE FPr /\ p STABLE GPr
COMP_UNITY_cor2
|- !p q FPr GPr.
(p UNLESS q)FPr /\ p STABLE GPr ==> (p UNLESS q)(APPEND FPr GPr)
COMP_UNITY_cor3
|- !p0 p FPr GPr.
p INVARIANT (p0,FPr) /\ p STABLE GPr ==>
p INVARIANT (p0,APPEND FPr GPr)
COMP_UNITY_cor4
|- !p q FPr GPr.
(p ENSURES q)FPr /\ p STABLE GPr ==>
(p ENSURES q)(APPEND FPr GPr)
COMP_UNITY_cor5
|- !p q FPr GPr. (p UNLESS q)(APPEND FPr GPr) ==> (p UNLESS q)GPr
COMP_UNITY_cor6
|- !p q FPr GPr. (p UNLESS q)(APPEND FPr GPr) ==> (p UNLESS q)FPr
COMP_UNITY_cor7
|- !p q st FPr. (p UNLESS q)(CONS st FPr) ==> (p UNLESS q)FPr
COMP_UNITY_cor8
|- !p FPr GPr.
(p ENSURES (~* p))FPr ==> (p ENSURES (~* p))(APPEND FPr GPr)
COMP_UNITY_cor9

|- !p q FPr GPr.
    p STABLE FPr /\ (p UNLESS q)GPr ==> (p UNLESS q)(APPEND FPr GPr)
COMP_UNITY_cor10
|- !p q FPr GPr.
    (p UNLESS q)(APPEND FPr GPr) = (p UNLESS q)(APPEND GPr FPr)
COMP_UNITY_cor11
|- !p q FPr GPr.
    (p ENSURES q)(APPEND FPr GPr) = (p ENSURES q)(APPEND GPr FPr)
COMP_UNITY_cor12
|- !p q Pr1 Pr2.
    (p LEADSTO q)(APPEND Pr1 Pr2) = (p LEADSTO q)(APPEND Pr2 Pr1)
COMP_UNITY_cor13
|- !p FPr GPr. p STABLE (APPEND FPr GPr) = p STABLE (APPEND GPr FPr)
COMP_UNITY_cor14
|- !p0 p FPr GPr.
    p INVARIANT (p0,APPEND FPr GPr) =
    p INVARIANT (p0,APPEND GPr FPr)
******************** comp_unity ********************

Bibliography

[And92] Flemming Andersen. A Theorem Prover for UNITY in Higher Order Logic. PhD thesis, Technical University of Denmark, 1992.

[AP91] Flemming Andersen and Kim Dam Petersen. Recursive Boolean Functions in HOL. In 1991 International Workshop on the HOL Theorem Proving System and its Applications, pages 367–377. IEEE Computer Society, August 1991.

[BA90] R.J.R Back and S. Agerholm. Predicate Transformers and typed λcalculus. In 2nd Nordic Workshop on Program Correctness, October 1990.

[CM88] K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison–Wesley, 1988.

[Dij76] Edsger W. Dijkstra. A Discipline of Programming. Series in Automatic Computation. Prentice–Hall, Inc., 1976.

[GGS88] Stephen Garland, John Guttag, and Jørgen Staunstrup. Verification of VLSI circuits using LP. Technical report, DAIMI PB-258, University of Århus, Denmark, July 1988.

[Gor87a] Michael J.C. Gordon. HOL - A Proof Generating System for Higher-Order Logic. Cambridge University, Computer Laboratory, 1987.

[Gor87b] Gordon et. al. The HOL Manual. Technical report, Computer Laboratory, Cambridge University, June 1987.

[GQNL90] P. Grønning, T. Quist Nielsen, and Hans Henrik Løvengreen. Refinement and Composition of Transition-based Rely-Guarantee Specifications with Auxiliary Variables. Submitted for publication, 1990.

[Hoa69] C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580, 1969.

[Mel88] T.F. Melham. Automating Recursive Type Definitions in Higher Order Logic. Technical Report No. 146, Computer Laboratory, University of Cambridge, September 1988.

[Mis90] Jayadev Misra. Soundness of the Substitution Axiom. Notes on UNITY, March 1990.

[OL82] S. Owicki and L. Lamport. Proving Liveness Properties of Concurrent Programs. ACM Transactions on Programming Languages and Systems, 4(3), July 1982.

[San91] Beverly A. Sanders. Eliminating the Substitution Axiom from UNITY Logic. Formal Aspects of Computing, 3(2):189–205, April-June 1991.

[Sta85] E.W. Stark. A Proof Technique for Rely/Guarantee Properties, pages 369– 391. LNCS 206. Springer–Verlag, 1985.

[Tar55] Alfred Tarski. A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics, 5:285–309, 1955.