1. Introduction

This draft presents an introduction to the use of PVS for validating algorithms and abstract data types.

./tex2code.pl < pvsintro.tex

2. The maximum of a set of numbers

An algorithm for computing the maximum of a set of numbers is presented in [?]. Misra presents both operational and non-operational descriptions for that same algorithm, using the logic of UNITY. That description essentially establishes relation between the states of program to be defined. That description is reproduced below, followed by a PVS encoding of it.

3. A UNITY description

Fact: An execution of a program can be represented as a sequence of states.

• state: a state of a program is an assignment of values to all its variables.

• action: a temporal logic expression defining a relation between old states and new states. For example,

p co q

that states (using Hoare triples)

∀α.{p} α {q

if p is true of a given state, after any action of the system in that state, q will hold in the resulting state q.

An action is a logical relation constraining the transitions, or updates in the language of [?]. (I’ll use the terms transition and update to designate synonyms for the usual step of a program, and say that actions constraining the transitions/steps of a program.)

A logical description of a program defines a set of conditions that any implementation of it should satisfy. Misra, in [?, ?], uses a formal system (called UNITY), which combines a temporal logic to present logical descriptions of programs and a language (whose semantics is expressed in the logic of UNITY) for representing operational descriptions of programs. As an example, he introduces a program for computing the maximum of a set of numbers as given in 1. Notice the use of the operator co described above.

Algorithm 1.

\underline{program} max \underline{initially} v = 0 α : v = m co v = m ∨ (v ∈ S ∧ v > m) β : m ∈ S ⇝ v ≥ m

In a logical description, the steps to be performed are described through predicates that represent logical relation between states. In a sense, 1 above describes a family of programs. The programs in that family should obey the following conditions:

• \underline{initially} v = 0 Before any computation v must be initialized to 0.

• v = m co v = m ∨ (v ∈ S ∧ v > m)

which states that ∀m.∀α : {v = m} α {v = m ∨ (v ∈ S ∧ v > m) For any transition in this program, if v equals m before the transition, then after it either v is still equal to m or it has been changed to some value from S and v > m.

• m ∈ S ⇝ v ≥ m

that establishes that for any m if m ∈ S in a given state, then eventually v will be greater or equal than m.

4. A PVS description

The algorithm is coded here as PVS theory. The first line defines that the theory is called max.

1 max : THEORY
2  BEGIN

Next two lines define:

• v: that identify the maximum at the end of computation.

• S: the set whose maximum is being searched.

3  v : nat;
4  S  : setof[nat];

UNITY’s co operator relates a state with its successor. A state will be understood as a map from variables to values [?]. However, because PVS doesn’t have temporal operators, and a relation on sequences of states must be expressed, the concept of state will be modeled through a function mapping pairs of integers to integers:

• st represents the state function. Given a non-negative integer representing the states (states are numbered from 0), and the variable v (another non-negative integer), it returns the value of v in the respective state.

5  st : [nat,nat->nat];

The axiom INIT defines the initial state (thus, 0) of the computation. In state 0, v has value 0.

6  INIT: AXIOM st(0,v)=0;

Axiom NEXT relates the value of v in state i (say m) to its value in the succeeding state (i + 1), which must be either m or some number greater than m and contained in S.

7  NEXT: AXIOM forall (i:nat,m:nat): st(i,v)=m IMPLIES
8  (st(i+1,v)=m OR
9  (st(i+1,v)>m AND S(st(i+1,v))))

Next the formula STABLE is introduced. A formula is a conjecture that must be proved. This conjecture in particular states a stability property: that if v is greater than some n in a state, it will still be grater than n in the succeeding state.

10  STABLE: FORMULA forall(i:nat,n:nat): st(i,v)>=n IMPLIES
11  st(i+1,v)>=n

12 13

14 END max

15

The PVS proof follows. Verbose proof for STABLE.

STABLE:

{1} ∀ (i: nat, n: nat): st(i, v) ≥ n ⊃ st(i + 1, v) ≥ n

Skolemizing,

STABLE:

{1} st(i′, v) ≥ n′ ⊃ st(i′ + 1, v) ≥ n′

Applying disjunctive simplification to flatten sequent,

STABLE:

\begin{matrix}\{-1\} & st(i′, v) ≥ n′ \\ \{1\} & st(i′ + 1, v) ≥ n′ \end{matrix}

Using n_{0} to name and replace st(i′, v),

STABLE:

\begin{matrix}\{-1\} & st(i′, v) = n_{0} \\ \{-2\} & n_{0} ≥ n′ \\ \{1\} & st(i′ + 1, v) ≥ n′ \end{matrix}

Forward chaining on NEXT, we get 2 subgoals:

STABLE.1:

\begin{matrix}\{-1\} & st(i′ + 1, v) = n_{0} \\ \{-2\} & st(i′, v) = n_{0} \\ \{-3\} & n_{0} ≥ n′ \\ \{1\} & st(i′ + 1, v) ≥ n′ \end{matrix}

Trying repeated skolemization, instantiation, and if-lifting, This completes the proof of STABLE.1.

STABLE.2:

{-1} st(i′ + 1, v) > n_{0}
{-2} S(st(i′ + 1, v))
{-3} st(i′, v) = n_{0}
{-4} n_{0} ≥ n′
{1} st(i′ + 1, v) ≥ n′

Trying repeated skolemization, instantiation, and if-lifting, This completes the proof of STABLE.2. Q.E.D.

5. A first abstract data type

16 stacks [t: TYPE+] : THEORY
17  BEGIN

18

19  stack : TYPE+
20  s : VAR stack
21  empty : stack
22  nonemptystack?(s) : bool = s /= empty
23  nonemptystack_exists: AXIOM EXISTS s: nonemptystack?(s)

24

25  push: [t, stack -> (nonemptystack?)]
26  pop: [(nonemptystack?) -> stack]
27  top: [(nonemptystack?) -> t]

28

29  x,y: VAR t

30

31  push_top_pop: AXIOM
32  nonemptystack?(s) IMPLIES push(top(s), pop(s)) = s

33

34  pop_push: AXIOM pop(push(x, s)) = s

35

36  top_push: AXIOM top(push(x, s)) = x

37

38  pop2push2: THEOREM pop(pop(push(x, push(y, s)))) = push(y,s)

39

40 END stacks