Download stanford pascal verifier user manual

March 1979
Edition 1
Stanford Verification Group
Report No. 11
Computer Science Department
Report No. STAN-CS-79-73 1
STANFORD PASCAL VERIFIER
USER MANUAL
bY
STANFORD VERIFICATION CROUP
Research sponsored by
Advanced Research Projects Agency
COMPUTER SCIENCE DEPARTMENT
Stanford University
Stanford Verification Group
Report No. 11
March 1979
Edition 1
Computer Science Department
Report No. STAN-(X-79-73 1
STANFORD PASCAL VERIFIER
USER MANUAL
bY
STANFORD VERIFICATION GROUP
DE. LUCKHAM, S.M.
G E R M A N , F.W. v.HENKE, R.A. KARP,
P.W. MILNE, DC O P P E N , W . P O L A K , W.L. S C H E R L I S
This research was supported by the Advanced Research Projects Agency of the Department of
Defense under ARPA Order No. 2494, Contract MDA903-76-C-0206. The views and conclusions
‘contatned tn t&s document are those of the authors and should not be interpreted as necessarily
representing the oficial policies, either expressed or implied, of Stanford University, or any agency
of the U. S. Government.
P.W. Milne is employed by CSIRO Division of Computing Research, P.O. Box 1800, Canberra City
ACT 2601, Australia
3
CONTENTS
PARTI
Foreword
I. O v e r v i e w
2. The Verifier
2.1 VCG
2.2 The theorem prover
3. The Assertion Language
3. I Kinds of assertion statements
3.2 Data structure terms
4. The Rule Language
4.1
4.2
4.3
4.4
4.5
Backward rules
Replacement rules
Forward rules
Differences between rules
Rules for data structure terms
5. Verification Examples
5.1
5.2
5.3
5.4
5.5
5.6
5.7
5.8
First example: understanding VCS
Concepts, documentation and verification
A hard invariant
Defining concepts to document a program
Specifications for sorting
A pointer example
Verification of Pascal list structure operations
A larger example
1
3
3
4
5
6
6
7
10
IO
10
10
II
II
12
13
16
17
21
23
24
25
27
P A R T II
Chapter I
Differences from Standard Pascal
1.1 C o m m e n t s
1.2 Program files
1.3 Procedure definitions
I .4 Assertions
35
35
35
35
36
Colitelits
1.5 Blocks
1.6 Types
I.7 F u n c t i o n s
1.8 I n p u t / O u t p u t
1.9 Global variables
I. 10 Virtual variables and Passive statements
I. I 1 Operator precedence
1.12 Union types
User Commands
Chapter 2
2. I
2.2
2.3
2.4
Imperative commands
Setting system parameters
Query c o m m a n d s
System control
Chapter 3
Description of the Simplifier
3.1 Introduction
3.2 Prover for arithmetic
3.3 Record prover
3.4 A r r a y prover
3.5 List structure prover
3.6 Remarks
Chapter 4
The Rule Language
4.1 Introduction to rules
4.2 Using the rule language
References
-
Appendix A Syntax Charts
Appendix B Parser Error Messages
Appendix C VCG Axiomatic Semantics
36
37
37
37
38
38
38
39
42
42
45
46
46
48
48
48
49
50
5 0
50
51
51
60
75
A-l
B-l
C-i
FOREWORD
The Stanford Pascal verifier is an interactive program verification system. It automates much of
the work necessary to analyze a program for consistency with its documentation, and to give a
rigorous mathematical proof of such consistency or to pin-point areas of inconsistency. It has
been shown to have applications as an aid to programming, and to h a v e potential for
development as a new and useful tool in the production of reliable software.
This verifier is a prototype system. It has inadequacies and shortcomings. It is undergoing
continuous improvement, and is expected to be used eventually in conjunction with other kinds of
program analyzers. The purpose of this manual is to introduce the verifier to a wider group of
users for experimentation. We hope to encourage both feedback to help improve this system, and
the development of other program analyzers.
The verifier is coded in Maclisp, a version of Lisp developed at M.I.T, for PDP- 10 computers.
Versions of the verifier run under the TOPS-20 operating system and the Stanford WAITS
operating system!.
How to read this nrallual
T h e m a n u a l i s d i v i d e d i n t o t w o p a r t s . Notation based on the SAIL character set is used
throughout because it is closer to mathematical usage. The alternate notation based on ASCII is
sometimes indicated; the reader can always find the corresponding ASCII notation by refering to
A ppendix A .
Part I is an introduction to the verifier, It contains a short survey of its features and components,
and examples of its use. The reader who has completed Part I should be able to construct simple
examples and run them. He should also have gained some idea of what the verifier can do and
what inadequacies to expect.
Part IT is a manual for those users who embark upon serious experiments with the verifier.
Chapter 1 lists the differences between standard Pascal and the documented Pascal that the
verifier requires as input. The major differences are the required documentation. There are also
some minor differences in code. This is because it is planned that the verifier will accept a more
general programming language, Pascal Plus, including Modules and constructs for concurrent
processing. There is no discussion of the extended language in this manual.
Chapter 2 describes the toplevel user commands.
Chapter 3 is a short description of the special purpose theorem provers. This tells the user what
kinds of knowledge are “built in” and what he must describe to the verifier by means of rules.
Chapter 4 is about the Rule Language. This chapter is in two
rule language and how to express mathematical facts as rules;
intricacies of writing rules and why rules written one way may
efficient proof searches than if they are written another way.
ma.ny simple examples.
sections. The first describes the
the second section gets into the
lead the verifier into much more
Section I should be enough for
Appendix A contains syntax charts similar to the charts given in the Pascal User Manual. Here
one will find the syntax of user commands for running the verifier and the syntax of input to the
verifier, i.e., programs, assertions, and rules. Also, at the beginning of Appendix A, the alternate
ASCII notation for mathematical symbols is given. Appendix B is a list of parser error messages
with a more detailed description of their meaning than is provided by the comments from the
system. Appendix C presents the axiomatic semantics used by the verification condition
generator.
Acknowledgements
We would like to acknowledge the contributions made to the development of the verifier by our
colleagues Shigeru Igarashi, Ralph London, Nori Suzuki, Scot Drysdale and Greg Nelson.
PART I
INTRODWX’lON TO THE STANFORD PASCAL VERIFIER
i. Overview
Section 2 gives a toplevel overview of the verifier and how it is used. Section 3 describes the
assertion language, the language in which the specifications of a program and the accompanying
internal inductive assertions must be written. There are some brief remarks about what kinds of
internal inductive assertions are required. A full description of compulsory assertions is given in
Part II, Chapter I, and this informa.tion is also contained in the syntax charts. Section 4 outlines
some of the basic constructs of the rule language. Rules defining concepts used in assertions ,must
be written in the rule language. Part II, Chapter 4 gives more details about rules and how the
theorem prover uses them. Section 5 gives a number of examples illustrating the use of the
verifier. The first few are quite simple and should be sufficient to enable the reader to run some
simple examples of his own, The final example, on verifying a parser, illustrates formulation of
rules from mathematical theories and the use of the verifier in debugging and improving
specifications. At this point the reader is in a position to begin finding his own ways to use the
verifier. The methodology of using verification systems is by no means fully explored. Further
exampies of verification experiments are given in the references at the end of Part II.
2. The Verifier
T h e v e r i f i e r e m p l o y s t h e i n d u c t i v e a s s e r t i o n m e t h o d d u e t o F l o y d (71 f o r r e a s o n i n g a b o u t
prOgrams. Floyd’s method was developed into a logic of programs by Hoare E 113 and others 13,
141. The verifier constructs its proofs within this logic of programs. It requires as input a Pascal
program together with documentation in the form of inductive assertions at crucial points in the
program and ENTRY/EXiT assertions attached to each procedure.
Fig. I shows what happens when the programmer gives this input to the verifier. The input goes
first to a verification condition generator which gives as output a set of purely logical conditions
called Verification Conditions (VCs). There is a VC for each path in the program. If all of the
VCs can be proved, the program satisfies its specification. The next step is to try to prove the
VCs using various algebraic simplification and proof methods. Those VCs that are not proved
are displayed for analysis by the programmer. If a VC is incorrect, this may reveal a bug in the
program or insufficient documentation at some point. A modification is made to the input and
the problem is rerun. If the unproven VCs are all correct this merely indicates that the proof
procedures need more mathematical facts about the problem. The programmer then specifies
appropriate lemmas as as rules using the Rule Language. These rules are input to the verifier
and the proof is attempted again. Ideally, the time for a complete cycle (Fig. 1) in a m o d e r n
interactive computing environment should be on the order of a minute for a one page program.
Part I: Introduction to the Stanford Pascal Verifier
Lemmas
(rules)
Ver i f’icat ion
Input
Program and
Documentation
I
Conditions
A
Simplified
vcs
J
flodif ied
ANALYSIS OF
OUTPUT
Problem
2.1 vcc
VCG contains a parser and a Verification Condition Generator (VCGEN). VCGEN uses
axiomatic semantics of the programming language to generate VCs. We chose Pascal because at
the time this project began it was the only language for which such an axiomatic semantics within
Hoare’s l o g i c o f p r o g r a m s h a d b e e n g i v e n [13J. VCGEN simply takes the place of the code
generator in a compiler. The program together with inductive assertions is parsed for syntax and
type compatibility (see Part Ii, Chapter I for details). The result is an internal tree representation
from which the VCs are constructed by transforming the inductive assertions as a function of the
code. The transformations correspond to axiomatic proof rules defining the meaning of the
programming language constructs. The theory of VCGEN is presented in 1141.
-The important point is that if all of the VCs can be proved then there is a proof within the weak
logic of programs that the given program satisfies its ENTRY/EXIT assertions and also that each
subsection of the program satisfies its surrounding inductive assertions. Such a proof can be
constructed by reversing the transformations that were applied by VCGEN. So, the VCs are
sufficient conditions for correctness, but not always necessary ones.
The -truth of the VCs often depends on how completely the inductive assertions describe sections
of the code. As a matter of practical convenience, the programmer should not be forced to supply
documentation beyond what is necessary to understand the program. The transformations
currently used by VCG are combinations of the axiomatic semantic rules of Pascal. The objective
of such combinations is to reduce the number of situations in which the user has to repeat his
assertions in trivial and tedious ways (this was a problem with earlier verifiers). The basic
4
Part I: Ilrtroductiorl to the StaIrford Pascal Verifier
assertion requirements are that procedure and function declarations must have ENTRY/EXIT
specifications, and loops within the body of the program must have invariant assertions. It is not
necessary to place assertions at all GOT0 labels. There are other required assertions (e.g., for
global variables) and the details of these are in Part II, Chapter 1.
It is easy to modify VCG for other languages that have axiomatic semantics formalizable within
the logic of programs. No other component of the verifier depends on the input programming
language.
2,2 The theorem prover
The prover takes a verification condition and attempts to prove it correct. If it succeeds, it
returns TRUE; if it proves that the verification condition is inconsistent, it returns FALSE; if
neither, it returns a simplified version of the verification condition.
The prover is the most complex component of the verifier. The major issue In its design is the
trade-off between generality (i.e., logical completeness) and its average response time to given
problems. If the theorem prover is very general, it takes too long to prove VCs and the user gives
up waiting. If it is too restricted in its logical power and requires to be told too many trivial facts
(e.g., x + I 5 y -+ x < y) the user will quickly become frustrated.
We have tried to solve this problem by separating the prover into two parts. The first part,
called the “simplifier”, contains built-in knowledge about the most common data structures of
programming . languages -- numbers, arrays, records, list structure, and simplifies very quickly
expressions involving these data structures. The second part of the prover is the “rulehandrer”,
which uses user-supplied axioms to reason about data structures not handled by the simplifier.
The simplifier is thus a very efficient but very specialized prover while the rulehandler is very
general and not necessarily very efficient. How the two components coexist is a mystery to the
authors of this manual.
As we shall see in Part II, Chapter 3, the simplifier includes a decision procedure for the
quantifier-free theory of rationals, arrays, records, list structure and uninterpreted function and
predicate symbols under +, <, store and select, cons, car and cdr. The main pitfall with a built-in
simplifier such as this is that it is in fact “built in” -- its workings are hidden from the user.
The rulehandler accepts rules supplied by the user to define the concepts used in documenting his
program. These rules are treated as defining axioms for these concepts and are automatically
: used by the prover in searching for a proof. The language for stating rules allows the user to
supply hints on how the rule is to be used. This is one method of making the search for a proof
more efficient (see Bledsoe (21) It is possible to write a set of mathematical facts as a set of rules
in different ways, some resulting in much more efficient behavior from the rulehandler than
others. Also, sufficient mathematical facts for a proof may be supplied, but, depending on h o w
they are expressed as rules, the rulehandler may or may not succeed In finding a proof. In
Section 4 we briefly summarize the kinds of rules and their use. A detailed treatment of the rule
language and how to write rtiles is in Part II, Chapter 4.
5
Part I: htroductiou to the Stauford Pascal Verifier
3. The Assertiorl Lauguage
The assertion language is the language the programmer uses to document his programs. A
documented program is a Pascal program containing assertions; assertions are required at certain
points in programs, and are optional at other places. An assertion is a statement of relationships
between program variables. It defines properties of computation states that must be true every
time the position of the assertion is reached during a computation. For a theoretical discussion of
assertions and the logic of Floyd-Hoare proofs, refer to E I I, 12, i 41.
The assertion language of the Stanford verifier permits logical statements within the quantifierfree first-order theories of arithmetic, Arrays, Records, and Pointers (i.e., the standard Pascal data
types). Essentially this is the language of Pascal Boolean expressions extended in the following
way:
’
- auxiliary user-defined predicate and function symbols are allowed
- priorities of the standard Pascal operators conform to mathematical
conventions rather than Pascal
- special data structure terms have been introduced (see below).
There is not much of a theory of designing assertion languages at present. Assertion languages
.may well become program specification languages later on. We have tried to keep ours simple,
adding new features only when the need for them is clear.
3.1 Kinds of assertion statements
Different kinds of assertions are allowed by the assertion language. We have introduced eight
kinds of assertions to aid stating specifications. Four of these apply to the specification of
procedures. In addition to ENTRY and EXIT assertions there are two others:
,?‘he JNITJAL declaration is used to describe the values of a parameter before and after a
procedure call. I f p r o c e d u r e p(x) a d d s 1 to x w e c a n n o t s i m p l y s a y x>O (p(x)) x=:x+1. A
con vtn tion denoting tense is needed. An INITIAL statement allows naming entry values, e.g.,
J N J T I A L X=XO A x>O (p(x)) X=X0+ i.
The -GLOBAL declaration permits the user to declare global variables of a procedure as f o r m a l
parameters. O n e i m p o r t a n t a p p l i c a t i o n o f t h i s i s i n d e a l i n g w i t h p o i n t e r p a r a m e t e r s . I f a
procedure has a parameter of type tT, it is often necessary to declare the reference class (beiow),of
ail objects of type T as a global variable. This permits the verifier to keep track of a n y sideeffects.
Other kinds of assertion statements are intended for use to avoid having to repeat inductive
Part I: lrrtroductiotl to the Statrford Pascal Verifier
assertions unnecessarily. The examples in Section 5 show the use of some kinds of assertions; a
complete list of kinds of assertions and compulsory assertions is given in Part 11, Chapter 1.
3.2 Data structure terms
The axiomatic theory of data structure terms has been introduced into the assertion language to
define the semantics of assignment and selection operations on the Pascal structured types
A RRAY, RECORD, and POINTER. For example, a data structure term of the form <A ,[Il,E>
denotes the array obtained from A by placing E in the ith. position; <A,[Il,E>[Jl denotes the jth.
element of CA ,[I],E>.
W e have similar terms denoting assignments to dereferenced pointers. For each pointer type
declaration, TYPE T=tTO, the verifier introduces a reference class, called *TO, of all elements of
t y p e T O . P o i n t e r s o f t y p e T are related to crT0 j u s t a s a r r a y i n d i c e s a r e r e l a t e d t o a r r a y s .
Example: The reference class resulting from Xt:=E is denoted by the term, <+TO,cX3,E>.
The ordinary first-order assertion language is extended to express the effects of data structure
operations. The newly introduced functions are defined axiomatically.
3.2.1 Referewe class identifiers
W e introduce new individual variables called reference class identifiers into the assertion
language. They have the fo,rm,
#<identifier>
where <identifier> is any legal Pascal type identifier.
Reference classes are not types in Pascal (although the syntax for bounded reference classes
appears in the early version of the Pascal specification). They are assertion language primitives
and behave very much like unbounded arrays. We will define the type of *T to be reference class
of T.
3,2.2 Fwwtiorrs aud predicates
011
data structures
. New function symbols corresponding to the Pascal selection, assignment, and new operations
complex data type variables are introduced:
Select ion:
Assignmel~t:
Extension:
x[y] (array selection), r.f (record selection), Dcq> (pointer selection)
<x, [y], II> (array assignment), <r, .f, z> (record assignment),
CD, cq>, t> (pointer assignment)
D”q
on
Part I: Iutroductiorl to t h e Stanford Pascai Verifier
The new terms formed by composition of these new functions must obey the Pascal type
compatibility requirements. T h u s x[y) is legal only if x is of array type and y is of the correct
index type. S i m i l a r l y <x,cy~>,z> is legal only if x is of type reference class and x,y,z h a v e
compatible types. To do this, the new functions have types. The type of x[yl is the type of
elements of the array term x. The type of <x,[y],z> is the same a s that of x. If the type of x is
r e f e r e n c e class of T, the type of xcy~ is T. The type of <x,cy>,z> is the same as that of x. The
type of Dux is the same (reference class) type as D . The types for record terms are defined
analogously.
The definition of terms in the assertion language is extended to accomodate new terms created by
the combination of reference class identifiers and the special functions. Assertion language terms
are:
I. ail Pascal variables
2. ail terms obtained from 1. and the new functions by function
composition restricted to compatible types.
The new terms are called data structure terms.
Reference predicate: Pointer.
To(X,D) means X is a pointer to a member of the reference class D.
-_
3.2.3 Axioms for data structure term
* The selection and assignment functions satisfy the following axioms (all the free variables are
universally quantified):
A
A
A
A
A
A
x
x
x
x
x
x
I. Y = U -) <X, [YJ, Z>[U]=Z
2 . Y#U -) <X, EY], Z>[uJ=XEuJ
3 . <X, ,Y, Z>.Y = Z
4 . <X, .Y, Z>.U = XU where Y and U are distinct identifiers
5 . Y=U -+ <X, cY>, Z>CUD=Z
6 . Y&l -B <X, cY>, Z>cU>=XcU>
The extension function obeys three axioms:
A x 1. DuXuY = DuYuX
A x 8 . X+Y + (DuX)cY>=DcY3
A x 9 . X#Y -) <D, cY>, Z>uX=<DuX, cY>, Z>
Similarly, the predicate PointerTo(X, D) obeys the following axioms:
A x I O . Pointer-.To(NlL, D )
A x I l . P o i n t e r - T o ( X , DuX)
A x 12. Pointer-To(X, CD, cY>, E>) s Pointer-To(X, D )
A x i 3 . X#Y -) (Pointer-.To(X, DuY) s Potnter-To(X, D))
Part I: Introductiou to the Stanford Pascal Verifier
A formulation of most of these axioms as verifier rules is given in 4.5.
Other standard lemmas may be derived from these axioms. For example, <A, [I], A[I]> E A can
be obtained as follows:
4 EJI, AI11 >
- A i f and o n l y i f (Vj) <A, [I], A[I]>[j] - A [ ] ]
We prove by cases.
S u p p o s e j+l, T h e n , <A, III, A[Il>[jl - A[jJ from Ax 2.
Suppose J-1. Then, <A, [I], AEiJ>[j] - AIIl=A[jl f r o m A x 1 .
i n b o t h c a s e s <A, (II, A[Il>ljl - AEj1. T h e r e f o r e , (Vj) <A, [II, A[Il>[jJ -
ACJJ.
These axioms form a first-order theory of data structures. The terms of this theory represent
finite sequences of operations on data structures. The theorems are logical formulas containing
equalities and inequalities between data structure terms.
For example, we can show that the formula
KZI
A
L=J -) <<A, [II, <AD], EJa 2-e
Ml, BAIlELI - 2
is a theorem of this theory. By axiom 2,
K+I + <<A, 113, cAbI, EJI, 2~ EKI, BdIIELI - <A, [II, <A[Il, [Jl, 2>413ELl.
A x i o m I i m p l i e s <A, Ill, <ALlI, EJI, 2>AIIELJ - <ADI, LJI, 2>1L1,
and finally L=J + <AIll, EJI, 2dL1 = 2.
In order to express many complicated properties of data structures we need to introduce auxiliary
predicates, For example, if we have Pascal type definitions,
VPe
T O = tT;
T = record . . . . Next: TO; . . .
it may be necessary to make assertions about “reachability” between pointers, i.e., from pointer x
one can reach pointer y by performing the Next operation finitely many times. We introduce
auxiliary predicates and add the axioms (D ranges over terms of type reference class of T):
Reach(D, x, y) “df (3j) Reachstep(D, x, y, J)
Reachstep(D, x, y, 0) “df (x=y)
Reachstep(D, x, y, j+ I) “df (3~) Reachstep(D, x, z, j)
A
Dcz>.Next=y
Axiomatizations of auxiliary concepts must be supplied by the programmer as rules (see Section 4
and examples, especially 5.7).
The semantics of Pascal array, record, and pointer operations can be defined by Floyd-Hoare style
axioms in terms of the theory of data structures. The actual semantics used in the verifier is
given in Appendix C.
Part I: Introduction to the Starrford Pascal Verifier
4. The Rule Language
4.1 Backward rules
B a c k w a r d r u l e s e x p r e s s l o g i c a l i m p l i c a t i o n s , G+F, and are stated, INFER F FROM C. T h e
rulehandler component applies these ruies in a depth first backwards chaining search for proofs.
A rule will apply to a problem, A-+B, if B is a n instance of F. INFER will then try to prove
A-+G’ where G’ is the corresponding instance of G. The rulehandier does not attempt to deduce
new rules from the given set.
Examule: In 5.2 we formulate a property of the gcd function:
GCD4: INFER GCO(X, Yl =GCO VlOO(X, VI ,Y) FROM Y>0:
A g a i n , n o t e t h a t t h i s r u l e w i l l o n l y b e a p p l i e d b y t h e s y s t e m i f a n i n s t a n c e o f gcd(x,r) gc&o&, r), u) occurs as a result to be proven during the proof.
--
4.2 Replacement rules
‘These express logical equivalences between atomic formulas, FwG, and equalities between terms,
F=G, and are stated in the form: REPLACE F BY G. Whenever an instance of F o c c u r s in a
VC the equality F=G Is asserted. (Note that F is not replaced by G, rather the notation “replace”
has historic reasons.)
Example: The following is used in 5.8.5:
CONSTANT NULL-SEQUENCE:
CON4: REPLACE CONCAT (X, NULL-SEQUENCE) BY X;
This rule asserts that concat(x, null-sequence) = x. Note, however, that this equality only becomes
known to the prover if an instance of concaf(x, null-sequence) occurs during the proof.
4.3 Forward rules
Forward rules also express an implication t&F, but they differ from backward rules in the w a y
they are used in proof searches. These rules are written: F R O M G INFER F. Forward rules can
be used to derive consequences from a set of known facts.
ExamrIle: The inference rule given in 4.1 can be rewritten as:
GCO4F: FROM Y>0 JNFER GCO(X,Y)=GCOVlOO(X,Y),V)r
IO
Part I: Introduction to the Stanford Pascal Verifier
In this case the fact expressed by the rule would be known to the system as soon as a term y>O
becomes true during a proof.
4.4 Differences betweeu rules
Different rules may express the same logical statement. For instance the equivalence of two
formulas A and B can be stated in at least the following three ways:
REPLACE A BY B;
INFER A FROM B; INFER B FROM A;
FROM A INFER B; FROM B INFER A;
The reason for this is that rules not only express logical facts; they also contain information for
the prover on how and when to use those facts. Part II, Chapter 4 explains how the different
kinds of rules are used.
The application-of a rule can be limited by the use of restricting expressions. Suppose we want to,
express the fact that xuy>O if x>O and y>O. We could write:
F R O M X>O
A
Y>O J N F E R X*Y>O;
This rule might, however, lead to very inefficient proofs. For each pair of terms known to be
positive, the fact that their product is positive will b e asserted. From x>O A y>O we derive not
o n l y x*y>O b u t a l s o x*z+y>O, x*JN~>O, and so on. We can avoid this by adding a whenever
expression to the rule:
W H E N E V E R X*Y F R O M X>O
A
Y>O I N F E R X*Y>O;
The restriction X*Y limits the application of this rule to those x and 7 whose product appears in
the formula to be proved. Again, note that the use of restrictions is explained in Part II, Chapter
4.
4.5 Rules for data structure terms
The axioms of the theory of data structures were given in 32.3. Below we give a set of rules
. expressing most of these axioms. The axioms omit the inequalities between all pairs of distinct
record field identifiers. At the moment, only some of the theory is implemented by the simplifier
and it is up to the user to include, in his rulefile, rules such as these to express any required data
structure axioms:
A R R O : R E P L A C E < A , CJJ, E>[J] B Y CASES I=J + E; IICJ -) A[Jl E N D ;
R E C O : R E P L A C E < A , .II, E>.JJ B Y C A S E S IJ=JJ + E; IbJJ + A.JJ E N D ;
P N T O : R E P L A C E < A , ~13, E>c3> B Y C A S E S I=J -) E; I+J + AcJ3 E N D ;
Part i: htroductiotr to the Starrford Pascal Verifier
PNTI: R E P L A C E AuJcJ> W H E R E IrJ B Y AcJq
P N T 2 : R E P L A C E < A , ~12, E>uJ W H E R E JzJ B Y <Auj, ~12, E>;
PNTS: W H E N E V E R AuX I N F E R POINTER-TO(X, AuX);
P N T 4 : F R O M POJNTER-TO(X, A ) I N F E R P O I N T E R - T O ( X , < A , cY2, E>);
P N T 5 : F R O M POINTER-.TO(X, A ) I N F E R P O I N T E R - T O ( X , AuY);
PNTG: F R O M -POINTER-TO(X, AuY) I N F E R - P O I N T E R - T O ( X , A ) ;
PNT7: F R O M T R U E I N F E R POINTER-TO(NIL, A ) ;
P N T 8 : F R O M P O I N T E R - . T O ( X , A ) A - P O I N T E R - T O ( Y , A ) I N F E R X#Y;
5. Verificatiorl Examples
The paradigm employed in ordinary programming can roughly be described as follows: One starts
out with some concepts that describe what the program is supposed to do and how it will do it.
Such concepts may infiude arithmetical facts, properties of data structures, e.g., “array A is sorted”,
and procedures, e.g., “exchange the ith. and jth. elements of array A”. These concepts are well
enough understood that they are used to guide the human problem-solving activity that finally
results in a program. M-any attempts have been made to formalize this activity as an ordered
sequence of steps, e.g., “ r e q u i r e m e n t s + code + documentation + testing”, or by a “topdown”
method. Despite these attempts, normal programming activity seems well described by the
diagram,
CONCEPTS
1
1
COMPILED
PROGRAM
CODE
TESTING
In designing verifiable programs we advocate a completely different process. Again we start out
wltii concepts. But before writing any code we develop a formal theory of the concepts involved.
C)ften the concepts are already axiomatized (e.g., arithmetic) and one can use well known formal
theories. II-I other cases (e.g., business applications) the necessary formalisms have to be developed
from scratch. Hopefully this will change as more and more programs are verified and more
theories for important programming concepts become available.
Using our formal theory of the initial concepts we can rephrase the original problem by precisely
stating what the program is supposed to do within the formal theory. Now we are ready to
embark on writing a program. This will be done with the theory in mind, and at any stage we
may use documentation by inductive assertions (the assertions being formulas of the formal
t h e o r y ) t o j u s t i f y a p a r t i c u l a r p i e c e o f c o d e . Additionally, some program statements, e.g.,
procedures and loops, must have formal inductive assertions stating their behavior - i.e., certain
statements have a required documentation. This means in particular that each loop has an
12
Part 1: Mroductiou to the Stanford Pascal Verifier
associated invariant.
statements.
The final product will be a program documented by precise formal
In parallel with writing the program, the axiomatic theory defining the programming concepts
must be expressed in a form accepted by the verifier, i.e., as “rules”.
Finally, the program and the rules are submitted to the verifier. The result may or may not be a
proof of the correctness of the program. If not, we have either written a w r o n g p r o g r a m o r
inadequate assertions, or the rules expressing the theory are insufficient for the system to find a
proof. In each case we have to improve one of the above steps (specification, coding, rules) until a
proof is established.
Graphically the verification paradigm for program development can be represented as follows:
CONCEPTS
r
1
FORMAL THEORY
1
SPECIFICATIONS
RULES
IT
VERIFICATION4
0OCUtiEr;JTEO
PROGRAM
4
COMPILED CODE
5.1 First example: understanding VCs
This is a simple example in constructing documented programs and reading very simple VCs.
We hope eventually to automate aids for analyzing VCs.
W e begin by constructing a procedure that multiplies a given value parameter, Y , b y a g l o b a l
valu e, N, and stores the result in X; its specifications are:
P R O C E D U R E CONSTMULTtVAR X:INTEGER: Y:INTEGER)t
GLOBAL (N);
EXIT X=Y*N;
We could implement this by repeatedly adding Y to X in a loop; if we use Z to count the number
of times the addition has been performed, we will expect X=Y*Z to be an invariant of the loop.
This
should b e s u f f i c i e n t internal documentation.
Finally,
we
will
try
calling
CONSTMULT(X,N) to compute the square of N.
13
Part I: Introduction to the Stanford Pascal Verifier
PASCAL
VAR N, 2: INTEGER;
PROCEDURE CONSTMULT ‘VAR XiINTEGER; Y:INTEGER);
GLOBAL (N) :
E X I T X=Y*N;
VAR Z: INTEGER;
BEGIN
X+0: Ze0;
INVARIANT X=Y*Z
W H I L E ZzN DO BEG1 N XcX+Y;
z+zt1
END
END;
EXI T Z=N*N:
BEGIN
CONSTMULT (Z,N) ;
END,
F o r C O N S T M U L T to--be consistent with its documentation, there are two VCs that must be
proved. KS tell us what theorems are needed to prove the correctness of paths in the program.
The expressions in a VC are substitution instances of assertions and boolean tests in the program.
W e can recognize which paths are in the V C by the values of loop and conditional tests, and
assertions appearing in the V C .
Unsimplified Verification Condition: CONSTMULT 1
0=Y*0 A
(X-0=Y*Z-0 A
- (Z-0zN)
-3
X-B=Y*N)
T h i s VC is of the form:
INVARIANT(O,Y,O)
A
(INVARIANT(XO,Y,Z-0)
A
-LOOPTEST(Z-0,N) -) EXIT(X-O,Y,N)
‘It implies the consistency of two paths:
(i) The path from the entry to the loop before it is executed: the initial values of X, Y, and Z
must satisfy the invariant, and since these values are, X=Z=O, this requires O=YnO.
(ii) The path from the loop to the exit: Since X and Z are variables of the loop, their final values
may differ from their initial values, so V C G E N has given these final values the new names X-0
a n d Z.-O.
14
Part 1: Introduction to the Stallford Pascal Verifier
Unsimplified Verification Condition: CONSTMULT 2
(X=Y*Z A
Z#N
-b
X+Y=Y*(Z+lII
This VC is of the form,
INVARIANT(X,Y,Z)
A
L O O P T E S T ( Z , N ) -) iNVARIANT(XtY,Y,Zt I).
It corresponds to the path around the loop, and implies that X*Y-Z is an invariant. To prove it,
the prover will need the distributive law of arithmetic, which m a y b e e x p r e s s e d by a rule as
follows:
RULEFILE(DISTRIBUTIVITY~
01 ST! R E P L A C E A* (B+C) BY A*B+A*C;
It should be emphasized that such arithmetical rules can sometimes lead the prover into deducing
m a n y i r r e l e v a n t -facts; f o r t h i s r u l e t o h a v e t h e d e s i r e d e f f e c t , t h e v e r i f i e r p a r a m e t e r
SUMMATCH must be turned on (see Part II, Section 4,2,13),
Finally, proof of the procedure call depends on the VC,
Unsimplified Verification Condition: MAIN 1
(Z-B=CONSTMULT-X(Z,N,N)
Z-0=N*N
+
Z-B=N*N)
A
.
This is trivially true, but it is instructive to note what VCGEN is doing in constructing the VC.
it is of the form,
Z,O=FUNCTiON(<initial values of all parameters>)
CONSTMULTEXIT(Z-0,N)
-9
EX IT(Z,O,N).
A
Z. 0 is the final value of the actual VAR parameter Z (note this is the outer Z). This VC states
-that the result of the procedure call (i.e., the EXIT assertion of CONSTMULT instantiated to the
-finat values of its actual parameters) may be assumed in proving the EXIT to the main program.
Also, a function is constructed for each VAR parameter that maps the initial values of all
parameters (including the globals) into the final value of that VAR parameter; VCGEN appends
the formal parameter to the procedure name to make a unique function name (in this example,
CONSTMULT-X). This reflects the semantics of procedure call in 1131.
I5
Part I: Iutroductiort to the Stauford Pascal Verifier
5,2 Concepts, documentation and verificatiou
As a next example we will verify a simple greatest common divisor (gcd) program. The concept
of the gcd i s o f c o u r s e w e l l k n o w n a n d w e c a n b a s e o u r d o c u m e n t a t i o n o n t h e s t a n d a r d
mathematical properties by using the following lemmas for non-negative x and y:
g&(x, 0) = x
gcd(x ( x) = x
gee * y) = gc4y 94
gdm& 8 y) 9 y) = gc4% y) if po
msd(x, y) < x
The program uses these properties by repeatedly replacing one of the values x or 1 by V&(X, r).
PASCAL
FUNCTION MOO(l,J:INTEGER):iNTEGER;
E N T R Y 120 A J>0;
EXI T MODr0:
EXTERNAL;
FUNCTION G(X0,Y0: INTEGER): INTEGER:
E N T R Y X0>0 A Y0>0;
EXI T G=GCO (X0, Y0) ;
VAR X,Y,R: INTEGER:
BEGIN
X+-X0; Y+-Y0;
REPEAT R+-MOO(X,Y);
X+Y;
Y+R
U N T I L Y=0
I N V A R I A N T GCO(XB,YB)=GCO(X,Y) A X>0
G&X
END:.
A
Yr0;
The invariant for the REPEAT-loop follows immediately from our basic idea of replacing one
argument of g&(x, y) by V&(X, J) and thereby not changing the value of gtd.
The next step towards a verification is to express the facts about gcn mentioned above in a form
acceptable to the verifier. In the rule language these facts can be expressed in various ways: one
can use forward or backward rules or any combination thereof. In the first case the prover would
deduce all terms equal to a term x as soon as it sees x. Going backwards the prover would try to
prove an equality only if it is needed. There is no generai rule telling us which is better, each
method has its own advantages and disadvantages. Let us specify the properties of gccI with
forward rules.
16
i
Part 1: Introduction to the Starlford Pascal Verifier
RULEFILE (GCO)
GCUl: R E P L A C E
GCCQ: REPLACE
GCD3: REPLACE
GCD4: REPLACE
GCD(X, 01
GCO(X,X)
GCD(X, Y)
GCD(X,Y)
B Y X:
B Y X-t
BY GCDIY,X):
WHERE Y>0 BY GCO(MOD(X,Y),Y);
Rewriting these rules as backward rules leads to the following rulefile, which is not sufficient for
the proof of all the verification conditions:
RULEFICE (GCD)
GCDl: I N F E R GCD(X,B)=X;
GCDZ: INFER GCD IX, X) =X:
GCD3: INFER GCD(X,Y)=GCD(Y,X);
GC04t I N F E R GCO(X,Y)-GCD(MOD(X,Y),Y) F R O M Y>0:
Two verification conditions require commutativity (rule GCD3); these two formulas cannot be
proved with this set of rules. The reason is that the backward rule GCD3 is only applied if the
system tries to pave a formula that matches the pattern of the INFER clause. If we change the
rule GCD3 into
GCD3: INFER GCCI(X,Y)=Z FROM GCD(Y,X)-Z;
we greatly increase the number of possible matches; in fact, using this modified rule, one can
verify the gcd program.
5,3 A h a r d i n v a r i a n t
The following example demonstrates that finding a suitable invariant is not always a simple task.
We want to emphasize, however, that this example is not typical of problems arising in practice.
In general we have some intuitive idea of what a loop is supposed to do and this will lead us to
finding the right invariant (in fact we ought to be able to write the invariant before we write the
code for the loop). ln this example we find ourselves in the position of verifying a rather tricky
program and finding its loop invariant requires understanding the trick. The program is an
iterative version of McCarthy’s Si-function [:!I]. This function is recursively defined as
f(x) = lfx>lOO fhen x-10 ehJVTx+lI))
lt can be shown that this recursive function computes
f(x) = if x> 100 then x- i 0 eke 9 1
Now we want to show that the following program computes the same function:
17
Part I: Introduction to the Stanford Pascal Verifier
PASCAL
LABEL 1:
VAR X,Yl,YZ,Z:INTEGER:
ENTRY TRUE :
EXIT (X>l00
A
Z=X-10) v (Xc101
A
BEGIN
YltX; Y2t1;
1:
Z.di):
ASSERT ????;
IF Yl>l00 T H E N
IF NOT(YZ=l) THEN BEGIN
Yl+Yl-10;
YZCYZ-1;
END
ELSE BEGIN
END.
._
END
GOT0 1
ELSE ZtYl-10
Yl+Yl+ll;
YZtYZ+l :
GOT0 1
The entry and exit assertions simply state that the program computes the same function as the
recursive 9 I-function. The difficult part is to find a suitable invariant at ????. T h e k e y , o f
course, is to first understand the operation of the program.
Each time label i is reached the program starts computing f. There are two possible cases
depending on Y 1. If the initial value of Y WOO, the program terminates immediately. In the
other case function f calls itself recursively, i.e., f(f(Y l+i I)). The program computes the inner call
to f by jumping back to label 1. But in addition, it has to be recorded that upon completion of
this computation, the outer call has to be computed. This is done by incrementing the variable
Y2; thus Y2 tells us how many outer calls remain to be evaluated whenever we reach label I.
Suppose at a given point in time all remaining outer calls will take the Y I> 100 branch. Then
each time Y I will be decreased by 10 and 2 will become Y I-10mY2. Since in this case 2 has to be
91, we propose the invariant Y I-1O*Y2=91. But this turns out to be too strong. It might be the
case that all but one of the outer calls are evaluated and we arrive at iabel I in a situation where
-Y2= 1 and Y I< 101. In this case the loop will take the Y 15100 branch and new recursive calls
have to be evaluated. Thus the invariant will only be Y 14O*Y2<92. This is still insufficient,
but the remaining details are fairly easy to find. First, we have to take <are of the case where
X> 100, i.e., the program terminates immediately. Second, we will need the fact that throughout
the loop Y2 is positive, so we have to add the conjunct Y2>0. Altogether we get the invariant:
((x>ioo A y&4 A Yi=x) V (xdo1 A yi-10*%?<%)) A y2>0
The following is a terminal session showing the verification of this program. Note that the
prover has to do some non-trivial reasoning to prove MAIN 4. The boldface characters were
typed by the user.
18
Part i: Introduction to the Stanford Pascal Verifier
r verify
H i t h e r e , IJelcome t o t h e P a s c a l V e r i f i e r ,
V e r s i o n (KC 4 , SIMP 24.1 ( O c t o b e r 4 . ..I
Type ‘HELP;’ for help
>read ItfWver;
R e a d i n g f i l e : I TF91. PAS CEX, VERI
SYNTAX SCAN COMPLETE.
PROGRAM PARSED,
CPU SECONDS t 0.383
>priMvc;
>
U n s i m p l i f i e d V e r i f i c a t i o n C o n d i t i o n : MAiN 1
10<y2 A
(100<X A
Y2=1 A
Yl=X v
x<101 A
Yl-10*Y2<92)
l@@dl A
A
-(YZ=l)
4
(18&x A
Y2-14 A
Yl-10=x v
XC181 A
(Yl-10)-10r(Y2-1)<92)
0<Y2-1)
A
U n s i m p l i f i e d V e r i f i c a t i o n C o n d i t i o n ! MAiN 2
(188Cx A
I=:1 A
x=x v
XC181 A
X-18*1<92)
0<1
A
U n s i m p l i f i e d V e r i f i c a t ion Cond i t ion: MAIN 3
(0<Y2
A
(l@@<x A
Y2=1 A
Yl=X v
k181 A
19
Part i: Introduction to the Stanford Pascal Verifier
Yl-10*Y2<92)
188<Yl
A
A
~4Y24)
4
188<x A
Yl-10=X-10 v
xX101
A
Yl-10=91)
Unsimplified Verification Condition: MAIN 4
(0CY2
A
(180<x A
Y2=l A
Yl=X v
XC101
A
Yl-10*!f2<92)
~(100<Yl)
+
(18&x
A
A
A
Y2+1=1
Yltll-x v
XC101
A
(Yltllb10*(Y2+1)<92) A
0<Y2+1)
>sirnyiify:
>
S i m p l i f i e d V e r i f i c a t i o n C o n d i t i o n : MAIN 1
TRUE
S i m p l i f i e d V e r i f i c a t i o n Conditiont M A I N 2
TRUE
S i m p l i f i e d V e r i f i c a t i o n C o n d i t i o n ! MAlN 3
TRUE
Simplified V e r i f i c a t i o n C o n d i t i o n ; MAiN 4
TRUE
20
Part i: htroductiou to the Stanford Pascal Verifier
5.4 Defining concepts to document a program
The next program we will verify returns the maximum value of an array.
To formalize the concept of the maximum of an array we define the predicate n&xc@, a, 1, r) to
be true if x i s t h e m a x i m u m o f t h e a r r a y e l e m e n t s a[il with k&r. W e c a n g i v e a f o r m a l
definition of maxof as:
From this definition the following lemmas are immediate:
mux0f(ar11, u, 1,l)
These lemmas may be written directly as backward rules without any changes of propositional
structure because-they are all simple implications between conjunctions of atomic formulas. The
rules below, however, are weaker than these lemmas. They are sufficient for the verification of
this implementation of max because the array is scanned from I to N.
The full input submitted to the verifier for this problem is given b e l o w . P a s c a l P l u s p e r m i t s
arrays in inner blocks to be dimensioned using VAR variables and this ts the reason for the
enclosing procedure DUMMY. (Note “:=” and “t” are both accepted as notation for assignment.)
RULEFJLEfMAX)
Ml: INFER MAXOF(A[lI,A,l,l1:
F R O M 122
M2: I N F E R MAXOF(X,A,l,J)
M 3 : I N F E R MAXOF(AIJl,A,l,J) F R O M 122
PASCAL
VAR N:JNTEGER:
PROCEDURE DUMMY:
EXJ T TRUE;
TYPE NARRAY=ARRAY El :Nl OF INTEGER;
FUNCTION MAX(A:NARRAYhINTEGER:
GLOBAL (N);
ENTRY N>0;
E X I T MAXOF(MAX,A,l,N);
VAR TEMP,J:JNTEGER;
BEGIN
TEMP:=A [II;
F O R I:=2 to N
INVARIANT MAXOF(TEMP,A,l, I-1)
00
I F(AEIJ>TEMP) T H E N TEMP:mAEIl:
MAX:=TEMP
21
A AUlsX A
A AW>X A
MAXOF(X,A,l,I-1):
MAXOF(X,A,l,I-11;
Part I: Introductiorl to the Stanford Pascal Verifier
END:
BEGIN END;.
It is instructive to look at the unsimplified verification conditions. At this stage the properties of
naxof declared in the rulefiie have not been applied.
Unsimplified Verification Condition: M A X i
tB<N A
21N
+
MAXOF(AIll,A,l,Z-1)
A
(MAXOFtTEMP-B,A,l, (NtlI-1)
-b
MAXOFfTEMP-B,A,l,NH)
Unsimplifiid V e r i f i c a t i o n C o n d i t i o n : M A X 2
t0cN
N<2
+
A
MAXOF(AEll,A,l,N))
Unsimplified Verification Conditionr M A X 3
(IIN
221
A
A
MAXOF(TEMP,A,l,I-1) A
TEMP<AI I1
-b
MAXOF(A[JI,A,i, (JtlI-1))
U n s i m p l i f i e d V e r i f i c a t i o n Conditions M A X 4
(J,<N
2~1
A
A
MAXOF(TEMP,A, 1,141 A
-(TEMP<AEJJ)
-4
MAXOF(TEMP,A,I, (1+1)-l))
The verifier partitions the paths of a program in a particular way and each VC corresponds to
one of these paths. MAX i corresponds to the path ENTRY -) enter FOR-bop A exit F O R - l o o p
22
Part I: Introductiorl to the Starrford Pascat Verifier
+ EXIT; TEMP.-O is the final value of TEMP on leaving the loop. MAX 2 corresponds to the
p a t h E N T R Y + bypass FOR-loop -) EXIT, MAX 3 and M A X 4 correspond to the two different
paths around the loop.
In practice, the initial rulefile i s u s u a l l y i n a d e q u a t e f o r t h e p r o o f o f a l l VCs. In this case
inspection of the unproven (but simplified) VCs will often suggest new rules or modifications.
These are then added to the ruiefile and run in the verifier, This procedure is then repeated
until a.11 KS are proved.
Ii,5 Specifications for sorting
This Bubble sort example is documented by standard sorting concepts. Each concept has a simple
first-order definition (except permutation, see E12, 263). For example,
OR DERED(A, L, R) means array A is ordered in the range IL, RI:
ovder_ed(a I,
Y) =dl
(Vi) (1~1 A kr -) A[IJs;A[I+ II).
PA RTITION(A, L, I, R) means that each element of A in EL, I] is smaller
than each element of A in [It I, R1:
Rules defining sorting concepts, including permutation, are given in E5J. The rules state not only
standard axioms satisfied by the concepts, e.g., transitivity of permutation, but also how the
concepts are related when operations are performed on arrays. Here is an example from El:
ORO6a: INFER OROEREOkA, IPJ ,X>,L,RI FROM OROEREOCA,L,RJ
A XrA (P-13 ;
A
L<P
A
P<R
A
X,<A [P+ll
Rule ORD6a states conditions under which the array obtained from A by placing X in A[PJ is
ordered.
The rules can be shown correct by proving them from the first-order definitions. The sorting
concepts may be used to document many different sorting algorithms, and the same defining set of
rules can be used for verification [5J (rules for the theory of data structures are also needed).
23
Part I: lutroductiou to the StaIrford Pascal Verifier
PASCAL
VAR N: INTEGER:
PROCEDURE DUMMY;
EXIT TRUE;
TYPE NARRAY=ARRAY El I NJ OF INTEGER;
PROCEDURE SORT WAR A: NARRAYl :
GLOBAL (N) ;
IN1 T I A L A=A0;
ENTRY Nzl;
E X I T PERMUTATION(A,ABl n OROERED(A,l,N);
V A R I,J,TEMP:INTEGER;
BEGIN
I:+ J:=l;
FOR I :=l TO N - l
I N V A R I A N T PERMUTATION(A,AB) n DRDERED(A,N-1+2,N) n
PARTITION(A,l,N-I+l,N)
DO
FOR J: =l TO N - I
INVAAIANT PERMUTATION(A,AB) n ORDEREO(A,N-1+2,N) n
ISBIGGER(AEJI,A,l,J-1) n PARTITION(A,l,N-I+l,N)
DO
IF A [Jl>AEJ+ll THEN BEGIN
TEMP: =A [Jl :
A[Jl:=A[J+ll;
END:
END
A [J+ll : =TEMP
BEGIN END;,
5.6 A poitjter example
The procedure below has a side-effect. It changes the contents of the cell referenced by its X
p a r a m e t e r b y m a n i p u l a t i n g Y . The problem is to verify this. The type declaration, P N T R ,
introduces the reference class #CELL of all cells referenced by pointers of type PNTR. *CELL is
‘a variable of the computation of SIDEFFECT although it cannot be mentioned in the code. It
must therefore be declared as a GLOBAL parameter of SIDEFFECT, and indeed as a VARiable
GLOBAL.
24
Part I: Introduction to the Stanford Pascal Verifier
PASCAL
T Y P E P N T R = WELL:
CELL - RECORD CAR:INTEGER END;
P R O C E D U R E SIDEFFECTWAR Y:PNTR; X:PNTR) ;
G L O B A L (VAR #CELL) ;
E N T R Y Xt,CAR = 1:
E X I T Xt.CAR = 2;
BEGIN
Y: =X:
Yt,CARl=2
END:.
The single verification condition for procedure SIDEFFECT is
(#CELLcX>.CAR=l n
POINTER-TO(Y,#CELL) n
POINTER-TO(X,#CELLl n
#CELL-B=<#CELL,
cx>,
<#CELLcX>,.CAR,2>>
-_
3
#CELL-0~x2. CAR=21
The identifier #CELL-O refers to the reference class after the operation Y?.CAR:=2 w h i c h
changes one of the ceils in *CELL (namely the one pointed to by Y). So the relationship between
them is
#CELL,0 o <#CELL, cY>, <tCELLcY>, CAR, 2-n
The assignment of the value of X to Y makes this equivalent to the form that appears in the V C .
The VC is proved using rules for reference classes given in Section 4,5,
5.7 Verificatiorl of Pascal list structure operations
-
List structures are usually implemented in Pascal by means of pointers and records. Verification
of programs that operate on lists requires introducing higher level concepts analogously to the
sorting concepts for sotWig operations on arrays. L i s t o p e r a t i o n s a r e d e f i n e d i n t e r m s o f
operations on reference classes.
-The procedure INSERT in the example below inserts a new word into a loopfrce list. To prove
that INSERT preserves loopfrcentw we use the Reach concept introduced in 3.2.3. The predicate
Reach(D,x,y) is true if by refering to the NEXT field repeatedly, starting at x, one can reach y;
i.e., the sequence, x, Dcx>.Next, DcDcxzNextD.Next, , . . in the reference class D contains the
pointer y. This implies that there are no loops between x and y.
25
Part I: introduction to the Stairford Pascal Verifier
PASCAL
T Y P E R E F = fWORD:
WORD - RECORD COUNT: INTEGER; NEXT:REF END;
PROCEDURE INSERT(ROOT,Y,SENTINEL:REF)r
G L O B A L (VAR #WORD) ;
E N T R Y REACH(#WORD,ROOT,Y) n REACH(#WORD,Y,SENTINEL) /\
YzSENTINEL n YPINIL;
E X I T REACH(#WORO,ROOT,SENTJNEL1;
VAR Z: REF;
BEGIN
NEW(Z);
Zf.NEXT+YkNEXT;
Yt,NEXTtZ
END:.
The entry assertion implies that the list from ROOT to SENTiNEL is loopfree and Y is a p o i n t e r
to a word in the list. The procedure inserts a new member of the list between Y and its successor.
The exit assertion implies that the result is still loopfree. This p r o p e r t y ot INSERT is easily
verified using the rules for data structures and some rules defining Reach.
Here are three examples of rules defining Reach:
Rl: I N F E R REACH(D,X,Y) F R O M REACH(O,X,Zl n REACH(D,Z,Y) 1
RZ: R E P L A C E REACHkD,cX>,COUNT,E>,Y,Z) BY REACH(D,Y,Zl;
R 3 : I N F E R REACHkD,cY>.NEXT,Z>,X,W)
F R O M REACH(O,X,Y) n REACH(D,Z,W) n -INBETWEEN(D,Y,Z,W):
Rule R I is implied by the transitivity of Reach. Rule R2 states that operations on the COUNT
field, i.e., Xf.COUNT e E, preserve loopfreeness. Finally, rule R3 states some conditions under
which the assignment, Yt.NEXT c 2, p r e s e r v e s loopfreeness between X and W. We can justify
the rules by proving them from the recursive definition of Reach given in 3.2.3. It is a
challenging exercise to construct axiomatizations of Reach that are complete in the sense that ail
satisfying interpretations are isomorphic to linear lists.
Finally, suppose we reverse the last two statements of INSERT:
-
BEGIN
NEW (Zl :
YkNEXTeZ;
Zf.NEXT+Yf,NEXT
END;.
The result of the attempted verification is:
26
Part 1: introduction to the Stanford Pascal Verifier
Simplified Verification Condition: INSERT 1
(REACH (#WORD, ROOT, Y 1 n
REACH(#WORO,Y,SENTINEL) n
YeSENTINEL n
YzNIL n
POINTER-TO (ROOT, #WORD) n
POINTER-TO(Y,#WORD) n
PO I NTER-TO (SENT I NEL, #WORD) n
POINTER-TO(Z,#WORD) n
-POINTER-TO (Z-0, #WORD) n
#WORD-l =<#WORDuZ-0,
cY>,
<#WOROcY~,.NEXT,Z-0>> n
#WORD-B=<#WORD-1,
cz-03,
<#WORDJcZ_0>,.NEXT,Z8>>
-b
REACH(#WORD_0,ROOT,SENTINEC) 1
The identifier Z-0 represents the new value of Z; *WORD-0, and *WORD-I are reference classes
resulting from operations performed by INSERT. The conclusion of the VC is that *WORD-O is
loopfree between ROOT and SENTINEL. But if we look at the expression for #WORD-O in the
premise (this expression results frown simplifications obtained from applying the data structure
rules) we see that the NEXT field of Z-0 is Z-0, clearly a loop. As the expression for *WORD-I
s h o w s t h a t t h e N E X T f i e l d o f Y i s p o i n t i n g t o Z-0, s o t h i s l o o p i s b e t w e e n R O O T a n d
SENTINEL, the desired result is false.
’
5.8 A larger example
We now present a verification of a simple parser. Here we have available the well developed
theory of context free grammars to assist us in documenting the parser. This theory provides us
with the necessary concepts. Using user defined predicates and rules, these concepts can then be
defined for use in the verification.
5.8,1 T h e o r y
We will briefly review the theory underlying t h e p r o o f . A context free grammar is a tupie
. CT, NT, P, (J}> where T and NT are the sets of terminal and nonterminal symbols, respectively.
The character J is a distinguished start symbol in NT and P is a relation over NT x (TuNT)*.
The sets T, NT, a n d P are ail finite. Whenever <I, t> is in P, then Y is of finite length.
T h e r e l a t i o n ‘I=:>” is defined over (TuNT)* x (TuNT)* as follows:
27
Part I: Introduction to the Stanford Pascal Verifier
We use periods to denote the concatenation of s e q u e n c e s over
defined to be the reflexive and transitive closure of ->.
(7WVT)*.
The relation “=>*” is
The goal of the parser is to determine whether or n o t a g i v e n s e q u e n c e o v e r T* is In the
language generated by the grammar; i.e., whether J ->* u for the input u. To express the theory
in our assertion language we introduce the following two predicates:
isprod(t, w) iJf 4, w> c P
isderiv(x, v) iff x E NT
A
a, v> c =>*
From the definition of =>* one immediately gets two lemmas
isderiv(x, x)
(isdertv(x, u.t.v) A iJprod(l, w)) 3 ideriv(x, u.wd)
5.8.2 The parsing algorithm
The parsing algorithm is standard (see [I], p 177); we use a stack automaton and generate a top
.down leftmost derivation of the input string. More precisely, we start with a stack containing the
s t a r t s y m b o l J. T h e n w e r e p e a t e d l y t a k e t h e t o p e l e m e n t f from the stack and if it is a
nonterminal symbol we push a w on the stack such that ispro&, w). Otherwise, if t is a terminal
symbol and it conforms with the first symbol in the input, we skip this first symbol. If none,of
these cases applies we report an error.
5.8.3 Implementation
First we decide upon the representation of the sets T, NT, and P in our program. The set T
yill b e a n e n u m e r a t e d t y p e c a l l e d lo&en and the set N T will a l s o b e a s t y p e nonterm. W e
introduce a special type for TuNT; this will be a record called item. Note that this could well be a
variant record; our system does not support vai-iant records as such but does provide union types.
Sequences, that is elements from T* and (TuNT)“, are represented as files; i.e., T* corresponds to
token’sequence, a file of token and (TuNT)* corresponds to f-W-sequence which is a file of item.
Note that for an actual implementation we would have to change f-nf-sequence to some type t h a t
can be represented in memory (e.g., linked lists). However, for the presentation of this example we
will use files; a change in t h e d a t a s t r u c t u r e w o u l d n o t a f f e c t t h e overall structure of the
verification.
28
Part I: Introduction to the Starrford Pascal Verifier
The representation of P is left undefined at this point; we assume the existence of an external
procedure isrhs which given t will return a w such that ispro&, w) holds. The decision of what
production is to be applied next is hidden inside isrhs and not specified further. To allow a
reasonable implementation of isrhs we pass as an additional parameter the next character of the
input, as lookahead. Thus our parser can deterministically recognize any LL( t) grammar.
T h r e e e x t e r n a l p r o c e d u r e s empty, push and fop implement a stack of item. Note, that push
pushes a whole sequence on the stack rather than a single element.
An external procedure
CYYOY
is used to issue error messages.
We distinguish between single elements of (TuNT) and the sequence of length one of (TuNT)*;
the function make-sequence takes an x E (TuNT) and converts it into <x> c (TuNT)*.
5.8.4 Specifications
As might be ob_vious by now, we cannot prove that the parser will accept every legal input string,
because we have not made strong enough assumptions about ids.
Instead we will prove the following statement: if the parser terminates and does not issue an error
message, then the input st ring is in the language generated by the grammar
This might seem to be a very weak statement; it is, however, a good illustration to demonstrate the
difference between robustness, rehabrllty, and correctness. Wtth a suitable implementation of isrhs
the parser will reliably parse any legal input string; an implementation of the procedure Errol can
guarantee a reasonable recovery from syntax errors, thus making the program robust. In the case
where the parser terminates without an error message, the program proof will guarantee a correct
parsing of the input regardless of the actual implementations of error and ids.
In writmg the assertions for this program we use the following functions:
imlted
concal
appentf
con I
.
maps a sequence over T* into a sequence over (TuNT)*
concatenates two sequences
appends a single element to a sequence
places a single element in front of a sequence.
The Invariant of the main loop states that the Input read so far concatenated with the contents of
the stack is derivable from the start symbol. There is no magic in finding this invariant; it
corresponds closely to the induction hypotheses of the formal proof that each context free
grammar is accepted by a non-deterministic push down automaton [ ll,(pl77).
To be able to formulate the invarlant we include a virtual variable Jource-read which at any
point contarns the portion of the Input read so far.
29
Part I: htroductiou to the Stanford Pascal Verifier
5.8.5 R u les
The rules necessary for the proof of the parser can be divided into two parts. In the first part, we
have rules describing the properties of isprod and isderiv. Furthermore we have to specify
properties of the auxiliary functions used, i.e., append, concal, conl, Imbed, make--sequence.
T h e r u l e s ISDI and ISDZ f o r m u l a t e t h e t w o l e m m a s f o r isderiv mentioned above. The rules
IMBI through IMB6 express that imbed distributes over make-sequence, con1 etc. IMB7 and
IMB8 define imbcd for a single element, i.e., this is mapped into one component of the record. In
the second part, we give rules that express trivial facts about sequences.
The final rulefile is:
RULEF I LE (PARSER)
CONSTANT NULL-SEQUENCE, I NFOl ;
ISDl: INFER ISOERIV(X,MAKE-SEQUENCE(X))r
ISDZ: INFER ISDERIV(X,CONCAT(Z,CONCAT(R,T)II
ISDERIV(X,CONCAT(APPEND(Z,L),T))
ISPROD(L,R):
FROM
A
I MB1 : REPLACE I MBED (MAKE-SEQUENCE (XI 1 BY MAKE-SEQUENCE (I MBED (Xl 1;
IMBZ: R E P L A C E IMBEO(CON1 (X,Y) 1 BY CON1 tIMBED( IMBEOIY) 1:
IMB3: R E P L A C E CONCAT(IMBED(X),IMBED~Y~~ BY IMBED(CONCAT(X,Y));
I M B 4 : R E P L A C E IMBED(CONCAT(X,Y)) BY CONCAT(IMBED(X),IMBEOo);
IMBS: R E P L A C E APPENDtIMBED(X), IMBEDtY) 1 B Y IHBEDtAPPEND(X,Y)):
I M B 6 : R E P L A C E IMBED(APPEND(X,Y)) BY APPEND(IMBED(X),IMBEDO):
IMB7: WHENEVER IMBEDtX) FROM TRUE INFER X=IMBED(X1~INFOl;
IMB8: WHENEVER X.INFOl FROM TRUE INFER X=IMBED(X.INFOl);
WHENEVER EMPTY(X) FROM EMPTY(X) INFER X=NULL-SEQUENCE:
NSl:
NSZ: FROM TRUE I NFER I MBED (NULL-SEQUENCE 1 =NULL-SEQUENCE :
NSlA: W H E N E V E R EMPTY(X) F R O M - E M P T Y ( X ) I N F E R X+NULL-SEQUENCE; ’
MS1 : REPLACE CONCAT (MAKE-SEQUENCE (X1, YI BY CON1 (X, Y) ;
APPl : REPLACE APPEND (NULL-SEQUENCE, XI BY MAKE-SEQUENCE (XI ;
FRl: WHENEVER FIRST(X) FROM TRUE INFER CONl(FIRST(X),REST(X))rX:
CON1 : REPLACE CONCAT (X, CON1 (U, V) 1 BY CONCAT (APPEND (X, U) , V) ;
CONZ: REPLACE CONCAT (APPEND (X, U) , VI BY CONCAT (X, CON1 (U, ‘0 1:
CON3: REPLACE CON1 (X, NULL-SEQUENCE) BY MAKE-SEQUENCE (Xl ;
CON4 : REPLACE CONCAT t X, NULL-SEQUENCE 1 BY X:
CON5: REPLACE CONCAT (NULL-SEQUENCE, X1 BY X;
EOF: REPLACE EOF(X) BY EMPTY(X);
We start out by attempting to verify the following version of the parser:
30
.
Part I: Introductiorr to the Stanford Pascal Verifier
PASCAL
TYPE
TOKEN
NONTERM
- (START-SYMBOL, AND~SOMEJlOREI :
TOKEN-SEQUENCE
TERM-OR-NOT
- FILE OF TOKEN;
- (NONTERMINAL, T E R M I N A L ) :
I TEM
- RECORD
KIND: TERM-OR-NOT;
I NFOl : TOKEN:
I NFOZ t NONTERM
END:
T-NT-SEQUENCE
VAR
- (EMPT;
IOENT,
NUMBER,
PLUSJ3YMBOL)
ANOJlANYJlORE I ;
- FILE OF ITEM:
SOURCE, SOURCE-READ
R, STACK
STRT, T
LOOK
DO N E
:
:
:
:
:
TOKEN-SEQUENCE;
T-NTJ3EQUENCE:
ITEM;
TOKEN:
BOOLEAN:
PROCEDURE ERROR:
ENTRY TRUE;
E X I T ERRORJlSG(lI:
EXTERNAL :
P R O C E D U R E ISRHSWAR R: T-NT-SEQUENCE: T: ITEM: LI TOKEN) :
ENTRY TRUE:
E X I T ISPROD(T,RI;
EXTERNAL:
% Procedures implementing a stack %
FUNCTION EMPTY (ST: T-NT-SEQUENCE) : BOOLEAN!
ENTRY TRUE:
EXIT TRUE:
EXTERNAL:
% R e t u r n t h e t o p o f t h e p a r s i n g s t a c k , p o p this e l e m e n t %
PROCEDURE TOP WAR X: ITEM) :
GLOBAL (STACK) :
I N I T I A L STACK&B:
ENTRY TRUE :
EXIT (-EMPTY (S0I -+ SBeCON1 (X,STACKI I A ( E M P T Y 60) -) E R R O R - H S G (1 I I :
EXTERNAL:
Part I: Introduction to the Stallford Pascal Verifier
% P u s h x o n t h e p a r s i n g s t a c k : note that we push whole sequences
rather than single elements. %
PROCEDURE PUSH (X: T-NT-SEQUENCE) ;
..
GLOBAL (STACK) ;
IN1 T I A L STACK&B;
ENTRY TRUE;
E X I T STACK=CONCAT(X,SB);
EXTERNAL;
% This function converts an element into a sequence of one element. %
FUNCTION MAKE-SEQUENCE (X: I TEM) t T-NT-SEQUENCE!
ENTRY TRUE:
EXIT TRUE;
EXTERNAL;
% Main program %
IN1 T I A L SOURCE=SOURCEB:
ENTRY -ERROR-MSG (1) A EMPTY (STACK) A
EMPTY (SOURCE-READ) A -EMPTY (SOURCE) ;
EX I T -ERROR-MSG (1 I -) ISOERIV(STRT, IMBED(SOURCE0) 1 t
BEGIN
STRT,KIND+NONTERMINAL: STRT, INF02+START_SYHBOL;
PUSH (MAKE-SEQUENCE (STRT) 1:
READ (SOURCE, LOOK) :
I N V A R I A N T -ERRORJlSGW +
(SOURCEB=CONCAT (SOURCE-READJON (LOOK,SOURCEI 1
ISOERIV(STRT,CONCAT(IMBEO(SOURCE~READ),STACK~~~
WHILE N O T EOt=(SOURCE) 0 0
BEGIN
TOP(T):
IF T.KINO=‘TERMINAL T H E N
IF T, INFOlzLOOK THEN ERROR E L S E
BEGIN
WR I TE (SOURCE-READ, LOOK) ;
% virtual %
READ (SOURCE, LOOK)
EN0
ELSE BEGIN
ISRHS(R,T,LOOK);
PUSH (RI
EN0
ENO;
IF NOT EMPTY (STACK) THEN ERROR;
END.
A
An aitempt to verify this program succeeds in establishing the truth of 4 out of the 5 verification
conditions generated. The following VC is the only one which does not simplify Co TRUE:
1 -ERROR-MSG ( 1) A
EMPTY (STACK) A
EMPTY (SOURCE-READ)
-EMPTYtSOURCE) A
SOURCE=SOURCEB A
A
32
Part i: Introduction to the Stanford Pascal Verifier
STRT~3=&TRT,.KIND,NONTERMINAL> A
STRT~2=&TRT~3,.1NFO2,START_SYMBOL> A
STACK_7=PUSH_STACK (MAKE-SEQUENCE (STRT-21 ,SOURCE-READ)
STACK 7=MAKE_SEQUENCE (STRT. 2) A
SOURCE_4=READ+-F (SOURCEB, COOK1 A
LOOK-4=REAO-X-X (SOURCE0,LOOK) A
LOOK_4=FIRST (SOURCE01 A
SOURCE-4=REST (SOURCE01 A
EMPTY (SOURCE-31 A
SOURCEB=APPEND (SOURCE-READ-2, LOOK-31 A
I SDERI V (STRT-2, CONCAT (I MBED (SOURCE-READ-21, STACK-61 1
EMPTY (STACK-61
-P
ISOERIV(STRT~2,IMBED(SOURCE0~))
A
A
One way to prove this formula is to show that
imbed(~ource0) = conc&t(imbed(Jource-ye~~-2), 5tuck-6).
Given that sour53 and stack.6 are both empty this means showing
imbed(append(source-read~2,look.3))
- ittlben(source-Yean-2).
But unfortunately, this VC is false; it cannot be proved from any set of consistent rules.
Consequently, the VC reveals an error in our program.
Investigating further, we find that the unproved verification condition comes from the path
which starts at the entry assertion of the main program, goes to the main Ioop, and then to the
exit assertion of the main program. Looking at our program closely we find that in fact the main
loop is not coded correctly. In the case where we read the last token from source into lo& the
main ioop will terminate. However, we haven’t yet made the necessary reductions to derive the
entire input string.
Having found this error we change the program to the following one:
% M a i n progranl %
IN1 T I A L SOURCE=SOURCEB;
ENTRY -ERROR-MSG (1) A EMPTY (STACK) A
EMPTY (SOURCE-READ) A -EMPTY (SOURCE) ;
EX I T -ERROR-MSG ! 1) 3 ISDERIV(STRT,IMBED(SOURCE0~~;
BEGIN
STRT. K I NDcNONTERMI NAL: STRT, I NF02eSTART~SYMBOL:
PUSH (MAKE-SEQUENCE (STRTI 1;
READ (SOURCE,LOOK) ;
DONEeFALSE:
I N V A R I A N T -ERROR-MSG(1) +
((-DONE + SOURCE0=CONCAT(SOURCE~READ,CONltLOOK,SOURCE1~~
ISOERIV(STRT,CONCAT(IMBED(SOURCE~READ),STACK~~ A
(DONE -) (EMPTY (SOURCE 1 A SOURCEB=SOURCE-READ) 1)
WHILE NOT OONE DO
BEGIN
33
A
Part I: Introduction to the Stamford Pascal Verifier
TOP(T):
IF T.KIND=TERMINAL T H E N
I F T.iNFObLOOK THEN ERROR ELSE
BEGIN
% virtual %
WR I TE (SOURCE-READ, LOOK) ;
I F EOF(SOURCE) T H E N OONE+TRUE E L S E READ(SOURCE,LQOKI
END
ELSE BEGIN
ISRHS(R,T,LOOK):
PUSH tR)
END
END:
IF NOT EMPTY(STACK1 THEN ERROR;
END,
This corrected program can be verified using the rulefile given above. To show that this proof is
not at all trivial we include one of the unsimplified VCs:
(-DONE A
(-ERRORJlSG ( 1)
3
(-DONE
+
SOURCEB=CONCAT (SOURCE-READ, CON1 (LOOK, SOURCE) 1) /\
~;~~E$IVtSTRT,CONCAT(IMBEO(SOURCE_REAO),STACK1~ A
-b
EMPTY (SOURCE) A
SOURCEB=SOURCE-READ)) A
(EMPTY (STACK)
+
ERROR-MSG (1) 1 A
(-EMPTY (STACK)
+
STACK=CONl (T-0, STACK-21 1 A
T-B=TOP-X (T,STACK) A
STACK-Z=TOP-STACK (T, STACK) A
T-B.KIND=TERMINAL A
T-0. I NFOl *LOOK A
ERROR-MSG (1) A
-ERROR-MSG (1)
3
(-DONE
-b
SOURCE0=CONCAT(SOURCE~READ,CONl~LOOK,SOURCEI~~
ISDERIV(STRT,CONCAT(IMBEO1SOURCE~READ) ,STACKJ I
t DONE
-b
EMPTY (SOURCE) A
SDURCEB=SOURCE-READ) 1
34
A
A
P A R T iI
i. DIFFERENCES FROM STANDARD PASCAL
The verifier accepts most of the constructs of Pascal, modified in some cases for assisting
verification. Whai follows is a list of the known differences between the language accepted by the
verifier and “standard” Pascal as presented in Jensen and Wirth (156 this list does not discuss the
syntax or semantics of the rule language also accepted by the parser.
1.1 Comments
The scanner for ail code ignores statements surrounded by percent (7.) signs. Thus, comments may
be added to code in this manner.
1.2 Program f&s
The Pascal code begins with the word PASCAL, The last character in the file should be a
period (.). An end-of-file, except from the terminal, is accepted in lieu of a final period. A main
program need not be present. Procedures must have a body, but it can be empty.
1.3 Procedure definitions
The GLOBAL, INITIAL, ENTRY, and EXIT statements (in that order) may follow a
PROCEDURE or FUNCTION statement. The first three are optional; the last one must be
there. For example:
P R O C E D U R E P(VAR X : I N T E G E R ; Y : R E A L ) ;
G L O B A L ( A ; V A R 2);
XHere the global Z may be changed by this procedure;
the global A may be referenced by this procedure.%
INITIAL X=XO,Z=ZO; ZXO and YO may appear only in assertions.%
E N T R Y FOO(X,Y,A);
E X I T MUMBLE(X,XO,Y) A BUMBLE(A,ZO);
T Y P E .....
V A R ,....
B E G I N . . . . . END;
Functions may not have an INITIAL statement,
35
Part Ii: Ckapter 1: Differewes from Standard Pascal
In the outermost block of a program, the ENTRY and EXIT assertions appear immediately
p r e c e d i n g t h e BEG;IN that starts the block. The order is ENTRY then EXIT, or just EXIT. An
lNJTIAL statement, if present, precedes the ENTRY/EXIT assertions. Thus:
PASCAL
T Y P E .....
V A R .....
P R O C E D U R E S A N D F U N C T I O N S . . ..e
E X I T MUMBLE(A,B);
BEGIN
Xmain block of the program%
END.
1.4 Assertions
The ASSERT, COMMENT, and ASSUME documentation statements have been added to Pascal
for verification purposes:‘
ASSERT <formula>
COMMENT <formula>
ASSUME <formula>
The ASSERT statement breaks a proof into two separate verification conditions. The
COMMENT statement does not cause a break, but adds an additional fact (which must be
verified) to the verification condition. The ASSUME statement does not cause a break; it adds
an additional assumption to the verification without requiring proof. For futher details see
Appendix C.
Each repetitive statement requires an invariant to be specified. Thus:
-
INVARIANT <formula> WHILE ---- DO ---FOR ---- INVARIANT <formula> DO ---REPEAT ---- UNTIL ---- INVARIANT <formula>
1.5 Blocks
As in PASCAL, declarations must appear in the order LABEL, CONSTANT (or CONST),
TYPE, VA R, functions and procedures. Unlike Pascal, you may h a v e more than one CONST,
TYPE, or VA R statement.
36
Part II: Chapter i: Differerrces from Startdard P a s c a l
1.6 T y p e s
A previously known integer or real variable identifier may appear as one of the array bounds for
the purpose of defining an array type by subrange.
Variant records and sets have not been implemented.
passed as parameters.
Functions and procedures may not be
The type CHAR has been implemented, but only character constants one character long may
appear in programs. Packed arrays are not implemented. The character delimiter is the singlequote e.g., ‘a’.
A TYPE may not be redefined as another TYPE within its scope. It may be redefined as a
constant, var, procedure, or function; however that makes the type invisible within the scope of
that redefinition and will cause a syntax error if any attempt is made to reference vars of the
redefined type.
1 . 7 F u n c t i o n s me
There is very strict enforcement of rules to ensure that functions have no side-effects. The
following are prohibited in functions (not procedures):
VA R parameters
The NEW statement
Calling procedures that change globals
Changing globals
READ, WRITE, and REWRITE statements
Note that a reference class is a global. Thus, assigning to any dereferenced pointer will cause an
error.
1.8 hf.NJt/OUpUt
T h e o n l y l/O s t a t e m e n t s a l l o w e d a r e E O F , R E A D , R E W R I T E , a n d W R I T E . E O F t a k e s a n
entity of type FILE and returns T R U E o r F A L S E . READ and WRITE each take only two
. arguments; the first is a file and the second is an entity of the same base type as the file. Files
may be declared in the usual manner; however, an entity of type FILE may appear in executable
code only in the READ, WRITE, and REWRITE statements (or be passed as a parameter).
37
Part II: Chapter 1: Differences from Standard Pascal
1.9 Global variables
Any global variable that can be changed in a procedure must appear in a G L O B A L s t a t e m e n t
+ for that procedure, in a list preceded by VAR. Any global variable that can be referenced in a
procedure must appear in a GLOBAL statement for-that procedure, either preceded by VAR or
not. It will generally lead to VCs which are easier to prove If a gtobai is not preceded by VAR
unless required.
Any global variable that is referenced by a function must appear in the GLOBAL statement for
that function. Functions may not have VAR global variables.
Giobais passed as parameters to another procedure are checked to be in the appropriate
GLOBAL list of the first procedure.
A variable in your program may not have the same name as a function, predicate, or record field.
However, the same name may be used as a record field in two different types of records.
1.10 Virtual variables arlb Passive statelrlerlts
T h e w o r d V I R T U A L m a y p r e c e d e t h e w o r d V A R In a declaration or a procedure or function
parameter definition. I n a d d i t i o n , t h e w o r d V I R T U A L m a y p r o c e e d a n o n - V A R p a r a m e t e r
definition. V I R T U A L e n t i t i e s m a y a p p e a r i n d o c u m e n t a t i o n ( E N T R Y , E X I T , A S S E R T ,
COMMENT, ASSUME, PASSIVE) or they may be passed to other virtual entities. They m a y
not be used elsewhere.
The PASSIVE statement has been added to permit assignment to virtual variables. Jt is merely
an assignment statement preceded by the keyword PASSIVE. This is the only way in which a
virtuai variable may be assigned to.
J.1 I Operator precedence
-The precedence for operators appearing in documentation and rules is different than in Pascal.
In particular, there are many more levels of precedence. T h e s y m b o l “v” is the lowest priority,
then “ A ”, and so on, in what seems to be a natural ordering (the specific ordering is contained in
the syntax charts). For this reason, the symbols used In documentation to represent the logical
operators are different than the AND, OR, and NOT of Pascal. For this purpose, documentation
i s the f o r m u l a s f o l l o w i n g I N V A R I A N T , C O M M E N T , A S S E R T , A S S U M E , E N T R Y , a n d
EXIT.
A limited form of type checking is performed in ail documentation statements noted above. A
variable appearing within a statement must be declared and known; expressions must make sense
(thus addition cannot be performed on a Booiean variable, for example). However, there Is no
38
Part II: Chapter I: Differences from Standard Pascal
requirement that function and predicate names be known. Parameters to these functions and
predicates are not checked. The exception to this is the PASSIVE statement, which must meet
the same (stricter) type-checking requirements as the assignment statement.
As part of the no side-effect enforcement, the verification condition generator checks to ensure
that the same data may not be passed to a procedure in two different ways. This situation is
signalled by a syntax error.
1.12 ilniorr types
The construct UNION has been added to replace variant records. UNION is a general type
constructor which can be combined with other types in the same way as ARRAY and RECORD.
There is a TAG function for determining the tag of a union variable, and there are selection and
construction functions.
The UNION type declaration has the form
T Y P E u n t y p e - UNION al: tl; . . . ; an: tn END;
where the ti are types and the al are constants of an enumerated type or integer subrange. If the
ai are of an enumerated type, the type must have been declared previously, and each of its
elements must appear once in the UNION declaration.
Assuming that u and ul are variables of a union type untype (above) and x is a variable of one
of the ti types, then the following operations are defined:
VA R u, u I: untype;
x: ti;
SELECTION
u:ai returns the ai component of u.
At any time, only one of the components of u exits. Selection of u:ai is an error if the tag of u is
n o t al:
TAG function
TAG(u) returns one of the constants ai, the current tag.
CONSTRUCTORS
untype:ai(x) returns a value of untype with tag al.
As a consequence of the declaration of untype, separate constructor functions are defined for each
of the ai. The constructor untype:ai takes values of type ti and converts them into values of the
union type.
39
Part ii: Chapter 1: Differewes from Stalldard P a s c a l
ASSIGNMENTS
U := u 1;
u:ai := x; valid only if TAG(u)=ai
u := untype:ai(x);
U :- x; implicitly applies construction
Assignment to a union variable of a value of the same type is always permitted. An assignment
to a component of a union variable, as in the second statement, is permitted only if that
component currently exists in u. In the third statement, u is set to the union value constructed
from the value of x. The fourth statement is equivalent to the third one: the parser determines
from the mismatch between the types of u and x, that the constructor untype:ai must applied.
Example: The data structure and basic operations of LISP defined in Pascal with union types.
PASCAL
T Y P E T A G S = tA,O,N):
LISP--F w;
DTPR = RECORD
CAR: LISP;
CDR: L I S P
END;
ATOM - RECORD
VALUE: LISP;
PLIST: LISP
END:
U
- UNION
0: DTPR;
A: ATOM;
N: INTEGER
END:
PROCEDURE CONS(X,Y: LISP; VAR RESULT: LISP);
G L O B A L (VAR #U):
E X I T TAGtRESULTtbD A RESULTt:D,CAR-X A RESULT~:D.CDR=Y;
VAR CELL: DTPR:
BEGIN
NEW (RESULT) ;
CELL.CAR: =X;
CELL.CDR: =Y;
RESULT?: =U: 0 (CELL)
END;
F U N C T I O N CAR(X: LISP): LISP;
GLOBAL (#U) ;
ENTRY TAG (Xt) =D;
EXIT TRUE;
BEGIN
CAR: =X?: 0. CAR
END;
40
Part 11: Chapter I: Differewes from Standard Pascal
PROCEOURE PLUS(X,Yr LISP; VAR RESULT; LISP11
GLOBAL (VAR #U) :
ENTRY TAG (X?) =N n TAG (Y?) =N;
E X I T TAG(RESULTf)=N A RESULTt:N=Xt:N+YtiN;
BEGIN
NEW (RESULT) ;
RESULT’b
-XflN+Yt:N:
.
% n o t e i m p l i c i t a p p l i c a t i o n o f &NO t o
convert INTEGER to type U %
END:
41
2JSERCOMMANDS
A system command consists of a command keyword, possibly followed by some arguments, and a
terminating “;“. The semicolon must always be present. Most command keywords can be
abbreviated to an initial substring that identifies the command unambiguously.
There are four classes of commands:
(I) imperative commands, which call the various parts of the verifier:
(a) READ, READVC and PRINTVC for reading (parsing) and writing files
in user-readable format;
(b) SIMPLIFY and RESIMPLIFY for calling the theorem prover;
(c) DUMP commands and LOAD commands for writing and reading files in
internal format;
(d) DELRFILE, DELRULE for selective deletion of rulefiies and rules.
(2) commands that set system parameters: ALIAS, SET, RESET, OPENFILE,
CLOSE. -(3) commands for obtaining some sort of information from the system: HELP, SHOW,
STATUS.
(4) commands for system control: QUIT, LISP.
The following sections describe the command syntax informally; the formal syntax is given in
Appendix A.
2.1 Imperative cotntnallds
-
Most of the imperative commands take a file name as an (optional) argument. The syntax of file
names is exactly the same as at monitor level. Unless specified otherwise, the system will assume
unit DSK: and the current default PPN (see also the ALIAS command). Some commands will
assume default file names if parts of a file name are omitted. The defaults for file names are
explained in the description of the individual commands. In order to override a default extension
an empty extension can be forced by “.“; e.g., FOO.[X,BAZ].
’ READ comnallds
A READ command parses source code (rulefiles, programs, VCs), i.e., input in external format.
Input is read either from the keyboard or from a file. The system determines from the keyword
(the first word in the file) what kind of data it is reading. It announces what it is doing, and
gives the names of the VCs and rules. A READ command takes a file name as (optional)
argument. If no argument is given, reading is done from the keyboard. The command READ is
42
Part Ii: Chapter 2: User Commarlds
used for parsing Pascal source code and rulefiles. The command READVC is for reading in
VCs in external format. The command READ also knows about VC-files, i.e., the c o m m a n d
“READ FOOVC;“. is equivalent to “READVC FOOVC;“. Examples:
READ;
READ FOO.BAR;
REA DVC FOO;
R EA D FOO.VC;
parses source code typed in from the terminal;
parses the file FOO.BAR;
parses the file FOO.VC, assuming that it contains VCs;
does exactly the same.
A READ command will not accept files with the extensions CRL, CVC, or CTB. Those files
have to be read into the verifier using a LOAD c o m m a n d .
PRINTVC
The c o m m a n d PRINTVC prints out VCs, either to the terminal or to a file (or both). It takes a
VC-specification and a file name as (optional) arguments. If no file name is given, printing is to
the terminal. T h e syntax of the arguments is the s a m e as for SIMPLIFY (see below for
ex a mples),
SIMPLIFY c o m m a n d s
The command SIMPLIFY calls the theorem prover. The prover attempts to simplify one or more
VCs, using the rules that are currently loaded. The command takes a VC-specification, a file
name and system parameter settings as (optional) arguments. If no VCs are specified, all current
VCs are taken. If a file name is given, output is to that file; a copy can also be displayed on the
terminal. If no file name is given, output is to terminal only. A list of system parameter settings
(in parentheses) may appear either right after the command keyword or at the end (before the “;‘I).
The command can be abbreviated to “S”. Examples:
SIMPLIFY;
S (TRACE,PROOFDEPTH=Q
SIMPL FOO l(SHOWGOAL);
SIMPL TO FILE.EXT[A,FOO];
a
S I M P L + FILE.EXT[A,FOOl;
SIMPL MAIN COPY TO AAA;
simplify all current VCs and display them on the
terminal;
simplify all VCs with TRACE turned on and
PROOFDEPTH set to 5;
simplify VC 1 of FOO and display subgoals
during the proof;
simplify current VCs and write simplified VCs
onto file FILE.EXTEA,FOOj;
same as previous example, “4“ may be used
instead of “TO”;
simplify VCs of MAIN; write simplified VCs
onto file AAA and display on terminal.
The RESIMPLIFY command takes the last VC returned by the simplifier and has another go a t
it. Sometimes this will have a beneficial effect.
DUMP commands
The group of DUMP commands inciudes the commands DUMP, DUMPVC, and DUMPRULE.
A DUMP command produces a file containing VCs (DUMPVC), or rules (DUMPRULE), i n
43
Part Ii: Chapter 2: User Commands
internal format so that at some later time they can be loaded directly using a LOAD command
without requiring parsing. All DUMP commands use default file names. If no file name is given
as argument, the default file name is VERIFY with an extension that depends on the command:
CVC for VCs, CRL for rulefiles. These standard extensions are always used when a file in
internal format is being created unless the user explicitly specifies a different (or empty) extension.
T h e s h o r t c o m m a n d D U M P d u m p s b o t h VCs and rules to appropriately named files; the
argument to DUMP must be a simple file name without extension or PPN, It is advisable - and
convenient - to make use of the default extension feature as the LOAD commands also know
about them. Examples:
DUMPVC FOO;
D U M P V C FOO.BAR;
D U M P V C FOO.iP,PR01;
DUMPRULE F O O ;
DUMP FOO;
write a file FOOCVC containing current VCs;
write a file FOO.BAR containing current VCs;
write a file FOOEP,PRO] containing current VCs;
write a file FOO.CRL containing current rules;
write files FOOCVC and FOOCRL containing
current VCs and rules, respectively.
If more than one rulefile exists, DUMPRULE will dump the one which was most recently parsed.
A particular rulefile may be specified for dumping by giving its name as a second (optional)
argument. Example:
DUMPRULE FILE, SRULES;
d u m p rulefile SRULES onto file FILE.
LOAD commands
The group of LOAD commands includes the commands LOAD, LOADVC, and LOADRULE.
A LOAD command reads in a file which was previously created by a DUMP command. LOAD
commands use the same conventions for naming files as the DUMP commands. If no file name is
specified for LOAD, or if no extension is specified, all loadable files with the default name
(VERIFY) and default extensions (CVC, CRL) will be used. The “long” commands load a file
with an extension corresponding to their suffix. Examples:
LOADVC FOO;
LOAD FOOCVC;
LOADVC;
LOAD FOO;
loads the file FOOCVC;
does exactly the same;
loads the file VERIFYCVC;
loads whichever (or all) of the files
F O O C V C a n d FOOCRL exist.
D E L E T E comrnauds
Rulefiles and rules can be deleted seiectively by the commands
D E L R F I L E <list of rulefiles>;
D E L R U L E <list of rule names>;
for rulefiles, and
for rules.
The command DELRFILE without argument deletes all rules (so beware!).
44
Part II: Chapter 2: User Commands
2.2 Set t i irg system parameters
ALIAS
The ALIAS command, like the monitor command, changes the project/programmer name (PPN)
the verifier uses as default. It affects all file input and output to and from the verifier.
Examples:
changes the default PPN to WER,FOOl;
prints out the current default PPN.
A L I A S VER,FOO;
ALIAS;
SET, RESET
The user can set the values of various parameters that control the system. Parameter values can
be changed either for the rest of the session with the SET/RESET commands (“sticky” changes),
or temporarily in imperative commands. SET accepts as argument a list of parameters and
values; if no parameter value is given to SET, it uses T (for TRUE). RESET sets parameters to
their default values; this command accepts only a list of parameter names as argument. Examples:
S E T T R A C E , PROOFDEPTH=5;
RESET TRACE;
Sequences of SET command operands in parentheses may be included in a command string either
after the keyword or at the end preceding “;‘I (for examples see the explanation of SIMPLIFY).
The difference between setting parameters this way, or using SET/RESET, is that SET and
RESET settings are permanent; settings given in a command string apply only for the duration of
the command execution. If the same parameter name occurs twice, the first setting is overwritten.
The type of parameter value expected depends on the parameter name. The following list gives
user adjustable parameters with the type of their values:
natnum:
bool:
a
an integer greater than or equal to zero
a LISP flag: T or F (= NIL internally)
ASSERTDEPTH
CASEDEPTH
DEPTHTALK
PROOFDEPTH
RULE
SHOWFACT
SHOWGOAL
SHOWTEST
SUMMATCH
-TERMINAL
natnum
natnum
bool
natnum
bool
bool
boot
bool
bool
boo1
TRACE
TRACEFACT
TRACEVC
bool
bool
bool
maximum forward assertion depth;
maximum depth of nesting of forward cases;
signal whenever a depth bound is reached;
maximum backward proof depth;
enable rulehandler;
enable assertion display during proof;
enable subgoal display during proof;
enable display of tests made during proof;
enable special sum matching: extra subspace instance;
if set, file output (from SIMPLIFY and PRINTVC)
is also displayed on the termina).
enable proof tracing;
enable display of assertions made in trace output;
enable display of intermediate VCs during proof
(works only if TRACE is set);
45
Part ii: Chapter 2: User Cornrnallds
Current default values can be found using the SHOW command.
OPENFILE
The command OPENFILE opens a backup fiie. A backup file gets a copy of all the output from
the system that is displayed on the terminal. It takes a file name as (optional) argument; the
default file name is VERIFY.BKP. If the parameter (NOT) is included after the file name,
output goes to the file only. A backup file can be closed using the command CLOSE. Example:
OPENFILE F O O ( N O T ) ;
Note that output cannot go to two different files simultaneously. Thus the backup file has to be
ciosed before PRINTVC or SIMPLIFY can write onto other files, or another backup file can be
opened. The system will notify you if this is necessary.
CLOSE
The command CLOSE closes a backup file. The command takes no argument+
2,3 Query co~nnraRds
HELP
The HELP command provides information about various system features. It takes a keyword as
argument. “HELP;” gives some general information about the verifier and pointers to further
information. “HELP WHAT;” gives the list of topics for which help is available.
SHOW
The SHOW command displays the current values of system parameters. It takes a list of
parameter names (separated by commas) as argument. If no arguments are given, SHOW
displays the values of all parameters the system knows about.
STATUS
The STATUS command prints out a list of names of VCs, rulefiles and rules currently loaded. It
takes no arguments.
2.4 System control
QkJ IT
- The QUIT command is provided to allow one to exit gracefully from the verifier. “QUIT;” will
return you to the monitor.
LISP
T y p i n g “ L I S P ; ” to the system gets the user ‘to the Maclisp toplevel. .This command exists
primarily for system maintenance and test; the uninitiated user should never need to use it. Once
at LISP toplevel, evaluating (RESUME) will return control to the verifier command level.
46
Part II: Chapter 2: User Commands
R u II n i og tire system
When loading the system, it will print out some more or less useful messages. As soon as t h e
prompt character “>” appears, the system is ready to accept commands. The system tries to be
fairly talkative; when executing a command it always prints out something. Thus, if the prompt
character appears the system expects more input before It can execute the command (for example,
t h e t e r m i n a t i n g “;‘I may have been omitted). All file manipulation is announced to the user,
including full file names.
Error recovery
If for some reason or other the system ends up with a LISP error, evaluating (RECOVER) will
return control to verifier command level. Typing <control> P will do exactly the same. If the
error occurred in the simplifier, it will be reinitialized automatically.
47
3 , D E S C R I P T I O N O F T H E SIMPUFIER
3.1 Iutroductiorr
The prover has two components, a simplifier and a rulehandler (which is described in Part II,
Chapter 4). The simplifier finds a normal form for any expression over the language consisting
of individual variables, the usual boolean connectives, equality, the numerals, the arithmetic
functions and predicates +, -, s, and <, the LISP constant and functions NIL, CAR, CDR and
CONS, the functions ARRAYSTORE and ARRAYSELECT for storing into and selecting from
arrays, the functions RECORDSTORE and RECORDSELECT for storing into and selecting
from records, and uninterpreted function symbols. Individual variables range over the union of
the reals, the set of arrays, the set of records, LISP list structure and the booleans T R U E a n d
FALSE.
The simplifier is complete; that is, it simplifies every valid formula to WWE. Thus it is also a
decision procedure for the quantifier-free theory of reals, arrays, records, and list structure under
the above functions and predicates.
The following are some examples of simplifications:
2+ 3*5
17
P=-P
‘P
x - f(x) ’ md) - f(f(f(x)))
TRUE
x s y A y + d I x
TRUE
A
3*d L 2rd 2 v[2*x - yl - v[x + dl
The simplifier includes a number of cooperating special purpose provers, each a d e c i s i o n
procedure for a particular quantifier-free theory. For instance, there is one prover for arithmetic,
one for arrays, etc. Each prover has some modifications for use in the verifier; some of the
modifications are temporary and refiect only the present version.
3.2 Prover for arithmetic
The axioms of this theory are:
48
Part ii: Chapter 3: Description of the Simplifier
The numerals 2, 3, . . . and z are defined in terms of 0, 1, t, - and s in the usual way. We also
allow multiplication by integer constants; for instance, 2 * x abbreviates x t x.
T h e i n t e g e r s , r a t i o n a l s a n d r e a l s a r e ail models for these axioms. Any formula which is
unsatisfiable over the rationals or reals can be shown unsatisfiable as a consequence of these
axioms. T h u s o u r s i m p l i f i e r i s c o m p l e t e f o r t h e rationah or reals. It is not complete if the
variables range over the integers, since there are unsatisfiable formulas, such as x t x - 5, which
cannot be shown unsatisfiable as a consequence of the above axioms. T h e reason for the
incompleteness is that determining the unsatisfiability of a conjunction of integer linear
inequalities -- the integer linear programming problem -- is much harder in practice than
determining the satisfiability of a conjunction of rational linear inequalities. This incompleteness
is not as bad as it seems, since most formulas that arise in program verification do not depend on
subtle properties of the integers.
ln the present version, we have implemented one useful heuristic which makes the simplifier no
longer sound for reals or rationals but which catches much of the incompleteness concerning
integers. ln addition to 5, we allow c as a predicate symbol, but define x < y to be x t I s y.
Notice in the description of the simplifier that multiplication is NOT mentioned although it
appears in the examples. At the moment, we allow expressions such as 2 * x and there is some an
hoc code which tries to capture the more obvious properties of multiplication by constants, but the
code makes no pretence of being complete. (The quantifier-free theory of integers under addition
and multiplication is undecidable.)
3.3 Record prover
The irecord prover handles expressions involving storing into and selecting from records and
record fields. The following axioms are implemented:
49
Part II: Chapter 3: Description of the Simplifier
<r, .f, r.f> - r
+zr, .f, el>, .f, e2> - <r, .f, e2>
<r, .f, e>.f - e
<r, .f, e>.g - r.g
With one exception, these are the axioms of the quantifier-free theory of records. The one axiom
that is not implemented in the record prover concerns permutation >f terms within data triples;
t h a t i s , t h e a x i o m c<r, .f, el>, .g, e2> = <<r, .g, e2>, .f, el>. The reason for this omission is that
this axiom can lead to combinatorial explosion. It appears to be rarely necessary in proofs and
can be included as a rule if necessary.
The record prover can be turned on and off from LISP. Evaluating (RECORDPROVER) turns
it on (and is the default); (NORECORDPROVER) turns it off.
3.4 Array prover
The array prover implements the following axioms for arrays:
< a , 113, a[$ = a
<<a, 113, el>, Eil, e2> - <a, Eil, e2>
<a, [i], e>[j] - (if i - j then e else a[jN
Again the axiom for permutations within data triples is missing. There are at the moment
p r o b l e m s w i t h t h e a r r a y p r o v e r i n t h e v e r i f i e r ; b e c a u s e o f a n i n t e r f a c e p r o b l e m with the .
rulehandler, it is running much too slowly and requiring too much workspace. For this reason the
arrayprover in the simplifier is temporarily defaulted to be off. It can be turned on in two ways
from LISP. Evaluating (FASTARRAYPROVER) turns on a version which implements the first
two axioms above plus the axiom <a, [iI, e>[il - e; it therefore lacks the axiom 1 z j =) ca, ttl, e>[jl
aEj1. Evaluating (SLOWARRAYPROVER) turns on a version which implements the three
Axioms above. (NOARRAYPROVER) turns the array prover off and is the default.
3.5 List structure prover
Since Pascal does not have LISP list structure, the LISP special purpose prover has thus far not
been turned on in the Pascal verifier.
3.6 Remarks
Complete descriptions of the various parts of the simplifiers and the component special provers
appear in [22, 23, 241.
50
4,THERULELANCUAGE
4.1 Introductioll to rules
We give an informal description of the rule language. A precise description of the syntax is
given in Appendix A; this section is intended as a brief introduction to rules.
There are two types of rules: forward rules and backward rules. Roughly speaking, forward rules
add new facts to the data base of the theorem prover as a consequence of old facts. Backward
rules specify sets of subgoals which may be used in proving goals set up by the theorem prover.
Some rules may cause “case splitting,” which is the separation of a proof search into multiple
contexts for the purpose of considering cases.
For each kind of rule, we give a brief description of the syntax, logical meaning, and semantics.
The logical meaning specified is the “strongest” logical fact expressed by the rule. The semantics
describe how this fact will be used by the theorem prover in proofs.
Certain conventions are used in the description below. Brackets in a syntactic description indicate
an optional expression. A L I T E R A L i s a n a t o m i c f o r m u l a o r a n e g a t e d a t o m i c f o r m u l a . A
TRIGGER-EXPRESSION is an expression which contains no propositional operators and which
is not an individual variable. A REPLACEMENT-EXPRESSION is an expression which
contains no propositional operators. An expression is an expression in the assertion language.
51
Part II: Chapter 4: The Rule Language
4.1.1 Backward rules
SYNTAX
infer A [ f r o m B] [ w h e n e v e r TR-l , TR-2, . . .I
A: (the INFER clause) a conjunction of literals.
B: (the FROM clause) a conjunction of literals.
TR-i: a trigger-expression.
The WHENEVER and FROM clauses are optional. If there is no FROM clause, B is defaulted
to TRUE. If there is a WHENEVER clause, it must have at least one trigger.
LOGICAL MEANING
SEMANTICS
A backward rule “applies” when the prover is trying to prove any of the literals in the INFER
clause. If the FROM clause can be proved, the INFER clause is assumed to be proved. Multiple
rules interact through standard subgoaling techntques. If A is the propositional constant F A L S E ,
a contradiction w i l l b e d e r i v e d i f t h e F R O M c l a u s e c a n b e p r o v e d . T r i g g e r s i n t h e
WHENEVER clause restrict situations in which the rule will be applied to those in which
itlstances of each trigger have occurred as subterms. Proof of the literals in the FROM clause
proceeds from left to right.
EXAMPLES
infer
A
div
B s N from A<N
A
821
i n f e r Ordered(a, i , j) f r o m Orderedfa, i,k)
A
Ordered(a,k, j)
d
i n f e r ISOERIV(X,MAKE_SEQUENCE(X))
i n f e r ISDERIV(X,CONCAT(Z,CONCATtR,T))1 f r o m
ISOERIV(X,CONCAT(APPEND(Z,L),T)1
A ISPROO(L,R)
% T w o rules for verifying a context free parser:
ISDERIV(X,Y) m e a n s t h e r e i s a d e r i v a t i o n f r o m X t o Y:
ISPROD(L,R) m e a n s t h e r e i s a p r o d u c t i o n f r o m L t o R. %
52
Part II: Chapter 4: The Rule Language
4.1.2 Forward rules: FROM rules
SYNTAX
[whenever TR-I , TR-2, . . .] from B infer A
[ w h e n e v e r TR-I , TR-2 , . , ,I from B infer cases CASE-l ; CASE-2 ; . . I e n d
A: (the
B: (the
TR-i: a
CASE-I:
INFER clause) a conjunction of literals.
FROM clause) a conjunction of iiterals.
trigger-expression.
a CASE (see below).
If there is a WHENEVER clause, it must have at least one trigger. A CASE must be one of the
following two forms:
C+D
or
C
where C and D are conjunctions of literals. In the second case, D is defaulted to be T R U E .
There must be at least one case in a CASES clause.
LOGICAL MEANING
B 3 [(C-l
A
D-l) v (C-2
A
D-2) v . . . 1
SEMANTICS
When all of the WHENEVER triggers have been instantiated (there may be none), and when all
of the literals in the FROM clause have become true, the INFER clause is asserted. If the INFER
clause is a conjunction of iiterals, they are all asserted. If the INFER clause is a CASES construct,
a case split is required. The actual split is delayed as long as possible (since a split is potentially
expensive) but is done before any backward rules are applied, A case of the split may be
eliminated during proof (but before the split is actually done) when Its C-l formula (the formula6
to the left of the arrow) becomes false. If all but one of the cases are eliminated, no split is done;
instead the remaining case is asserted immediately.
EXAMPLES
f r o m P(S) i n f e r 4NX,Y,Sl
% W h e n P(S) ie t r u e , Q(X,Y,Sl i s false, f o r a l l X a n d Y %
w h e n e v e r A*B f r o m A20
A
820 i n f e r A*Bz~
w h e n e v e r X / Y f r o m Y& i n f e r X=Y*(X/Y)
w h e n e v e r MIN(l,J,Kl f r o m T R U E i n f e r
c a s e s IIJAIIK + I; J<IAJIK -) J : K~IAKIJ + K e n d
% MIN(I,J,Kl=I if IsJ and IsK . . . %
53
Part il: Chapter 4: The Rule Language
4.1.3 Forward rules: REPLACE rules
SYNTAX
replace TR [where Al by RP
replace TR [ w h e r e A 1 by cases C- I -) RP- 1 ; C-2 3 W-2 ; . . . end
A: (the WHERE clause) a conjunction of iiterals.
C-i: a conjunction of iiterals.
TR: a trigger.
RP: a replacement.
R P-i: a replacement,
Tile WHERE clause is optional. If there is no WHERE clause, A is defaulted to TRUE. If there
is a CASES clause, it must have at least one case.
LOGICALMEANING
A =) (T
R
=
R
P)
SEMANTICS
When an instance of TR appears in the data base and the WHERE clause has become true, then
do the action specified by the BY clause. If the BY clause is a replacement, then an equaIity (or
equivalence) between TR and RP is asserted. If the BY clause is a CASES clause, a split is
propagated. The two rules given in the syntax specification are equivalent to the foilowlng two
FROM rules:
whenever TR from A infer TR - R P
w h e n e v e r T R f r o m A i n f e r c a s e s C - l -) TR = RP-l ; C-2 + TR - RP-2 ; . . . end
d
EXAMPLES
replace X DIV 1 by X
% Division by 1 %
r e p l a c e A*B b y B*A
% Commutativity o f multiplication, This rule will not loop. %
r e p l a c e <A, [Il,E>IJl b y c a s e s I=J + E ;
IHJ + A[Jl e n d
% Array data structure term simplification %
r e p l a c e SIGN(X) b y c a s e s X;r8 + 1: X& + - 1 e n d
% W i l l c a u s e a s p l i t i f n e i t h e r X28 n o r X43 c a n b e s h o w n %
54
Part II: Chapter 4: The Rule Language
4.1.4 Rulef iles
SYNTAX
RULEFILE(name)
[constant CS- I, CS-2, . . , ;I
[pattern PT-I, PT-2, , , . ;]
R N - I : R U L E - I ; RN-2: RULE-2;. , .
RULE-i: a r u l e .
RN-i: an identifier which will name the rule.
CS-I: an identifier which is to be a pattern constant.
PT-x: an identifier which is to be a pattern variable.
The CONSTANT and PATTERN specifications are optional. Ail identifiers appearing in the
rulefiie are assumed to be pattern variables except those used as function or predicate names, or
as r e cor d f i el d i dent i f i er s. Thes e de fa ul ts c a n be ov e rri dde n us i ng the CONS TAN T a n d
PATTERN declarations.
SEMANTICS
A rulefiie is a collection of rules. More than one rulefiie can be active in the theorem prover at
once. Each rule and each rulefiie must have a unique name. Thus rules or rulefiles can be
replaced by reading new rules or rulefiles with identical names; old rules or rulefiles with the same
name are deleted. The order rules appear in the file Is, more or less, the order in which they will
be applied by the theorem prover.
EXAMPLE
rulef i lefsample)
c o n s t a n t N U L L , E M P T Y , CONSTl, CONSTZ:
% Declare various identifiers to be pattern constants %
CONSTt f r o m T R U E i n f e r CONST~HCONST~;
% A s s e r t t h a t CONSTltCONST2 t o t h e d a t a b a s e %
I NEQ:
i n f e r X>O f r o m X4 A X20;
% Rules like this may be required sometimes %
APNULL! r e p l a c e APPENDlNULL,XI b y X :
% NULL is a constant %
GINFO; r e p l a c e G(X) w h e r e X,INFO-EMPTY b y N U L L ;
% INFO is a record field identifier,
and therefore not a pattern variable %
55
Part II: Chapter 4: The Rule Language
4.1.5 Switches md parameters
There are various parameters and switches for controlling the proof search and tracing. Several
of these are depth bounds which allow the user to constrain the search in various ways. T h e
SHOW switches are particularly useful for debugging ruiefiies. In the default case, ail t r a c e
switches are off. The SHOW command (see Section 2.3) can be used to determine the default
settings of the depth bounds.
D E P T H T A L K ( s w i t c h ) -- If this switch is set to true, the prover will print a message whenever it
reaches a depth bound during search.
P R O O F D E P T H ( i n t e g e r ) - - This value is approximately the maximum depth of nesting of
backward rules,
A S S E R T D E P T H ( i n t e g e r ) - - This value is approximately the maximum depth of nesting of
assertions made by forward rules.
C A S E D E P T H ( i n t e g e r ) -- Approximately, the maximum number of forward case splits which
will be allowed. Ail others will be ignored. T h i s v a l u e d o e s n o t lnciude splits which are
eliminated due to case r<duction.
T R A C E ( s w i t c h ) -- If this switch is set, a proof summary will be printed after simplification of a
verification condition.
‘ T R A C E F A C T ( s w i t c h ) -- If TRACE and TRACEFACT are both set, the proof summary wjii
include a listing of facts asserted by forward rules.
TR A CEVC (switch) -- An Intermediate version (“presimpiified”) of the theorem to be proved will
be printed. This version is the result of simplifying the formula In the presence of no rules. This
output Is useful for interpreting the TRACE results.
SUMMATCH (switch) -- If this switch is set, additional specific instances will be generated
during matching of sums. The use of this switch is described in Section 4.2.13.
SHOWFACT (switch) -- This switch will cause the prover to display facts asserted by forward
rules during simplification. Some of these facts may be asserted in inconsistent contexts, and may
be false.
S H O W G O A L ( s w i t c h ) -- The theorem prover will display subgoals (from backward rules)
generated during a proof if this switch is set. This feature is useful during development of
rulefiles and assertions in programs. Some successful subgoals will not be displayed, because they
are proved by TEST (see Section 4.2.1).
SHOWTEST (switch) - - T h e t h e o r e m p r o v e r w i l l s h o w a i l i n s t a n t i a t e d iiterals which a r e
TESTed during proof if this switch is set (see Section 42.7).
56
Part II: Chapter 4: Tile Rule Language
4.1.6 Au exawpie
Here is a sample rulefile and two proofs which make use of it. The ruiefile is not particutariy
efficient, though it does demonstrate severai features of the rule language. The verification
conditions come from an insertion sort program. T h e T R A C E , T R A C E F A C T , a n d T R A C E V C
switches have been set. It took three seconds to prove INSERTSORT 2, and seven seconds t o
p r o v e I N S E R T S O R T 3 . I f o n l y t h e r u l e s O R D 3 a n d ORD9 a r e i n c l u d e d , p r o o f o f
INSERTSORT 3 takes only two seconds.
RULEFILE(INSERT)
% R u l e f i le f o r i n s e r t i o n s o r t %
PERMl:
PERMZ:
PERtl3 :
I N F E R Permutation(J,J);
I N F E R Permutation(Exchange(A,I,J),B) F R O M Permutation(A,B);
R E P L A C E c<Pl, [PZI ,Pl [P31>, [P3l,P4> 8Y Exchanget<Pi, [PZI ,P4>,PZ,P3);
DATA1 :
DATAZ:
R E P L A C E < A , (JI ,X> [Kl W H E R E K=J BY X;
REPLACE <A, EJ3 ,A CJI > BY A;
ORDl:
INFER
O r d e r e d (K, I, J) FROM J zJ:
Ordered(K, I, J) F R O M Ordered(K, J ,L) A Ordered(K,L, J):
Ordered(K, J,J) F R O M Ordered(K,L,MI A L<i A JsM:
Orderedf<K, [Jl ,E>, J,L) F R O M I - J A E<KEJ+ll A Ordered(K, J+l,L);
F R O M l<J A J<J A Ordered(A,l,J);
Ordered(<A, IJl,A[J-ll>,l,J)
F R O M J=J A Ordered(A,l,J-1);
Ordered(<A, IJll,AEJ-lb,l,J)
Ordered(<K, [JI,E>,J,L) F R O M J = L A K[L-111E A Ordered(K,I,L-1);
Ordered(A,l,J) F R O M Ordered(A,l,I-1) A AIJIzA[J-~I;
Ordered(<K, EJl,E>,J,L) F R O M J<J A I<L A Ordered(K,J,I-1) A
Ordered(K, J+l,L) A KEJ-111E A EsKEJtll:
ORCQ:
ORD3:
ORES,:
OR05 :
CIRD6 :
OR07 :
OR08 :
ORD9 :
INFER
J NFER
INFER
INFER
J NFER
J NFER
INFER
J NFER
ARR:
J N F E R KILl<K[Ml F R O M Ordered(K,I,J)A I<L
57
A
L<M
A
MsJi
Part II: Chapter 4: The Rule Language
U n s i m p l i f i e d V e r i f i c a t i o n Conditionr I N S E R T S O R T 2
(ORDERED (K, 1, J)
JrN A
X<K [I+13 A
A
0<1 A
I<J A
PERMUTATIONkK, III ,X>,K0)
0<1-1
-P
A
MKII-13sX) A
K-Z=<K, [I-Ml ,KH-13~
-b
OROEREO(K~Z,l,J)
JIN A
X<K-2 [I -1+13 A
@<I-l
I-l<J
A
A
PERMUTATIONkK~2,
A
11-13 ,X>,K0) 1)
Presimplified Verification Condition: INSERTSORT 2
(ORDERED (K, 1, J) A
J<N A
X<K IltI1 A
0~1
n
I<J A
PERMUTATIONkK, 111 ,X>,KB)
221 A
K11-ll>X A
K-2-<K, 111 ,KH-lb
-9
A
ORDERED (K-2,1, J1 A
X<K-2 II 1 A
PERMUTATIONkK-2, H-11 ,X>,K0))
Simplified Verification Condition! INSERTSORT 2
TRUE
58
Part II: Chapter 4: The Rule Language
Proof summary for INSERTSORT 2.
Assertions made by rules;
OATAl: K~2~IJ=KII-13
P E R M 3 : <K-2, II-lI,X>=EXCHANGEt<K, tII,X>,I,I-1)
Top level goal OROEREO(K_2,1,J)
P r o o f f r o m b a c k w a r d s r u l e ORO5.
Subgoa 1 X<K-2 I I I
P r o v e d w i t h o u t b a c k w a r d s rules.
T o p l e v e l g o a l PERMUTATION(<K-2, H - 1 3 ,X>,KB)
P r o o f f r o m b a c k w a r d s r u l e PERM2.
End of proof summary for INSERTSORT 2,
Unsimplified Verification Condition! INSERTSORT 3
tOROEREO(K,l,JI
J<N A
X<K 11tll
@<I
A
A
A
A
I<J
PERMUTATIONtcK, III ,X>,KB)
0<1-1
+
(K[I-l.I<X
-b
A
(K-l=<K, [1-1+13,X>
+
OROEREOfK-l,l, (Jtl)-1)
JtlsNtl
2sJtl A
A
A
PERMUTATIONfK-i,KBI 1))
Presimplified Verification Condition! INSERTSORT 3
(ORDERED (K, 1, JI A
JIN A
X<K[ltIl
@<I
I<J
A
A
A
PERMUTATION(<K, 113 ,X>,K0)
251 A
K[I-1lsX A
K-l=<K, [II ,X>
-9
A
59
Part II: Chapter 4: The Rule Language
ORDERED (K-1,1, J) 1
Simplified Verification Condition! INSERTSORT 3
TRUE
Proof summary for INSERTSORT 3,
T o p l e v e l g o a l OROEREOtK-l,l,J)
P r o o f f r o m b a c k w a r d s r u l e OR09,
Subproof st
S u b g o a l OROERED(K,ltI,J1
P r o o f f r o m b a c k w a r d s r u l e 0R03.
S u b g o a l OROEREO(K,l,I-1)
P r o o f f r o m b a c k u a r d e r u l e ORO3.
End of proof summary for INSERTSORT 3.
4.2 Using the rule language
In this section we d e s c r i b e t e c h n i q u e s for writing rules. T h e p r i m a r y p u r p o s e o f t h e r u l e
language is to allow users of the verifier to supply lemmas to the theorem prover. By providing
the necessary rules, the user can effectively extend the assertion language to include new concepts.
For example, let Ordered(A,i,j) mean that the array A is ordered in the intervaI [i,jl. By giving
suitable rules, Ordered can be used in assertions in programs, and the theorem prover can be
expected
to prove a large variety of valid verification conditions involving Ordered.
d
Suppose we wish to express the following fact about Ordered:
(*O
(VA,i,j) (Ordered(A,it 1,j)
A
i~j
A
AWsACit i] 3 Ordered(A,i,j)).
That is, if the array A is ordered in [it l,j], and A[il is not greater than the smallest element of A
in the interval (namely, A[it I]), then A is ordered in E&j].
It would be nice if we only had to provide logical statements like (m), and proofs of valid
verification conditions were forthcoming. However, the theorem prover does not have much
60
Part II: Chapter 4: The Rule Latrguage
heuristic knowledge, and uses only the simplest methods to search for proofs. Therefore, when we
provide a logical statement to the prover, we must tell it how to make use of that fact.
We start by distinguishing the two main types of rules. Then, a short description of the theorem
proving algorithm is given. This provides the background for a more complete discussion of the
differences between the two types of rules. Following this, some details are given about the
ordering of proof search, to help the user improve the efficiency of his rules.
Pattern matching is then discussed. The matcher used in the rulehandler makes use of semantic
knowledge in certain domains.
Several sections follow which describe various specific features of the rule language. Included
among these features are rule schemata, a device for controlling application of rules through the
use of the matcher, case splitting, for doing proof by considering cases, and semantic matching.
Finally, some general advice is given on efficiency considerations.
4.2.1 Forward and backward rules
Here is one way ()(I) can be expressed to the theorem prover:
R I: INFER Ordered(A,i,j) FROM i<j
A
O r d e r e d ( A , i t I,]) A A[i~sA~it 11;
This has the effect of saying: “If you are trying to prove that A is ordered in [i,jl, for any A, 1,
and j, then first prove that i<j, then Ordered(A,it i,j), and finally, AEiJ<AIit il.”
Here is another way of expressing (*):
R 2 : F R O M O r d e r e d ( A , i t l,j)
A
i<j
A
A[i]<A[it 13 I N F E R Ordered(A,i,j);
’
That is, for any A, 1, and 3, if you know that Ordered(A,it l,j), i<J and A[i]~A[i+l] are all t r u e ,
then you can assert Ordered(A,i,j). An equivalent way of writing R2 is:
R2A: F R O M O r d e r e d ( A , i , j )
A
i<j
A
A[i-IJrAlil I N F E R Ordered(A,i-I,j);
Rules like R I are called BACKWARD rules; rules like R2 are called FORWARD rules. One
way to think about backward rules is that they work backward: setting up subgoals from goals.
, Similarly, forward rules appear to work forward from assertions, generating new assertions.
Backward rules may be compared to PLANNER consequent theorems; forward rules to
antecedent theorems. Thus, though they may have the same logical meaning, they are applied
differently in the search for a proof.
61
Part II: Chapter 4: The Ruie Language
42.2 The theorem prover
This section will provide a rough idea of how the rulehandier of the theorem prover works.
In the theorem prover, many proofs can be accomplished without rules, since decision procedures
for various theories (including equality and Presburger arithmetic) are built into the simplifier.
The built in theories are described in Part II, Chapter 3.
The prover tries to prove theorems by deriving contradictions in a data base. Thus, if we are
trying to prove AAB =) C, it asserts A a n d B, then asserts the negation of C, and finally tries to
show that this data base describes an impossible situation. For example, suppose we want to
p r o v e x=y 3 fcx)=fly). W e f i r s t a s s e r t x=y. Then we assert the negation of the conclusion:
f(x>#fly). But by the properties of equality, these assertions cannot both be true, so the theorem Is
proved.
This method may be likened to the standard “Truthtable” method for simplifying propositional
formulas, in that all possible assignments are considered for the propositional variables, “z=y” and
“flx)=f(y).” For eat h of these assignments, we must show either that the formula simplifies
propositionally to TRUE, or that semantically the given assignment is impossible; that is, it
describes a contradiction:- Thus, in the example, there were four cases to consider. Three of them
reduced to 7XUE propositionally. The fourth, assigning TRUE to x=y and FALSE to flx)=fly>
resulted in a contradiction, eliminating that case from consideration. If we could not have
eliminated this case semantically, the formula would not simplify to TRUE, because this case
represented propositionally is TRUE 3 FALSE, or FALSE. Thus, data base contexts a l w a y s
represent conjunctions of iiterals; each literal is positive or negative depending on the truth-value
assignment in the current (non-tautoiogicai) case.
4.2.3 Forward rules
Forward rules typically assert new facts to the data base as a consequence of old facts. For
e x a m p l e , t h e r u l e s F R O M BA A I N F E R D a n d F R O M D I N F E R C a r e u s e d t o p r o v e t h e
verification condition AAB 3 C in the following way: Initially, the data base is empty, and the
rules are “waiting” for instances of B and D to be asserted. First, A is asserted to the data base,
followed by B. After B is added, the first rule “fires” and waits now for an instance of A to be
asserted (literals in a FROM clause are considered from left to right). A is already in t h e
database, so the rule immediately continues and asserts an Instantiated D to the data base. The
state of the data base at this point may be represented by AABAD.
After’ D is asserted, the second rule “fires” and asserts an instantiated version of C. Finally, -C is
asserted from the verification cond.ition, and a contradiction is now evident: AABADACA-C.
Thus, AAB 3 C has been proved using the two rules.
To prove AABSAD, multiple data base contexts would be used. First a contradiction would be
derived from AABA-C; then a contradiction would be derived from AABA-D, giving the proof.
62
Part Ii: Chapter 4: The Rule Language
These two sub-proofs share a subset of the data base, AAB. That is, in both cases, we have
TRUE assigned to A and B. This means that forward ruies triggered by A or B will “fire” o n c e
only, and the results will go into the common data base.
4.2.4 Case splits
It is possible for a rule to require splitting of the data base into multiple contexts for the purpose
of considering cases. For example, the rule,
CAS: FROM A INFER CASES B; C END;
indicates that if A is true, then BvC is true. That is, it indicates a disjunction between the
elements of the CASES clause. This rule would be used to prove the data base, -BAGAA,
inconsistent in the following manner: After A is asserted, the rule “fires” and indicates that a case
split is required. Case splits are delayed as much as possible, to take advantage of sharing of
common information In the multiple contexts. When the case split is done, two cases will be
considered. To prove the theorem, a contradiction must be derived from both cases. In the first
case, B is asserted to the data base, obtaining ~BATCAAAB, w h i c h Is f a l s e . T h e o t h e r c a s e ,
-BA-CAAAC, also simplifies to FALSE, resulting in a proof.
If more than one forward CASES rule applies, requiring multiple case splitting, the cases are
nested, so the total number of cases considered will be the product of the numbers of c a s e s
propagated.
42.5 Backward rules
One way to think about a backward rule in this environment is to consider it a s t h e
contrapositive of a forward rule. T h u s , t h e b a c k w a r d r u l e I N F E R C F R O M D c o u l d b e
considered to be equivalent to FROM 4 INFER -D. Now suppose we write a backward rule
-
C l : I N F E R A F R O M BAC;
The contrapositive of BAC 3 A is -A 3 ~Bv-C. This could be written as the forward rule
C 2 : F R O M -A I N F E R C A S E S -B; 4Z E N D ;
From these two examples, it appears that all backward rules can be translated into equivalent
forward rules. Is there any difference, in fact, between forward and backward rules? There is,
and it will become apparent when we see how the system deals with more than one rule. Here are
two backward rules for Ordered:
O R D I: I N F E R Ordered(a,i,j) F R O M i<j A Ordered(a,i,j-I)
O R D 2 : iNFER Ordered(a,i,]) F R O M i<J A Ordered(a,i+ 1,j)
63
A
A
alj-1 JsaEj3;
a[iJsa[i+ I J;
Part Ii: Chapter 4: The Rule Language
Suppose we are trying to prove Ordered(B,M,N). The proof will go as follows: We try to use rule
ORD I first, since it appears first. There are three cases to consider, corresponding to the three
literals in the FROM clause of the rule. These cases are tried sequentially. If all of these cases d o
not simplify to FALSE, we abandon attempts at this rule and go on to consider the case split
required by the rule ORD2, which also has three cases.. Thus we will try at most six cases, at least
two (one from each rule).
Each of the cases we try may have subcases, generated by rules that become applicable due to the
new assertion made to the data base on that case. The process of applying backward rules and
splitting in this manner is called SUBGOALING.
While backward-style splitting is more efficient than forward-style splitting, it is not
COMPLETE, in that forward-style splitting may yield a proof in examples where backward-style
splitting would not, The reader should be able to construct an example to illustrate this.
Thus, we distinguish between forward, complete splitting and backward, incomplete splitting. In a
given data base, with forward splitting, each applicable rule multiplies the maximum number of
cases considered; with backward splitting, each applicable rule adds to the maximum number of
cases considered. Had forward complete splitting been used with ORDI and ORD2, at most 9
cases would have been considered, rather than just 6. For this reason, it is desirable to use
backward splitting (or subgoaling) whenever possible. To illustrate this: suppose there were 10
rules for Ordered similar to ORDI and ORD2, each with three cases. If they were backward
rules, we would consider at most 30 cases. Were they forward rules, we would have to consider
some 3t IO (that is, 59049) cases,
4.2.6 Ordering backward rules
In our proofs, splits are always delayed until all other assertions have been made to the data base.
A II backward rules are considered to propagate splits. This includes rules like INFER P FROM
Q, which propagates a split with one case, and rules like INFER P, which propagates a split with
no cases. The reader should be able to convince himself that the rules INFER P FROM Q and
FROM -P INFER ~Qare not equivalent for this reason: These rules are logically equivalent, but
not
a heuristically equivalent because incomplete splitting is used in the backward rule.
When more than one backward rule applies, rules are tried in the order they appear in the
rulefiie, the data base of rules. By ordering rules carefully, the user can improve the speed of his
proofs, Consider the following four rules:
N I:
N2:
N3:
N4:
infer
infer
infer
infer
N(x,y)
N(x,y)
N(x,y)
N(x,y)
from
from
from
from
P(x) A q(y);
S(x,y);
N(y,x);
N(C(x),C(y));
The “easier,” non-recursive rules appear first.
When trying to prove N(A,B), non-N subgoals
64
Part II: Chapter 4: The Rule Language
would be tried in the following order (assuming none were provable): P(A), S(A,B), P(B), S(B,A),
P(C(B)), S(C(B),C(A)), P(C(A)), S(C(A),C(B)), P(C(C(A))), a n d s o o n . q(x) i s n e v e r t r i e d , s i n c e
the P(x) case always fails.
.The rule N3 will not loop forever. W h e n P(A) and S(A,B) fail, the rule sets up the goal N(B,A).
After P(B) and S(B,A) fail (sub-subgoals from NI and N2 on this subgoal), N3 applies a g a i n ,
setting up the goal N(A,B). But “setting up a goal” means denying a fact to the data base. Since
-N(A,B) already exists in the data base, denying N(A,B) again produces no effect, so no new rules
apply and the next subgoal, from N4, will be considered: N(C(B),C(A)). infinite looping could
arise from N4, however, unless there is a rule which expresses C(x)=x. In general, it may be
extremely difficult, if not impossible to write non-recursive rules for certain concepts. For this
reason, there are “depth-bounds,, or cut-offs built into the rule mechanism to limit search,
Suppose the N rules had been ordered: N4, NI, N2, N3. Because we use a depth-first search
paradigm, the rule N4 would be applied recursively until the depth bound was reached before
any other subgoals were generated! Thus, if the depth bound were three, the first subgoal would
be P(C(C(A)))
In fact, strict depth-first search is not used; the rulehandler uses a combination breadth-first
depth-first search: All subgoals at a level are generated. If any of them can be proved without
further backward rules, they will not be set up as subgoals. Thus, even with the bad order of
rules, there would be no search in the proof of P(A)AQ~A) 3 N(A,B).
Within a given rule, subgoals are tried in the order they appear in the FROM part of the rule.
Thus, “easier” literals should appear first, since, if their proofs failed, further cases which may
involve more extensive searching will not be tried. Considerations such as these would help the
user decide how to order the subgoals in the rule Ni.
4.2.7 Introduction to matching
Logically, rules are universally quantified statements, with quantification over all variables which
appear. Thus, the rule
M I : F R O M P(x)~Qjx) I N F E R R ( x ) ;
represents the logical statement Vx[P(x)~@x) 3 R(x)J.
.
When a rule “fires,” the effect internally is to make a copy of the rule with “constrained”
quantification. For example, suppose we are trying to prove
P(A) A qjB) A QC) A A=B 3 R(B).
The first literal asserted to the data base is P(A). At this point, MI fires, and waits for qSA) to
be asserted. One way of viewing this is that a new rule,
65
Part Ii: Chapter 4: The Rule Language
M I A : F R O M aA) I N F E R R ( A ) ;
has been added to the system, and that to avoid duplication, MI has now been constrained to fire
with x distinct from A in this context. QJA) is fully instantiated; in resolution terminology, it is a
ground literal. This means we can TEST its validity directly, rather than merely waiting for
“instances.” Thus, if we had a forward rule
M2: F R O M T R U E I N F E R ax);
this rule would apply during the test of Q(A), and MIA would assert R(A). Had the literals in
M I’s FROM clause been reversed, use of M2 would not have been possible since rules only apply
to literals which appear in the data base (and thus are ground).
However, there is no rule M2 in our example, so testing Q(A) fails, and the rule M IA continues
to wait. The next literal asserted to the data base from the theorem is Q(B). This does not fire
any rules. P(C) is the next literal asserted. At this point MI fires again, since C is distinct from
A, and another virtual instance rule is created,
M IB: F R O M Q&) I N F E R R ( C ) ;
The data base is P(A)AQSB)AP(C). A=B is now asserted. At this point, the rule M IA fires, since
Q$B)=qSA) by the (built in) theory of equality, and R(A) is asserted. The data base is now
P(A) A qjB) A P(C) A A=B A R(A).
Rule M 1 is waiting for instances of P(x) where x is distinct from A,B, or C. Rule M IB is waiting
for QJC) to become true. Rule MIA has already fired for all of its possible instances (only one).
Finally, the denial of the conclusion of the theorem is asserted, -R(B). Since R(A) and A=B a r e
both in the data base, a contradiction is indicated. Thus, we have proved the theorem using the
rule M I.
We make several observations about this proof. Forward rules without CASES are always
“waiting” on some literal pattern. If this literal pattern is not fully instantiated (for example, P(x)
iJ.1 M I), the prover will wait for instances to appear in the data base. On the other hand, if the
literal is fully instantiated (for example Q(A) in MIA), the prover not only waits for the literal to
a p pea r, it also “tests” the literal for validity in the data base. This means that in each distinct
context in the data base, the literal will be denied in an effort to obtain a contradiction. During
the test of the literal, forward rules may be applied, resulting in proof of the literal in the given
data base.
4.2.8 Ordering within rules
S u p p o s e w e w a n t t o p r o v e A >O A P ( A + I) 2 Q(A+ l), and we know (Vx)[x>O
are two ways we could write forward rules to express this fact:
66
A
p(x) 3 q(x)]. T h e r e
0
Part II: Chapter 4: The Rule Language
A R 1 : F R O M x>O
AR2 F R O M P ( x )
A
A
P(x) I N F E R Qjx);
x>O I N F E R Qjx);
Consider using AR I. When A>0 is asserted, AR I fires, and creates a virtual instantiated rule,
A R I A : F R O M P ( A ) I N F E R Q(A);
in the data base, since x was bound to A when ARI fired. With this rule, we cannot prove the
theorem. Suppose we are using A R2 instead. After P(A+ I) is asserted, the rule instantiates to
AR2A: F R O M A+i>O I N F E R QjA+i);
T e s t i n g A + I>0 s u c c e e d s , s i n c e A>0 is in the data base, and thus is known to the built in
Presburger arithmetic prover. Therefore, qSA+ I) is asserted, and the theorem is proved. This
illustrates the fact that the order in which iiterals appear in a rule affects the ability of the system
to obtain a proof.
This ordering constraint also holds for backward rules because cases are considered in the order
they appear in the rule. Suppose we had the rules
O R D 3 : I N F E R O r d e r e d ( a , x , y ) F R O M x<y A Ordered(a,x,t)
O R D 4 : I N F E R O r d e r e d ( a , x , y ) F R O M xcy A Ordered(a,z,y)
A
A
Ordered(a,z,y)
Ordered(a,x,t)
C o n s i d e r u s i n g O R D 3 t o p r o v e , s a y , Ordered(B,I,J). The first subgoal is 1x3, which is fully
instantiated, and thus will be tested in the data base, and may require further backward rules for
proof. If it is provable, then the rule waits for some z such that Ordered(B,I,t) exists in the data
base, If it finds an instance, say where t=K, it sets up the further subgoal Ordered(B,K,J), which
is fully instantiated and thus may use further backward rules for proof. Thus, Ordered(B,I,K)
must actually appear in the data base, in order to provide an instance for z, while Ordered(B,K,J)
need only be derivable from rules. Had we used ORD4, the situation would have been reversed.
Thus, the two rules are not equivalent, and both may be required for some proofs.
This ordering constraint should not be viewed as a weakness of the rulehandier, since by giving
all permutations, it could be circumvented. Indeed, it provides the user with a way of controlling
proof search since he can predict which literals will be uninstantiated.
4.2.9 Rule schemata: Whenever alld Replace
Suppose we desired to assert x*yzO whenever we saw a product, x*y and it was evident that x20
a n d yr0. W e could w r i t e
MULI: F R O M xr0 A yr0 I N F E R x*yrO;
Consider the effect of this rule. Whenever an assertion is made in the data base of the form EzO
61
Part II: Chapter 4: The Rule Language
for any expression E, both iiterals in the FROM clause will match. Thus, for every pair E and F
where both ErO and FrO (possibly E=F, of course), the rule will fire, asserting E*FrO. This adds a
new inequality assertion to the data base, and so the rule will match many times more. In the end,
many useless facts will get asserted and much prover time will be wasted, since the rule matches
Indiscriminately.
We can remedy this by using a device called a RULE SCHEMA, which allows us to give a
“trigger pattern.” The rule
M U L 2 : W H E N E V E R x*y F R O M x10 A yr0 I N F E R x*yzO;
says that whenever a product, A*B, appears in the data base, an instantiated version of MUL2
will appear:
MUL2A: F R O M A>0 A BzO I N F E R AmBrO;
Here, all literals are instantiated, so the validity of the FROM iiterals can be tested. Further, the
rule applies only to products which actually appear in the data base. T h u s , adding the
WHENEVER clause weakens the rule by restricting its application so it makes assertions only
about products which appear in the data base. However, the WHENEVER clause also
strengthens the rule by causing the FROM literals to be fully instantiated, and thus subject to
testing in the data base. That is, the WHENEVER rule, MUL2 would p r o v e
ArO A B>,O 2 (Ati)*BzO
while MULI would not. While they have different heuristic meanings, logically, MUL2 a n d
MULI express the same fact.
One v&y common application of WHENEVER is asserting equalities between terms, For
example,
GCDI: W H E N E V E R GCD(x,y) F R O M x M O D y - 0 I N F E R GCD(x,y)=y;
Another way of writing this rule is
G C D 2 : R E P L A C E GCD(x,y) W H E R E x M O D y - 0 BY y;
This rule is semantically equivalent to GCDI. The “REPLACE” syntax is used for historical
reasons; in fact, there is no actual rewriting or replacement -- an equality is asserted. Thus,
REPLACE rules may be viewed as statements of directional equalities.
Because of the structure of the data base, rules like
T W I S T : R E P L A C E F(x,y) B Y F(y,x);
will cause no looping. Similarly, replacement rules can be provided for both directions of a n
equality:
68
Part II: Chapter 4: The Rule Language
A S C I : R E P L A C E F(x,F(y,z)) BY F(F(x,y),z);
ASC2: R E P L A C E F(F(x,y),z) B Y F(x,F(y,z));
WHENEVER clauses may include more than one trigger pattern. Ail triggers must match before
the instantiated rule will appear. Triggers are expressions which contain no propositional
operators and are not individual variables.
4.2.10 Levels of proof
Thus far, we have seen that there are two levels of interaction between instantiated iiterals in
rules and the data base. A literal in a rule is a FINAL literal if it occurs in the FROM clause of
a backward rule or in the INFER clause of a forward rule, Final iiterals are those iiterais which,
when instantiated, can get asserted “permanently” in a data base context, which may be the
branch of a split. Since these iiterals become part of the data base, they can cause other rules to
be applied, and further splits to be generated. Thus they have the same status as literals which
actually occur in the theorem to be proved.
Literals which are not final are called TRANSITION literals. In general, the prover waits for
transition literals to become true before “firing” a rule. When the rulehandler is attempting to
establish validity of an instantiated transition literal, it will test that literal in the data base at
various times. During testing, forward rules which don’t split may be applied, as well as
knowledge from the built in theories. Presently, there is also the restriction that when a transition
literal is being tested, nested tests will not be done; that is, they will fail. Thus, the following rules
will not work together as expected:
TR I: FROM P(x) A QIF(x)) I N F E R R ( x ) ;
TR2: REPLACE F(x) WHERE S(x) BY G(x);
The prover uses a process called FIND to locate instantiations for uninstantiated literals. In
general, t h I‘s means that a literal must be found in the data base which matches the pattern literal
in the rule. In the case of equalities, the process is slightly more powerful. If both sides of the
pattern equality are uninstantiated, an actual matching equality must be found in the data base.
Otherwise, when only one side of the equality is uninstantiated, the prover will wait for an
instance of this side of the equality to become equivalent to the value in the data base
corresponding to the instantiated side of the equality pattern.
All uninstantiated literals are proved with FIND. Thus, if ATOM(A) is asserted,
A T O M : F R O M A T O M ( x ) I N F E R xzCONS(y,z);
will cause the prover to wait for an instance of CONS(y,z) to become equivalent to A. If such a n
instance appears, a contradiction will be propagated.
Uninstantiated iiterals should, of course, not be single pattern variables.
69
Part ii: Chapter 4: The Rule Language
4.2.1 I Forward cases
In order to increase efficiency of proofs, a case elimination mechanism has been built into the
forward CASES construct. Let <A,EIJ,E> represent the array A after the assignment AIIJtE has
._
been performed. Thus, we have
<a,Cil,e>[iJ=e and izjxa,liJ,e>EjJ=a[jJ.
This fact can be written as a REPLACE rule
A R R A Y : R E P L A C E <a,Eil,er[jJ B Y C A S E S i=J + e; it] -+ aCj3 E N D ;
This rule is equivalent to
A R R A Y I : W H E N E V E R <a,[il,e>[jJ F R O M T R U E I N F E R C A S E S
i=j + ca,[iJ,e>[jJ=e;
izj -+ <a,EiJ,e>[jJ=a[jJ E N D ;
Interpret the “arrow” in the CASES clause as AND. Suppose we wish to prove
The rule splits and considers two cases
4dl,AEIl~EJJ+A~JJ A I-J A <A,[Il,A~IJ>IJl=AEIJ
<A,~IJ,A~IJ~EJkA~JJ A I#J A <A,EIJ,A~IJ>~Jl=AEJJ
Both cases simplify to FALSE, proving the theorem. In this example, the case split is required
for proof.
Suppose, however, we were proving
<<B,[ I J,2>,[23,3>[ IJ=2.
If splits were done, four cases would be considered, three of which would be eliminated trivially.
To avoid unnecessary splitting, and unnecessary delay of assertions of facts from forward rules,
cases can be eliminated dynamically once a split has been propagated. As soon as only one case
remains, its facts are asserted immediately. In our example, the rule ARRAY first applies with
a=<B,[l J,!b, 14, e=3, j= I. The first case, with i-j or 24, is eliminated by test as soon as the rule
applies, causing the other branch of the split to be propagated as fact. Thus the data base
becomes,
<<B,[ 1 J,2>,[2J,3>1 I J22 A 22 I A <<B,[ I J,2>,[2J,3>[ I J=<B,[ i ],2>[ i J.
At this point, the rule applies again, with a=B, 14, e=2, j-i. The second case is eliminated by
test, and the fact <B,[ I J,2>[ I J=2 is propagated causing an immediate contradiction.
70
Part II: Chapter 4: The Rule Latrguage
T h IJS, forward CASES generally cause splitting only when a split is necessary or further* splits are
r-i uired to eliminate cases. Forward splits will not occur, however, within the proof of a subgoal
f o r a backwards rule, though case elimination m lay cause facts to be asserted.
For efficiency reasons, only literals appearing before the arrow in a given case are used to
eliminate other cases. Thus, the rule
C A S : F R O M P I N F E R C A S E S Q i -+ RI; Q2 -+ R2; Q3 -+ R 3 E N D ;
is equivalent to the set of rules
CAS I: FROM P A -Q2 A 9Q3 INFER Ql A R I ;
C A S 2 : F R O M P A -Qi A -Q3 INFER Q2 A R 2 ;
C A S 3 : F R O M P A -Ql A -Q2 INFER Q3 A R 3 ;
a s s u m i n g it never splits. If any of the Q or Ri are not fully instantiated when the split is
propagated, further instantiations will occur only within each case, not across cases. The following
Iwo rules are equivalent:
C S I : F R O M P ( x ) I N F E R C A S E S Qi(x,y); Q?(x,y) E N D ;
C S 2 : F R O M P ( x ) I N F E R C A S E S Qi(x,y); Q~(x,z) E N D ;
4,2.12 Semantic matcititig
Suppose we had a rule
S M I: I N F E R P(xt I) F R O M P ( x ) A Q(x);
If we wanted this rule to apply in proving P(2tA) from P(At I) and QjItA), the pattern matcher
would need to have some knowledge of properties of addition. We call this type of matching
Semantic Matching. The matcher used in the rulehandler makes use of properties of addition,
multiplication, arithmetic relations, and equality. T h e m a t c h e r assumes t h a t a l l v a r i a b l e s
appearing in sums and products are integer valued. This is conservative in the sense that no
additional matches are obtained by the assumption, while many are eliminated.
.
Properties of addition and multiplication used are commutativity, associativity, identity, and in the
case of addition, multiplication by constants. In the case of the relational operators, the integer
a s s u m p t i o n m a k e s XrO and Xt 1~0 equivalent. In fact, the prover stores all inequalities of a
given sign internally in the form EzO for some expression E. This means that the pattern Fry
w i l l m a t c h A+B<F(C)tG(D), binding x to C and y to AtB-G(D)ti. Note that only a negated
inequality pattern will match a negated inequality in the data base, however.
Equality matching makes use of the symmetric and substitutive properties of equality. T h u s , the
rule
7i
3
Part II: Chapter 4: The Rule Lallguage
EQI: I N F E R x=y F R O M P(x,y);
will prove P&A) 2 A =B.
Often, patterns will not match as soon as the target is. found because facts asserted later in proof
are required for the match. For example, in proving P(A) A A=F(B) =) QJB) with the rule
tl: F R O M P(F(x)) I N F E R Q(x);
the rule applies only after A--F(B) has been asserted to the data base. For efficiency reasons, this
sort of “waiting” does NOT take place with semantic patterns. Thus, P(A*B) A A=F(C) 3 QjB,C)
will not be proved by
QZ: F R O M P(x*F(y)) I N F E R qx,y);
while A=F(C) A P(A*B) 3 OJB,C) will. This limitation is not a serious one in practice, and may
be circumvented by using a WHENEVER clause, as in
93: W H E N E --V E R F ( y ) F R O M xtF(y) I N F E R qjx,y);
4.2.13 Subspace nlatchi~lg
When matching a pattern like xty against a sum, it is possible that many distinct matches will
result. For this reason, certain sum matches produce “subspace” specifications as their result. For
example, m a t c h i n g x+y a g a i n s t AtBtC p r o d u c e s t h e s p e c i f i c a t i o n xty==(AtBtC), w h i c h
represents a linear equation with variables x and y When x or y appear in further patterns, they
will be considered to be unbound, except subject to the constraint of this equation. Multiple
constraints are merged using Gaussian Elimination over the integers. T h u s P(xtr, x-y) will
m a t c h P(A,A-4*B), b i n d i n g x to A-2*B a n d y to 2*B. P(xty,x-y) a n d P(A,A-3*(B) w i l t n o t
match, however, because x and y are considered to be integer variables.
Subspace matching is a powerful facility, but it is not desirable in certain instances. Consider the
rule
DIST: R E P L A C E (atb)*c B Y a*c t b*c;
Since a and b will be part of a subspace specification, the BY clause will not be instantiated,
severely limitrng applicability of the rule. For this reason, a facility has been provided which
allow; extra specrflc i n s t a n c e s t o b e g e n e r a t e d b y t h e m a t c h e r i n a d d i t i o n t o t h e subspace
specifications. This facility is controllable by a switch (called SUMMATCH), since for efficiency
reasons, it may not always be desirable.
In some cases, it may be necessary to eliminate the subspace match entirely. If we were simplifying
P(A)
A
P(3)
A
P(B)
A
P(c) 3 P ( C t B )
72
a
Part II: Chapter 4: The Rule Language
with the rule
S U M P : I N F E R P(x+y) F R O M P ( x )
A
P(y);
many unnecessary subgoals would be generated. When the rule matches, it generates a subspace
specification for x+y==(CtB) in its virtual instance. FIND is used to locate instances of P(x), since
x is not fully specified. The first instance is P(A), resulting in the binding of x to A and y to
C+B-A by solving through. By this process, many useiess goals will be generated. If we c o u l d
somehow guarantee that P(x) would be instantiated, we would not have this problem. One way t o
do this is to invent a new predicate which does not appear in t h e t h e o r e m s t o b e p r o v e d .
Suppose we replaced SUMP by
S U M P 2 : I N F E R P(x+y) FROM INST(x)
S U M A U X : I N F E R INST(x);
A
P(x)
A
P(y);
Since lNST does not appear in the data base, it can only be proved with rules. But rules only
“fire” on Instantiated literals, so FIND will always fail on INST, eliminating the subspace matches.
Thus, only the specific instances (provided as a result of setting the switch mentioned above) will
be considered. This combination of rules guarantees that P(x) (and consequently P(y)) in SUMP2
will be instantiated.
4,2.14 Efficiency considerat ions
The user Is reminded that the theorem prover is limited in its capacity. Rules may be thought of
as a device for programming the theorem prover: it is easy to write inefficient programs -- harder
to write efficient ones. Like programs, inefficient rulefiles cause the .prover to use excessive time
or space, running until either the patience of the programmer or core storage is exhausted. This
sort of inefficiency can be prevented In many cases by merely considering efficiency as well as
logical elegance when writing rulefiles. Remember, however, that there are many concepts that are
difficult to code effectively as rules.
Beware of excess searching caused by badly ordered backward rules. When writing rulefiles,
consider how to order the rules so search will be efficient. Simply reordering rules and literals
within rules can lead to dramatic decreases in proof times.
Beware of forward rules asserting multitudes of useless facts and causing unnecessary splits.
Strengthen FROM clauses to restrict application,
Beware of rules that create numerous virtual instances. For example,
L O S S : W H E N E V E R F ( x ) , F ( y ) F R O M F(x)=F(y) I N F E R P(x,y);
wilt create nt2 instances of the rule if there are n instances of F(-) in the data base. While most
of the virtual instances may not fire, their presence in the data base will increase the s p a c e
required for proof.
73
Part II: Chapter 4: The Ruie Language
Plan carefully whether to use forward or backward rules, or both, to express a particular concept.
Forward rules are most effective for “complete” domains, where all relevant facts can be
propagated immediately. Examples of such domains are simple data structures, type properties of
program data objects, and some simple arithmetic facts. Backward rules are best suited to larger
“incomplete” concepts, where forward inference would produce too many facts or could not
generate all relevant facts. Ordered and Permutation are examples of such concepts.
Ad just the depth bounds to conservative values before attempting a large proof. Some domains
with very broad search spaces need shallow bounds, while other domains which require narrow,
deep searching need to have the bounds set accordingly. Rules which require broad deep
searches will be inefficient; it may be advisable to rethink their structure.
In general, the best advice is to understand what a set of rules means from both the heuristic and
logical viewpoints. Syntactically translating logical statements into rules without regard to
efficiency can lead to prolonged and wasteful searches.
4.2.15 A note on nlultiplication
The built in Presburger arithmetic package (which is independent of the rulehandler and
semantic matcher) includes a facility for recognizing multiplication by constants. However, this
facility is equivalent to the set of rules:
REPLACE
REPLACE
REPLACE
REPLACE
-1*x B Y -x
0*x B Y 0
1*x B Y x
2*x B Y x+x
a n d so on. This m e a n s t h a t w i t h o u t r u l e s , t h e f o r m u l a P(xuy) A x=0 3 P(0) will not simplify,
w h i l e t h e f o r m u l a x=0 A P(x*y) 3 P(0) will simplify. This unfortunate weakness can often be
circumvented partially by adding rules of the sort:
a
R E P L A C E x*y W H E R E x=1 B Y y
R E P L A C E x*y W H E R E x=2 B Y xlccy
and so on, where necessary.
74
REFERENCES
C II
A.V. A ho, j.D. Ullman, T h e T h e o r y o f P a r s i n g , T r a n s l a t i o n , a n d C o m p i l i n g , Volt I,
Pren lice-H all, Inc., Englewood Cliffs, N. J., 1972.
c21
W.W. Biedsoe, Splitting and reduction heuristics in automatic theorem proving, Artificial
Intelligence, Vol. 2, 1971, 55-77.
[31
R. Cartwright, and DC Oppen, Unrestricted procedure calls in Hoare’s logic, Proceedings
of the Fifth ACM Symposium on Principles of Programming Languages, ACM, New York,
1978.
[4] S . A . C o o k , A xiomatic and interpretive semantics for an Algol fragment, Technical Report
79, University of Toronto, 1975.
I51
R.L. Drysdale,and H.J. Larsen, A standard basis for automatic verification of sorting
algorithms, forthcoming AI Memo, Stanford Artificial Intelligence Laboratory, Stanford
University,
[6J
D.A. Fisher, Copying cyclic list structures in linear time using bounded workspace, CACM,
Vol. 18, 5, May 1975, 251-252.
[73 R . W . F l o y d , A ssigning meanings to programs, Proc. Symp. Appl. Math. Amer. Math. Sot.,
V o l . 19, 1 9 6 7 , 19-32.
181
S.M. German, Automating proofs of the absence of common runtime errors, Proceedings of
the Fifth ACM Symposium on Principles of Programming Languages, ACM, New York,
19’78, 105-l 18.
191
S.M. German, D.C. Luckham, and D.C. Oppen, Proving the absence of common runtime
errors, forthcoming A I Memo, Stanford Artificial Intelligence Laboratory, Stanford
University,
[ IO3
F.W. v.Henke, and D.C. Luckham, A methodology for verifying programs, Proceedings of
the International Conference on Reliable Software, Los Angeles, California, April 20-24,
1975, 156-164.
[ I 11 CA .R. Hoare, An axiomatic basis for computer programming, CACM, Vol. 12, 10, Oct.
1969, 576-580, 583.
El23
C.A.R, Hoare, Proof of a program: FIND, CACM, Vol. 14, I, Jan, 1971, 39-45.
[I31 C.A.R. Hoare, a n d N . W i r t h , A n a x i o m a t i c d e f i n i t i o n o f t h e p r o g r a m m i n g l a n g u a g e
PASCA L, Acta Informatica, Vol. 2, 1973, 335-355.
1141 S. lgarashi, R.L. London, and DC. Luckham, A u t o m a t i c p r o g r a m v e r i f i c a t i o n I : L o g i c a l
basis and its implementation, Acta informatica, Vol. 4, 1975, 145-182.
75
References
[I 51 K. Jensen, and N. Wirth, Pascal User Manual and Report, second ed., Springer-Veriag,
New York, 1975.
[I61
R.A. Karp, and D.C. Luckham, Verification of fairness in an implementation of monitors,
Proceedings International Conference on Software Engineering, San Francisco, Oct. 1976,
40-46.
[I 71 J. King, and R.W. Floyd, Interpretation oriented theorem prover over integers, Second
ACM Symposium on Theory of Comp., Massachusetts, 1970.
[ I81
D.E, Knuth, The art of computer programming, Vol. III - Sorting and Searching, AddisonWesley Publishing Company, Reading, Mass. 1973.
[I91 DC Luckham, and N. Suzuki, Automatic program verification IV: Proof of termination
w i t h i n a w e a k l o g i c o f p r o g r a m s , A I M e m o AiM-269, Stanford Artificial Intelligence
Laboratory, Stanford University, Oct. 1975; also, Acta Informatica, 8, 1977, 21-36.
[203 DC. Luckham, and N. Suzuki, Automatic program verification V: Verification-oriented
p r o o f r u l e s f o r arrays, records, and pointers, AI Memo AIM-278, Stanford Artificial
Intelligence Laboratory, Stanford University, March 1976; revised: “Verification of array,
record, and pointer operations in Pascal”, Dec. 1978.
1211
2. Manna, Mathematical Theory of Computation, McGraw-Hill Book Company, New York,
. N.Y., 1974.
1221 C.G. Nelson, and DC. Oppen, Fast decision procedures based on congruence closure, AI
Memo A IM-309, Stanford A rtificiai Intelligence Laboratory, Stanford University, Feb. 1978;
also, Proceedings of the 18th Annual IEEE Symposium on Foundations of Computer
Science, 1977.
E231
C.C. Nelson, and D.C. Oppen, Simplification by cooperating decision procedures, AI Memo
AIM-31 I, Stanford Artificial Intelligence Project, Stanford University, April 1978; also,
Proceedings of the Fifth ACM Symposium on Principles of Programming Languages,
ACM, New York, 1978.
[241
D.C. Oppen, Reasoning about recursively defined data structures, Proceedings of the Fifth
ACM Symposium on Principles of Programming Languages, ACM, New York, 1978.
1251 W. Poiak, Verification of the in-situ permutation program, forthcoming IEEE Software
. Engineering, July 1979.
1261 N. Suzuki, Verifying programs by algebraic and logical reduction, Proceedings of Int’l.
Conf. on Reliable Software, IEEE, Oct. 1975, 473-481.
1273
N. Suzuki, Automatic verification of programs with complex data structures, Ph.D Thesis,
Computer Sci. Dept., Stanford University, 1976.
76
Appendix A
Command Sylltax
A l t e r n a t e liotatioli
assignment
greater or equal
implication sign
ot
negation
history sequence concatenation
t or :=
2 or 0
+ or ->
v or ! or 1
- or N
a or !! or 11
A.1 Command syrltax
<command>
I LISP <imperative-command>
<read-command><print-command>
csimp-command>
<load-command>
<dump-command>
<delete-command>
csetparm-command>
<alias-command>----,
<set-command>
<reset-command>
<open-command>
<information-command>
s or
less or equal
not equal
+ or
and
A or
reference class extension u or
reference class selection = or
0
0
$2
&&
[\ , = or \I
Appendix A
Command Syntax
<read-command>
__
<pr i n t-command>
- PRINTVC
*<to-file-name>
cswi tches> 3L+ tvc-epec> -T
es i mp-command>
SIMPLIFY
WC to-f i I e-name>
RESIMPLIFY rL <SW i tchew rL WC-spec> f
< I oad-command>
-_
L O A D +<shor t-f i 1 e-name>4
LOADVC -<f i lepame> -T
LOADRULE -T
<dump-command>
DUMP -<short-f i I e-name>
l
t
DUMPVC -<f i (e-name>
, 3<vc_9pec> f
-t OUMPRULE -<file-name>
, +<rule-f i le-name> f
<de I ete-command,
I OELRULE -
I
<ru I e-name>
*
4
A-2
Appendix A
<alias-command>
- ALIAS
beidentifier>
<8e t-command>
- SET -wpar-ee t t i ngs>-+
wese t-command>
I_) RESET -<par-name>
t
I
’
<open-command>
- DPENFILE +<f i le-name>+
A-3
Command Syntax
Apperldix A
Command Syntax
<to-file-name>
b
b TO +tcomplete-f i le-spec> f
- COPY rL 3 -T
<f i le-name>
L
,
~complete~file~spec~ 3
<short-f i le-name>
L
<identifier> f
ccomp I e te-f i I e-speo is the standard monitor syntax for a file name.
<vc-speo
-<identifier>
<r-u I e-name>, <ru I e-f i I e-name>
-<identifier>+
<switches>
-
- ( *<par-settings>+ 1
3
<par-set t i rigs>
*r.‘.....eTIylq+
< p a r name>,
<par-va I ue> refer to the list of System Parameters given in Part II, Section 2.2.
A-i
Appendix A
Verifier Syiitax
A.2.1 Outer level of input
<source input>
l r =+
<Pascal program> f
<rut es>
<rules>
- RULEFILE I--) ( *<identifier>4 )
1 r +<rul9-dec’Tf 1 T wrub8tmt-j-t
<ru I e-deo
<rule-9tmt>
L-tforwardstatement>-
I
<rule-label>
-<ident i f ier>M I 3
<Pasea 1 p r o g r a m >
*
- PASCAL
cdeclarat ions>
<main block> f
A-5
l
Appendix A
Verifier Syntax
A.2.2 Statements that appear in rulefiies
<backwardstatement>
-*
- I N F E R --+<r-conjunct ion>
tr-fromJar t>
<r-whenever-part> f
<replacestatement>
- REPLACE -+<r-re 1 at i ona I >
F BY *cr,case-exp>*
cr-whereJar t> f
<forwardstatement>
<r-whenever-part>
- INFER -+<r-case-exp>-+
<r-f ram-par t >
- FROM -+<r-express i on>-+
<r-whenever-part>
- WHENEVER I_)
T <r-exp;e;s i on>rr
<r-where-part>
A-6
Verifier Sylitax
Appendix A
A.2.3 Expressions that appear ilr rulefiles
<r-case-exp>
w - e x p r e s s ion>
P
-cr-diejunction>
+ -*<r-disjunction> -T
<r-disjunction>
+
- < r - c o n j u n c t ion>
v -w--conjunction>
f
-f
< r - c o n j u n c t ion>
---*cr-not-expression>
+ fi -wSnotwexpre99ion++
’
<r-not-expression>
_
f-w-Jelat
ional>+
et--relational>
+
---*~r~simpIe~expre99ion~
<r-relop>--, ~r~simple~expres9ion~ -T
A-7
Appendix A
w-r-8 I op>
--fxJ”-“‘““<’
<r-term>
b
-<r-f ac tot->
t
<r-mu I op>+<r-f ac tar>
f
<r-factor>
( +<r-expression>+
a
1
I-+
k<r-var i ab 1 e>-
A-0
Vet-if ier Syntax
3
Apperldix A
Verifier Syntax
<r-variable>
<r-histexp>
<r-data-triple>
U -+<identifier> 3L cr-modfnb f
<r-modfn>
-. --+<identifier>+ ( -wr-exl igt>+ ) -P
<r-histexp>
<r-exl ist>
<r-data-tr ipIe>
- < --*<r-variable> + ,
111+ , -+<r-tripxpB-4 > H
<r-Jr i pxp> is the same as <r-expression> except that at the level of r-relop, the relational
operator “2 is omitted. This has the effect that expressions containing this operator must be
enclosed in parentheses when appearing in the final portion of a data triple. it Is required to
eliminate ambiguities caused by using > to terminate a data triple.
A-9
Appendix A
A.2.4 Outer structure of Pascal programs
<declarations>
---+<speci f icat ions>
L<procs,f
<specifications>
L
< l a b e l dec>
econst deo
+
<decl-stmts>
<main block>
---*<in-out a s s e r t i o n s > + B E G I N -wcompound tail>--,
A.23 Norrexecutable statemerrts
c 1 abe I dec>
<const dec>
<decl-stmts>
c t y p e deo< m o d u l e dec>
cschedu I er dew
<create deo
A-10
Verifier Syntax
Verifier Syntax
Appelldix A
c t y p e dec>
- TYPE -<identifier>+ = +cPascaI
type>4 1
war deo
h
+ VAR FtidentiIier>vr
; HePascal type>--, 1
b
VIRTUAL 3
.
t
<procs>
A.2.6 Procedure declarations and associated assertloas
<proc dew
I_) PROCEOURE --widentifier>
TLJ+
< i n - o u t a58ertlons>--+
<fun dew
I_) FUNCTION +cidentifier>dcfun params>-+
<params>
< f u n params>
I
+<PascaI t y p e > + ; +<fun a s s e r t i o n s > +
Verifier Syntax
Appendix A
<globals>
- GLOBAL -+ (
<fun a s s e r t i o n s >
win-out assertions>+
L < f u n globah -J
I-+;-+
< f u n globals>
--+ GLOBAL -+ t ,Fb<identi f ier>,l--
-PC----------l
II +
P
<in-out assertions>
wexi t stmt++
< i n i t i a l stmt> JL < e n t r y stmt> 3
< i n i t i a l stnit>
- I N I T I A L 6Fb<identifjer>4 = ~~widentifier>,-=r ; +
*
< e n t r y stmt>
+ E N T R Y *<a-expression>--, j ---)
< e x i t stmt>
b E X I T --+<a-express ion>--, ; +
A-12
Appendix A
Verifier Syntax
A.!&7 Module and Scheduler declaration
<module deo
+ M O D U L E -widentifier>+ I -wvisible p a r t > E<;iwiA:nvieible part>f- ; --+
< m o d u l e invis!ble p a r t >
wlnvis.ible p a r t > +
+ INVISIBLE
SCHEOULEO BY-<identifier>+ I
< s c h e d u l e r dec>
I_* SCHEOULER <-<identifier>4 ; d<sched v i s i b l e part>
<sched v i s i b l e p a r t >
@<visible part>+
R E C E I V E S *<identifier>+ ; -T
<visible p a r t >
- VISIBLE
wvisible i t e m deo
<base type dew f
-
l *
<invisible part>
---) I N V I S I B L E -wepeclfications>+tboundaries>
A-13
<mod in i t>+ END -P
. Appendix A
Verifier Syntax
<basetype dew
- BASETYPE -4dent i f ier>
<visible i t e m deo
<visible
proc dec>
- PROCEOURE *<identifier>
-< v i s i b l e f u n dew
- FUNCTION +<identifier>+<fun
pawme> t -+@ascaI type>-+ ;
+
<fun globah f
< a x i o m deo
I_) AXIOMS
w~expreasion~~
F O R A L L ( +<axiom-spew+ 1 ; fl
<axiom-spec>
~<ide;t~fierwl-~ : +4dentifirr,Tb
A-i4
;
Verifier Syntax
Appendix A
<boundaries>
b
-4nvar iant etmt>
cinvis-basetype> f
< i n v a r i a n t stmt>
b I N V A R I A N T -+<a-expression>+
:3
<invie-basetype>
- BASETYPE w<identifier>- = *<Pascal type>+ ;
+
I
<mod
init> --
y B E G I N *<cornPound tail>--, : 3
A.2.8 Module and condition variable instantiation
< c r e a t e dec>
F CREATE A T cidsn;iIisr,r
I ti<identifier>-+
+
;
b
I
<cond dew
--+ CONDITION +<ident i f ier>
A-15
Appendix A
Verifier Syntax
A.2.9 Pascal type declarations
<Pasta I t y p e >
<simple t y p e > - - - - +
<record type>
<pointer type>
<simple type>
<identifier>
<identifier>+._.
A
i
*<identifier>
<ident i f ier>- I
<identifier>
<signed number>
<signed number7 f
I
J
Fcidentl f ier7-r 1
b
1
<array type>
t’
Jb
1 p l e type7
3
- A R R A Y 3 [ -4
imited
, s i, m
OF
-<Pa8cai
<limited simple type7
b
-<ident i f ier>
< i d e n t i f i e r > - t
<signed number> f
<identifier>
x<s i gned numbewf
<signed number-7
3.T
<number>+
+
A-16
t
type>+
Verifier Syntax
Appendix A
<record t y p e >
- RECORD ’
T r ade:tjf
ier>T; !4+<Pascai
typewr END 3
xuni on type>
- I +J’ END -
- U N I O N -<identifier>-
I
-~PascaI type>
< p o i n t e r type>
I_) ‘T’ +<identif iem+
<f i le t y p e > =
b F I L E I-) O F -*<file P a s c a l type>---,
<f i I e Pasta I t y p e > is t h e s a m e a s < P a s c a l t y p e > e x c e p t i t d o e s n o t c o n t a i n < p o i n t e r
type>,
A-17
Verifier Syntax
Appendix A
A.2.10 Executable statements
<compound ta i I >
<statement>
c -<exprese i on>
+wariable>
PASS I VE 4
4
77 :A
-<identifier>
L ( ~<expre;8~on>-J+
1 -T
----* B E G I N -*<compound tail>
L--, IF *<expression>+ T H E N *<statement>
ELSE *<statement> f
+ GO TO --wnumber>
GOT0 it
b ASSERT - < a - e x p r e s s ion>
-3 COl’lMENT
- ASSUME iI
L
-w N E W I-) ( --+cvariabIe>+ 1
---) W I T H --f-twar;a:,le>-,+ 0 0 -wtatement>
.
- I N V A R I A N T +<a-expression>+ W H I L E -+<expre88ion++ 0 0 - < s t a t e m e n t > -<for s t a t e m e n t >
*<repeat s t a t e m e n t >
- READ -+ ( -+<identifier>+
, -widentifier>+ 1
-+ W R I T E + ( -+<identifier++ , +<identifier>+ 1
-+ R E W R I T E ---) t -*<identifier>+ 1
-<case s t a t e m e n t >
A-18
?
Appendix A
Verifier Syntax
<for s t a t e m e n t >
II* F O R +<identif ier>
L
c - < e x p r e s s i on>x 13w><expre88 i owl
I N V A R I A N T +<a-expression>--, 00 +<etatement>*
<r&peat s t a t e m e n t >
- REPEAT -<etatement>
UNTIL ti<expreereion>+
INVARIANT -+<a-expression>-+
r,J
<ca8e etatemenb
+ CASE +<expression>+ O F ~:ry~;;;?; ; @<8tatemenbr END w
A.24 Expressions in Pascal programs
< e x p r e s s ion>
b
-<simple e x p r e s s i o n >
<r-relop>+csimple
expression>J
<simple expression>
-<term> ,
+
-
+ - < t e r m > -
t-J
<term>
4<
factor>
* - < f a c t o r >
A-19
J
b
Appendix A
Verifier Syrl tax
<factor>
<variable>
-<identifier>
L
(
-f-wexpr;s;ion>‘J*
)
f
I
r
b<po8tap>,Jf
’
<pas tap>
< a - e x p r e s s i o n > is the s a m e as <r-expression> with the following changes--A union selection
: < i dent i f i et-> may be followed by an expression in parentheses; this permits the parser to
automatically build the union construction, as in executable statements. The history sequence
- o p e r a t o r @ is prohibited; record fields indicated by a period (.) may not have a parameter list
following the fieldname. These restrictions have the effect of prohibiting module history sequence
statements.
<number> is an unsigned constant.
~8 t F i ng> is a character string.
< i dent i f i er> is a sequence of letters and digits, starting with a letter.
A-20
3
Appendix B
Parser Error Messages
B. I General
The parser makes a pass over the source code you have provided for correct syntax. If this
results in no error, the message “SYNTAX SCAN COMPLETE” is given. If an error occurs, the
parser will tell you what it was scanning, what would have been an acceptable next token, and
what some previous tokens were.
This initial syntax scan merely verifies that the format of what is seen is correct; it makes no
checks on the actual content. If this syntax scan is satisfactory, a second phase is entered where
content checks are made. What follows is a list of errors that can occur during this second or
semantic phase. If this second phase is completed successfully, then whatever action the parser
was trying for you is then done. Note that when parsing Pascal code, verification conditions for
procedures and functions which were completely parsed prior to a semantic error will be present
and can be still worked on with the simplifier.
The following listing is in alphabetic order. The notation “vcg” following a message indicates that
the source of the error is the verification condition generator rather than the parser. This should
not normally be of concern to a user.
B.2 Semantic errors
ACTUAL PARAMETER TYPE DOES NOT MATCH FORMAL DECLARATION
The parser checks procedure and function calls to ensure that the type of each parameter matches
the declaration of that procedure or function. One of yours didn’t make it. Information printed
out may include the type expected or the name of the formal parameter in the declaration.
..
ARGUMENT LIST EXPECTED
A function name appeared in an expression and it was not followed by an argument list enclosed
in parentheses.
BAD PUT ENTRY--VERIFIER ERROR
.
An internal check in the parser symbol table entry code has discovered something that shouldn’t
be there. If this was a program product of some manufacturer, you’d be Instructed-at this point to
send in a trouble report. As it is, the choices are less appealing! In any case, it would be bad to
trust anything produced by the parser after getting this error.
B-l
Appendix B
Parser Error Messages
BASE TYPE FOR POINTER NOT DEFINED
ln an assertion within a Pascal program, you used the notation “cidentifier>t”. To correctly
translate this into an assertion the system understands,, the parser has to be able to figure out what
reference class the <identifier> belongs to. It does this by looking up the entity in its symbol table,
and in this case it couldn’t find it. If you want to include this as part of the assertion, you will
have to provide the reference class. Instead of this syntax, use *<base type> c <identifier> =) (no
blanks between + and <base type>).
BASE TYPE FOR REFERENCE CLASS DOES NOT MATCH WHAT WAS EXPECTED
In an assertion within a Pascal program, you used the notation “+<identifierI> c 4dentifier2> 3”
(or some qualified form equivalent to this). Either <identifierZ> was not of pointer type, or if it
was of pointer type, its base type was not the same as <identifier IX
BOOLEAN EXPRESSION EXPECTED
An expression of boolean type was expected, such as in a WHILE test or an IF test.
BOTH SIDES OF ASSIGNMENT MUST BE COMPATIBLE TYPES
For an assignment statement to be correct, the types of the entity being stored into and the type of
the expression being stored must be compatible. Thus, they must both be numbers, or one must
be a subset of the other, or they must be the same type. You had an assignment statement where
this was not the case.
BRANCHING INTO COMPOUND STATEMENTS PROHIBITED
You may not branch into a WHILE, REPEAT, FOR, or WITH body using the GOT0
a statement. If you need unlimited branching, you will have to create your control structure entirely
with GOT0 not using any of these iteration statements.
CASE NAME TYPE MUST MATCH CASE EXPRESSION
At the head of a CASE statement is an expression of a certain type. Each of the cases following
must be identified with a constant of the same type.
CHAR TYPE MAY ONLY HAVE ONE CHARACTER STRINGS
An entity of type CHAR may be a string at most one character long. Longer strings will be
allowed eventually.
B-2
Appendix B
Parser Error Messages
C L A S S N A M E JNCORR,ECTLY Q U A L I F I E D O R U S E D
A class na.me must be followed by a period and another Identifier when invoking a procedure or
function from the class externally. Alternatively, you tried to assign to a class procedure name or
function.
CONSTANT DUPLICATED IN THIS T Y P E DEFINITION
A union type consists of ids followed by types; each of these ids must be distinct within a given
type definition, You duplicated one of the ids.
CONSTANT MAY NOT BE QUALIFIED
You have an identifier which was given a value in a CONST or CONSTANT statement. These
identifiers have the value you gave substituted by the parser, thus they are really parse time
abbreviations. In particular, they are always scalars and can’t be subscripted, or have record
fields, etc. following them.
CONSTANT MAY NOT BE STORED INTO
You have an identifier which was given a value in a CONST or CONSTANT statement. These
identifiers have the value you gave substituted by the parser; thus they are really parse time
abbreviations. Therefore, you can’t store into them -- put them on the left hand side of a n
assignment statement except as part of a subscript or something like that.
CONSTANT OF A KNOWN ENUMERATED TYPE EXPECTED
Each union type consists of a list of id-type pairs. Each id must be a constant of the same
enumerated type. You have given an id which is not a constant of an enumerated type.
CONSTANT TYPE DIFFERS FROM PREVIOUS CONSTANTS
Each union type consists of a list of id-type pairs. All the ids must be constants of the same
enumerated type. You have given an id of a different type than previously encountered in this
. declaration.
DUPLICATE LABEL IN CASE STATEMENT
The same label appears twice in a case statement, Each case must appear at most once.
B-3
Apperldix B
Parser Error Messages
EMPTY CASE STATEMENT (vcg)
This message should not be printed under any circumstances. If it does occur, it indicates that the
parser has produced a case statement with no branches.
ERROR IN ASSIGNMENT STATEMENT (vcg)
This message should not be printed under any circumstances. If it does occur, it indicates that the
parser has produced an illegal assignment statement.
ERROR IN C-D-U -CASE I
Caused by forgetting to set _ to T .
ERROR IN C-D-U - CASE 2
Caused by forgetting to set _ to NIL.
ERROR IN C-D-U - THIRD TYPE
N o w y o u ’ v e r e a l l y d o n e I t . You were warned NOT to use the CONCURRENT Dynamic
LJnderbar feature UNLESS you talked to me first. Now that you are having trouble, don’t expect
me always to solve YOUR problem.
This message MIGHT also be caused by incompleteness in the W matcher, so be sure to send a
complete minimal protocol to BUG-VERIFY % STANFORD, zip code 94305, and, allow at Jeast
nine months for delivery..
EXIT ASSERTION OMITTED FROM PROCEDURE OR FUNCTION
An EXJT assertion is required by the system. The absence of one is usually detected by the
syntax scan. But when the word P R O C E D U R E or FUNCTION followed by Just a name is
found, the syntax scan must permit it since it could be the body of a block declared forward. If it
isn’t;this error is given.
FILES CANNOT APPEAR IN ASSIGNMENT STATEMENTS
You tried to assign to an identifier of type FILE. Files may appear only in assertions, READ
statements, and WRITE statements (in addition to being declared).
B-4
Appendix B
Parser Error Messages
FILES OF ENTITIES OF POINTER TYPE ARE PROHIBITED
The base type of a file may not be of type POINTER.
FOR CONTROL VARIABLE MAY NOT BE REDEFINED INSIDE FOR STMT
Pascal prohibits redefining the FOR statement control variable within its loop. Note that this
error can occur when the control variable is passed to a procedure which may change it -- i.e., as
a VAR parameter or when it is declared as GLOBAL within the called procedure. It can also
occur in more obvious ways.
FUNCTION NAME MAY NOT BE USED AS VARIABLE (vcg)
You have a function or predicate name appearing in an assertion or code which is also declared
as the name of a variable. This is not permitted.
FUNCTIONS MAY NOT HAVE SIDE EFFECTS--STRICT ENFORCEMENT
In order to permit only functions without side effects, the parser is extremely rigid in disallowing
things. In particular: function bodies may not contain global statements, JO statements, or NEW
statements. In addition, functions may not have VAR parameters. This rather severly limits
functions! You may have to make your function into a procedure which returns its value as a
VA R parameter. Sorry!
GENSYM AND YOU AGREE--SORRY!--RENAME YOUR VARIABLE
When the parser called the LISP function GENSYM to invent a n a m e f o r s o m e r e a s o n o r
another, the name returned was already in your program, declared as one of your entities in this
block. You must change the name of the entity of that type. This message will usually be given
in addition to an IDENTIFIER DECLARED MULTIPLY message.
GLOBALS FROM OUTSIDE THE MODULE MUST APPEAR IN VISIBLE GLOBAL
STMT
Module visible procedures may have two global statements: one, appearing with the visible
declaration, describes the entities global to the module that the procedure might change. The
second, attached to the invisible declaration of the procedure, details the module variables
changed by this procedure.
B-5
Appendix B
Parser Error Messages
IDENTIFIER DECLARED MULTIPLY 1N ONE BLOCK
This particular identifier is already the name of something in this block. Change one or the
other.
ID IN POINTER OF INCORRECT TYPE
When defining a pointer type, the pointer base type must be another type identifier. Since the
base type for a pointer type may appear before it is defined, this error may not appear until after
processing all TYPE statements for a particular function or procedure.
ID NOT DECLARED OR NOT A VARIABLE
In processing an expression, the parser found an identifier that was not in the symbol table; or if
it was, it was not declared as a VAR but rather was of some other kind. This error can occur, for
example, if a virtual variable appears in executable code (other than documentation or a
PASSIVE statement}. --
ID NOT DECLARED AS VISIBLE BASETYPE NAME
In the BASETYPE specification within the invisible part of a module, you tried to declare the
specifications of an identifier that was not declared as the name of a basetype in the visible
specifications.
ILLEGAL ENTRY ASSERTION FOR FUNCTION (vcg)
The ENTRY assertion for a function may not contain the function name.
-ILLEGAL PROCEDURE CALL (vcg)
The procedure call rule requires that each of the VAR parameters and GLOBAL*varlables in a
particular procedure call refer to a distinct variable.
IMP-ROPER SUBRANGE DEFINITION
Subranges may be declared as explicit types or as subscripts for arrays. They are usually two
values, in which case the lower value of the subrange must really appear before the upper value
in the defintion of the base type. In particular, for subranges of integers, the first integer must be
smaller than the second. Also the types of the two entities in the subrange must be compatible
with each other.
B-6
Appendix B
Parser Error Messages
I N T E R N A L E R R O R I N VCC O R RUNCHECK (vcg)
This message is produced only in the special runtime error checking version of the verifier. It
indicates a system error in the verifier.
INVALID ARGUMENT TYPE TO ARITHMETIC OR LOGICAL OPERATOR
The parser checks that each arithmetic or logical operator only receives sub-expressions of proper
type; thus Y expects only to find two numbers, NOT a boolean, etc,
INVALID CONSTRUCTOR OR SELECTOR F O R U N I O N T Y P E
CJnion type construction must have three elements: the type to be constructed, the tag to be
associated with it, and the value to be associated with it, in that order. The type of the value
must be consistent with the tag, and the value must be present. Therefore, there must be an
expression enclosed in parenthesis of the appropriate type, and there must be a tag of the
appropriate type. Union selection, however, merely consists of a union variable followed by
selection of a union field. No expression may follow.
J N V A L I D SUBRANGE I T E M
Subranges may be declared as explicit types or as subscripts for arrays. In the latter case only, a
VAR is permitted. In both cases, a number, an abbreviation for a number (identifier defined i n
a CONST or CONSTANT statement), or a constant of an enumerated type may be used. None
of these types of entities were found in your definition,
INVALID TYPE FOR CASE STATEMENT EXPRESSION
The expression following the keyword CASE must be of scalar type. Further, it may not be o f
type R EA L or a subset of type REAL.
INVALID TYPE FOR CONTEXT WHERE USED
.
An attempt was made to dereference (t) an entity not of type pointer, or subscript an entity not of
type array. Alternatively, in a FOR statement, the index variable and both expressions must be
compatible with a numeric type. Finally, too many subscripts were present for a particular v a r
(i.e., there were two subscripts to an array which only had one dimension, or one subscript to a
var that was not an array).
B-7
Appelldix B
Parser Error Messages
KNOWN TYPE NAME EXPECTED
When you define a type in terms of another type, the second type must already be known to the
parser (exception: pointer base types). Also, the base type for a reference class appearing in a
GLOBAL statement must be known to the parser. Finally, the type of a parameter to a function
or procedure must be known to the parser before seeing the function or procedure declaration.
LABEL APPEARS IN PROGRAM BUT IS NOT DECLARED
You use a label in your program unit but do not declare it entering the program unit (with the
LABEL declaration). Labels must be local to the procedure in which they appear, and must b e
declared there~
LABEL DECLARED AND REFERENCED BUT NOT PRESENT
Somewhere in your procedure or function, you have stated GOT0 n, but after completing
parsing your procedure- or function, the label n was not found on any statement within that
procedure or function. Note that if n is within the body of a nested procedure or function, it is
not regarded as being within the body of the outer procedure or function.
LABEL MUST BE POSITIVE INTEGER
A label must be a positive integer; it cannot be zero.
LABEL SPECIFIED MULTIPLY IN ONE PROGRAM UNIT
The same label appears on two or more statements in one procedure or function.
-
MISSING ASSERTION ON PATH THROUGH LABEL (vcg)
The program contains a closed path formed by a GOTO, but there is no assertion anywhere i n
the path.
MISSING ITEM IN LOADSYMBOLS INVOCATION
T h e LOA D S Y M B O L S c o m m a n d c o n t a i n s t w o p a r a m e t e r s . T h e f i r s t i s t h e n a m e o f t h e
procedure whose symbol table environment is being recreated; the second is the name of the file
containing the symbol table code. One of these was missing.
B-8
Apperrdix B
Parser Error Messages
MULTIPLY DEFINED IDENTIFER IN INVALID CONTEXT
Contrary to the usual scope rules, once an entity is defined to be a TYPE, MODULE, o r
SCHEDULER identifier, it may not be redefined as a TYPE, MODULE, or S C H E D U L E R
identifier in a less global scope, Give the new type, module, or scheduler another name.
NAME OF MODULE EXPECTED
In a CREATE statement, the identifier following the colon must be the name of an entity
previously defined as a MODULE.
NEW STATEMENT MUST HAVE POINTER ARGUMENT
A NEW statement can only initialize an entity of type pointer.
NUMBER OF PARAMETERS IN CALL DOES NOT MATCH DECLARATION
A procedure or function may be executed by being calied only with exactly as many parameters as
it was declared with.
PARAMETER LIST NOT PRECEDED BY FUNCTION NAME
While processing an expression, a parameter list (a list of expressions enclosed in parentheses) w a s
found. However, the entity preceding the parameter list was not of type function.
PATTERN VARIABLES MAY NOT BE PREDICATE OR FUNCTION SYMBOLS
A variable name appearing in a PATTERN statement in a rulefile was found in a context where
it would make a predicate or function into a pattern. This is a second-order match, and is
prohibited by the prover. Rulefile predicates and functions must be constants; they cannot be
instantiated in the prover.
PROCEDURE NAME E X P E C T E D
You had a statement which looked like a procedure call, but the entity that should be the name of
the procedure was not found or was declared to be something else.
B-9
Appendix B
Parser Error Messages
PROCEDURE OR FUNCTION DECLARED FORWARD AND NOT FOUND
You declared a function or procedure to be FORWARD and then didn’t provide the body of the
function or procedure. If you just want to specify the properties of a function or procedure
without specifying its body, use EXTERNAL or EXTERN instead of FORWARD.
PROCEDURE OR FUNCTION DELCARED FORWARD AND RESPECIFIED
When the body of a procedure or function declared forward appears, the parameter list, type,
initial, entry, exit, and global portions are not duplicated. The format is “PROCEDURE or
FUNCTION <identifier> ; < b l o c k > “ .
RECORD FIELD MODIFIES ENTITY NOT OF TYPE RECORD
Following an entity, the notation “.cidentifier>” was found, as if the entity was a record of which a
particular field was being selected. However, the entity being so modified was not of type
RECORD.
RECORD FIELD NAME MAY NOT BE USED AS VARIABLE (vcg)
You have used a record field name that is the same as the name of a variable in your program.
This is not permitted.
REFERENCE CLASS EXPECTED
Processing an assertion in Pascal code, a term of the form “r4dentifier I> c <identifier% 3” was
found. The entity +<identifieri> was not the name of a reference class known by the parser. You
need to declare a type that is a f <identifier I> to get the reference class.
-SCHEDULER MAY NOT BE SCHEDULED
A scheduler is used to control access to modules, and is assumed to run in a hardware mutual
exclusion state. As such, to have a scheduler for a scheduler is a built-in deadlock. Therefore, a
syntax error is given.
SCHEDULER NOT DECLARED OR OF WRONG TYPE
A scheduler for a module must be of type scheduler, Your name wasn’t. Alternatively, you tried
to enter some condition variables and didn’t have a scheduler with a RECEIVES field
(concurrent version only).
B-IO
Appelldix B
Parser Error Messages
SUBSCRIPT TYPE DOES NOT MATCH SUBSCRIPT DECLARATION
Each subscript of an array must be of a compatible type with the declaration of that array. Your
use of an array did not match on one or more of its subscripts. The printout may tell you the
..
type ex petted.
SUBSCRIPT TYPE MUST BE SCALAR
When defining an array type, the type of each subscript may not be a record, pointer, array, or
file.
SYMBOL TABLE TOO OLD -- PLEASE RECREATE IT
The LOADSYMBOLS and DUMPSYMBOLS operations have an internal check which make
sure that they are consistently used, You have tried to do a LOADSYMBOLS operation using a
file that was created too long ago -- there has been an incompatible change in the verifier symbol
table structure since then. You must recreate the file by another DUMPSYMBOLS operation or
get an older verifier.
THIS BUILT-IN FUNCTION MAY NOT BE QUALIFIED
You tried to follow a built-in function call by additional characters. Most built-in functions, such
as TAG or EOF, may not be qualified by de-referencing, record fields, subscripts, or union
selection.
THIS ITEM MAY NOT BE USED IN RULEFILES
Currently not used, it may be adopted when type checking is extended in rulefiles,
-
THIS PROCEDURE NOT FOUND ON YOUR SYMBOL TABLE FILE
The LOADSYMBOLS operation has gone through the entire symbol table file you gave it and
did not find the environment of the procedure or function you specified.
TOO MANY CONDITIONS IN THIS CLASS--CHANGE CVS
The maximum number of condition variables which may appear within any class is determined
by the value of a constant named CVS which must appear in your program. CVS did, in fact,
appear, but you tried to declare a class containing more condition variables (concurrent version
only).
B-H
Appendix B
Parser Error Messages
TYPE ERROR IN DATA TRIPLE
In a data triple appearing in a program assertion, the second entity of the data triple must be of a
correct type to qualify the first entity. The third entity must be of a type which can be stored in
an element of the first entity.
UNDEFINED OR UNKNOWN RECORD FIELD
You tried to qualify an entity of record type with a record field which did not appear in the
declaration of that type.
UNDEFINED OR UNKNOWN UNION TYPE FIELD
You tried to qualify an entity of union type with a union field which did not appear in the
declaration of that type.
UNION FIELD MODIFIES ENTITY NOT OF TYPE UNION
You tried to modify an expression not of union type with a union field.
UNKNOWN ERROR MESSAGE -- PARSER OR VCG ERROR
An attempt was made to emit an error message from within the parser or VCG. However, that
message did not exist on the error message file. Please let someone who fixes things know!
VARIABLE IN WITH-STMT NOT OF TYPE RECORD
The expressions following the keyword WITH must each evaluate to be a variable of type
RECORD.
VARIABLE MUST APPEAR IN GLOBAL STATEMENT
Within a procedure, you tried to reference a global variable which did not appear in a GLOBAL
statement, Globals m a y b e r e f e r e n c e d w i t h i n f u n c t i o n s w i t h o u t a p p e a r i n g i n a G L O B A L
statement; indeed this statement is prohibited within functions. See the next error for further
discussion.
B-12
Appendix B
Parser Error Messages
VARIABLE MUST APPEAR IN GLOBAL STATEMENT PRECEDED BY V A R
You have tried to change the value of a global variable. When you do this in a procedure, you
must put the name of the variable (or reference class, for pointer changes) into a G L O B A L
statement VAR list. The VAR list is necessary only when values are changed; not merely
referenced. If the global is merely referenced, it need not be preceded by VAR (and will simplify
proof problems for you if it isn’t). GLOBAL statements are not permitted in functions; in that
case you may have to convert the function into a procedure which returns its value as a VAR
parameter.
A global variable appearing in an INITIAL statement must also appear in a GLOBAL
statement. The assumption is that changing the value of the global is intended; if the global is
not changed, merely use the global name in assertions and drop the INITIAL statement.
Note that reference classes of pointer types may be globals, and thus may have to appear in the
GLOBAL statement.
VAR PARAMETER MAY NOT HAVE EXPRESSION PASSED TO IT
You have tried to pass an expression to a procedure in a position where a VAR parameter was
declared. This is not permitted, as it is not defined what it means to store into such an entity in
Pascal. You can pass an expression to a non-VAR parameter, but of course, such expression will
be strictly an input value to the procedure. Note also that GLOBAL statements are not permitted
in functions, which may not have side effects. Thus, getting this syntax error within a function
can require re-writing the function as a procedure.
VISIBLE BASE TYPE NOT DEFINED WITHIN MODULE
A type name appearing in a BASETYPE statement must be fully specified within t h e m o d u l e . I t
must appear in a normal TYPE statement therein.
-
WAIT-FOR STMT REQUIRES CONDITION VAR AS PARAMETER
T o use a wait-for statement, there can be only one Pa rameter. It must be declared as a condition
v a r iable within the class (concurrent version only).
WAIT-FOR STMT REQUIRES APPROPRIATE DECLARATION WITHIN SCHEDULER
To use a wait. for statement, there must be a scheduler containing a procedure named wait-for.
Further, that scheduler must have exactly two parameters: the first of type CVLINK, the second
of type SCHEDPROCNAME (concurrent version only).
B-13
*
Appendix C
Verification Condition Generator
Notation
x-.0 is a fresh identifier
ot is a reference class
CL1 A s s e r t i o n statertrerlts
ASSERT
PIASSERT L)R
ASSUME
P(ASSUME QR
COMMENT
PICOMMENT QJR
C.2 Basic executable statemeuts
ASSIGNMENT
PI,” {x:=e] P
(where x is an identifier)
x-O=<x,,f,e> 3 PIi 0 {x.fbe} P
(where x is a record)
a..O=<a,Eil,e> 3 Pi,” .O {a[i]:=e} P
(where a is an array)
+t-O=<+t,cxqe> 3 PJ$ 0 {x%-e} P
(where xt has type t)
C-i
a
Apperldix C
Verification Condition Generator
CASE
for i=l, . . . , n , QIASSUME c=ei; Si)R,
c=el v.. . v c=en
QICASE
c
O F el:Si; . . . ; en:SnjR
T h e p r e c o n d i t i o n c=ei v . . . v c=e,, is omitted if c has a subrange type containing only el, . . . ,
ell*
CONDITIONAL
QfASSUME L ; B)R, QJASSUME -L; C)R
QJF L T H E N B E L S E C)R
GOT0 and Labels
The verifier does not permit a block to be exited by a non-local GOTO. The other restriction is
that every closed path formed by GOTOs and labels must contain an ASSERT statement. Each
path through a labelled statement produces a separate verification condition. The rule used by
the verifier constructs an assertion at each labei. In the generat case, it is somewhat complicated.
However, if a label is at an ASSERT statement, the rule for G O T 0 Is
P 3 Rj
P (COT0 j} Q
where the statement at label J is ASSERT Rj*
a
NEW
There are two axioms for the NEW(x) statement. The first axiom applies If x Is an identifier.
Otherwise, the second axiom is used.
-POINTER~TO(x~O,+t)l\x~O~NiL 3 Qjf[ux -01; - o (NEW(x)] Q
qlNEW(s- 0); s:=s-OjR
c-2
I
Apperldix C
Verificatiorl Condition Gene,rator
REPEAT
R E P E A T statements are translated into equivalent W H I L E statements. As part of this
translation, labels appearing in the body are automatically renamed.
WHILE
hL(B)I, P =) I
A
VsB(h-L 2 9)
P(INVARIANT I WHiLE L DO BjQ
r
where 6~ is the set of variables changed in B .
WITH
WITH statements are eliminated by translation.
Cl.3 Procedures and fwctiom
PROCEDURES
A Procedure declaration has the form:
PROCEDURE p(U; VAR V)
GLOBAL (C; VAR H);
INITlAL X=X0;
ENTRY I(U,G,V,H);
EXlT O(U,G,V,H,XO);
BEGIN
body
END;
where
LJ
is the set of formal value parameters
V is the set of formal variable parameters
G is the set of unchanged global variables
H is the set of changed global variables
X0 is A set of logical variables that may appear in assertions.
Two rules are used to define the semantics of procedures: The procedure declaration rule Is used
to check the consistency of the assertions in the declaration. The procedure call rule is used to
check the consistency of programs that call p.
c-3
Appendix C
Verification Condition Generator
There is a slight complication in the declaration rule concerning value parameters whose values
can be changed by the body. Jf a procedure q calls p with a value parameter, p operates on a
copy of the value, so if p changes the value of its parameter, the change is not visible to q. In the
procedure declaration rule, this behavior is modelled by requiring the exit assertion to refer to the
initial values of value parameters, before execution of the body. The value parameters U are
divided into the subsets U, of variables that can be changed in the body, and UC, variables that
r e m a i n c o n s t a n t . N e w v a r i a b l e s UO, are introduced to stand for the initial values of value
parameters that can be changed in the body. Occurrences of variables in U, in the exit assertion
are replaced by the new variable in UO,, to insure that the exit assertion refers to only the initial
value.
The declaration rule checks the consistency of a procedure with its ENTRY and EXIT assertions
by proving the formula
I(Uc,Uv,G,V,H)~X=XO~UvdJOv {body} O(U,,UO,,G,V,H).
In the procedure call rule below, A is the set of actual value parameters, and B is the set of actual
VA R parameters. Each _yAR parameter consists of an identifier, Pip followed by a possibly empty
sequence of component selectors,
Si*
The call rule introduces new variables tl, . , . , tn to save the
values of the selector sequences of the VAR parameters. B-0 is the set (&O, . . . , on-0) of new
variables introduced to stand for the values of the VAR parameters after the procedure call.
Similarly, H-0 is a set (hi--O, . . . , h,-0) of new variables for the VAR globals. The variables
actualsX are the actual initial values corresponding to the formal variables in X0.
The formula ap asserts that the final value of each variable changed by the procedure call is
functionally dependent on the initial values of all the parameters. A new uninterpreted function
symbol, pi(A,G,B,H), is introduced to stand for the final value of each VAR parameter and VAR
global,
Q{tpi;. . * ; tntsn} (I(A,G,B,H) A
(O(A ,G,B-.O,H - 0 ,aCtUalSx)
A @p(A,G,B,H,B-O,H-O)
{Pit<Pi,‘i,Pi-O>; * * - ; (3nt<Pnvtn,Pn-O>; H&H-O) R))
Q {p(kB)) R
w h e r e (Pp(A,G,B,H,B-.O,H-0)
E
~~I-O=PI(A,G,B,H)
A
A h 1-O=pn+ i(A,G,B,H)
* * m A on-Oepn(A,G,B,H)
A
* * . A hm-Oppn+m(A,G,B,H).
c-4
Appendix C
Verification Conditioll Generator
Example: consider the declaration
P R O C E D U R E p ( d : m i ; V A R e:m2; V A R f:m3);
I N I T I A L d=dO,f=fO;
E N T R Y I(d,e,f);
E X I T O(d,e,f,dO,fO);
BEGIN
body
END;
Then for the call p(a,b[iJ,xLf), we have:
Q (t it~elector(EiJ); t2tseleclor(cx>.f)j
(I(a,bEi J,*tcx>.f) A
(O(a,b-O,*t-O,a,*tcxD.f)
A
b-O=p I(a,bliJ,*tcx>.f)
A
#t-Oup2(a,bllJ,rtcx~.f)
(bttb,t l,b-O>; +ttcxt,t2#-O>) R(a,b,x,+t))
Q (p(a,bEi 1,xt.f)) R(a,b,x,+t).
The assignment rule reduces the upper formula to
Q 3 (I(a,bliJ,+tcx=>.f)
A (O(a,b-O,*t-O,a,stcx>.f)
A
b-O=p l(a,b[il,*tcx~.f)
A
rt_O=p2(a,blil,*tcx~.f)
3 R(a,<b,[iJ,b_O>,x,<rt,cx>.f,et-O>))).
FUNCTIONS
A Function declaration has the form
FUNCTION f(U):m;
ENTRY I(U);
E X I T O(U,f);
BEGlN
body
END;
where U is the set of formal value parameters.
The body contains assignment statements of the form f:=e, which assign a value to the function.
Occurrences of f as a term in the exit assertion 0 are interpreted to stand for the value of the
function. When f appears as a function sipn in 0, it has its usual interpretation -- the function f.
c-5
Apperldix C
Verification Condition Generator
The system checks the consistency of a function declaration by proving the formula
I(U) (body@=fi
_ l:=e} OWLfn).
A new variable, f-_fn, is introduced and the assignment statements are renamed, to avoid conflicts
between the two interpretations of f. The formula above is used when none of the varables in U
can be changed by the body. When this is not the case, additional new variables are introduced
as in the procedure declaration rule.
The semantics of function calls are not given by a single rule. Instead, the semantics of the
executable Pascal statements have been defined to account for function calls. To simplify the
presentation, the axioms stated elsewhere in this appendix assume that no function calls occur in
executable statements. Thus the actual rules implemented in the system are slightly more complex
than the ones listed here.
To indicate the general approach, consider assignment statements xEiJ:=j, where i and j are
expressions containing function calls. Let fl(A I), . . . , fn(An) beGan order in which the function
calls can be evaluated to execute the assignment, and let Ik(Uk) and Ok(Uk,fk) be the entry a n d
exit assertions for fk.
Then under the actual axiom used in the system, the conditions for
assignment are expressed by
1 &A I} A (0 itA if&A 1)) = . . . In(An) A (On(An$n(An)) 3 RI:X,L~J,J>) * * * ) ~X(i~:P.U R*
C-6