Home

stanford pascal verifier user manual

1. 0 n ORDERED A 1 N VAR 1 TEMP INTEGER BEGIN Jsel FOR 1 TO N I INVARIANT PERMUTATION 0 n ORDERED A N 142 N n PARTITION A 1 N I41 N DO FOR J 1TO N I INVARIANT PERHUTATION A AQ n ORDERED A N 142 N ISBIGGER A LJ A 1 J 1 n PARTITION A 1 N 151 8 00 IF A CJ 2ACJ41 THEN BEGIN TEMP ALJ J 1 11 END END BEGIN END 5 6 A pointer example The procedure below has a side effect It changes the contents of the cell referenced by its X parameter by manipulating Y The problem is to verify this The type declaration PNTR 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 Introduction to the Stanford Pascal Verifier PASCAL TYPE PNTR fCELL CELL RECORD CAR INTEGER END PROCEDURE SIDEFFECT VAR Y GLOBAL VAR CELL ENTRY X4 CAR 1 EXITX CAR 2 BEGIN Y X Yt CAR 2 END The single verification condition for procedure SIDEFFECT is CELLcX gt CAR n POINTER TO Y CELL n POINTER TO X CELL n HCELL_ lt ACELL cX lt ACELLcX gt CAR 2 gt gt ACELL_ cX gt CAR 2 The identifier CELL_O refers to the refere
2. 1 lt file_name gt Eee short file name Eodem complete file spec is the standard monitor syntax for a file name vc spec M LC Th AI lt ru e name rule f il e name lt identifier gt t lt switches gt lt par_settings gt 3 par settings lt name lt val Command Syntax par name par value refer to the list of System Parameters given in Part Section 2 2 Appendix A Verifier Syiitax A 2 1 Outer level of input source input o ne lt rules gt eee pese e rule dec RULEFILE identifier CONSTANT E377 P CONST l PATTERN lt rule stmt gt lt backwardstatement gt creplacestatenent gt J foruardstatement lt rule label gt lt identi fier 1 Pascal program hoc main 5 Appendix A Verifier Syntax A 2 2 Statements that appear inrulefiles lt backuardstatement gt 23 INFER Mio ae a cea aah TON lt replacestatement gt gt REPLACE er relati M BY r case exp er a foruardstatement 12 INFER lt case gt r uhenever par po r from par isl lt from part FROM x r expression lt r whenever part gt WHENEVER lt r_express i i
3. WRITE lt identifier gt identifier REWRITE xidentifier case statement A 18 Appendix A Verifier Syntax lt for statement gt FOR lt identifier gt lt express i IE TO express i on t DOWNTO m INVARIANT a expression 00 statement repeat statement REPEAT m UNTIL gt INVARIANT lt a_expression gt case statement CASE expression OF 1 lt statement gt END identifier 1 A 2 1f Expressions Pascal programs express ion lt simple SPT E lt r_relop gt lt simple lt simple expression gt lt term gt lt term gt lt factor gt lt fat bow gt DIV MOD 19 Appendix A Verifier Syn tax lt factor gt number string expression NOT factor variable variable lt lt i dent i f i a Kaeo a NONE ik J posta lt pos tap gt lt identifier gt 1 lt identifier gt lt expression gt 2 poe aa ae lt a expression gt is the same as lt r expression gt with the following changes A union selection lt identifier gt may be followed by an expression in parentheses this permits the parser to automatically build the union construction as in exe
4. V CREW Q CASE c OF 5 The precondition c e v is omitted if c has subrange type containing only CONDITIONAL Q ASSUME L Q ASSUME L C R Q IF L THEN ELSE CjR GOTOand 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 label In the general case it is somewhat complicated However if a label is at an ASSERT statement the rule for GOTO is P Rj P GOTO j Q where the statement at label jis ASSERT Rj 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 ax_O NIL gt oh 9 NEW x 0 Q NEW s_ 0 s s_0 R Q NEW s R c 2 Appendix C Verification Condition Generator REPEAT REPEAT statements are translated into equivalent WHILE statements As part of this translation labels appearing in the body are automatically renamed WHILE P gt I 4 amp 1 gt Q P INVARIANT I WHILE L DO where is the set of variables changed WITH WITH statements are eliminated by translation C 3 Procedures and functions PROCEDURES A Procedure dec
5. 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 x iJ j where i and jare expressions containing function calls Let f Ag order in which the function calls be evaluated to execute the assignment and let 1 Uy and O U f be the entry and exit assertions for fk Then under the actual axiom used in the system the conditions for assignment are expressed by I A D D gt 1 f AS RE tij xlike j R C 6
6. Verification Examples 5 1 First example understanding VCs 5 2 Concepts documentation and verification 5 3 A hard invariant 5 4 Defining concepts to document a program 5 5 Specifications for sorting 5 6 A pointer example 5 7 Verification of Pascal list structure operations 5 8 A larger example PARTII Chapter Differences from Standard Pascal 1 1 Comments 1 2 Program files 1 3 Procedure definitions 1 4 Assertions Contents 15 Blocks 56 16 Types 37 1 7 Functions 37 18 Input Output 19 Global variables 38 1 10 Virtual variables and Passive statements 1 11 Operator precedence i 1 12 Union types Chapter 2 User Commands 42 2 1 Imperative commands m 2 2 Setting system parameters 46 2 3 Query commands 46 2 4 System control Chapter 3 Description of the Simplifier 48 31 Introduction dn 3 2 Prover for arithmetic 49 3 3 Record prover 50 34 Array prover 50 3 5 List structure prover 50 3 6 Remarks Chapter 4 The Rule Language 51 4 1 Introduction to rules 4 2 Using the rule language References 75 Appendix A Syntax Charts Art Appendix B Parser Error Messages Appendix VCG Axiomatic Semantics 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
7. lt r f e gt g ng 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 of terms within data triples that is the axiom r f el g e2 e r g e2 gt f el gt 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 il 1 gt a lt lt a i el i e2 a i e2 a 1 e Lj if i then e else alj Again the axiom for permutations within data triples is missing There are at the moment problems with the array prover in the verifier because of an interface problem 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 1 gt 1 e it therefore lacks the axiom j gt ca il e j alj Evaluating SLOWARRAYPROVER turns on a version which implements the three axioms above
8. Ckapter 1 Differences from Standard Pascal In the outermost block of a program the ENTRY and EXIT assertions appear immediately preceding the BEGIN that starts the block The order is ENTRY then EXIT or just EXIT An INITIAL statement if present precedes the ENTRY EXIT assertions Thus PASCAL PROCEDURES AND FUNCTIONS EXIT MUMBLE A B BEGIN Zmain block of the program END 14 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 have more than one CONST TYPE or VA R statement 36 Part Il Chapter i Differerrces from Standard Pascal 16 Types A previou
9. 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 THE RULE LANGUAGE 4 1 Introduction 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 LITERAL is an atomic formula or a negated atomi
10. ged mod x y ged x y if y 0 mod x y lt x The program uses these properties by repeatedly replacing one of the values x or y by mod x y PASCAL FUNCTION HOD I J INTEGER INTEGER ENTRY 20a J50 MOD28 EXTERNAL FUNCTION YO INTEGER INTEGER ENTRY X050 4 YO gt 8 EXI T G 6CD X0 YO VAR X Y R INTEGER BEGIN XeXB 0 REPEAT R MOD X Y XeYi YeR UNTIL 0 RIANT GCD X Y a X gt 8 a gt 0 Ge END The invariant for the REPEAT loop follows immediately from our basic idea of replacing one argument of gcd x by mod x y and thereby not changing the value of ged The next step towards a verification is to express the facts about gcd 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 general rule telling us which is better each method has its own advantages and disadvantages Let us specify the properties of gcd with forward rules Part I Introduction to the Stanford Pascal Verifier RULEF ILE GCD GCD1 REPLACE GCD X 0 BY X GCD2 REPLACE BY X GCD3 REPLACE GCO X Y BY GCD Y X GCD4 REPLACE GCD X Y WHER
11. lt set command gt lt reset_command gt lt open command gt CLOSE lt information command gt HELP TRI SHOW lt name STATUS Command Syntax less or equal lt or lt not equal or lt gt and Aor amp reference class extension 0 or amp amp reference class selection or or M Appendix A Command Syntax lt read command gt READ gt lt fi le name gt gt READVC J pri n t command gt PRINTVC aes T gui sui lt simp_command gt SIMPLIFY eee aL to f i RESIMPLIFY TENA sui TUNE load command LOAD lt shor tf i le_name gt gt LOADVC file name LOADRULE lt dump command gt DUMP lt f i e name gt DUMPVC lt name EE DUMPRULE lt f i le_name gt lt rule_fi ere lt delete_command gt gt DELRFILE RICE S lt rule_fi eT OELRULE NM gt A 2 Appendix A lt alias command gt ALIAS t identif lt number E E se t command gt SET par settings rese t command gt 2 RESET lt name lt open command gt OPENFILE lt file_name gt gt Command Syntax Appendix A lt to_file_name gt TO lt complete_fi
12. 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 Union types The construct UNION has been added to replace variant records UNION is 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 TYPE untype UNION al ti 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 1 untype x ti SELECTION 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 not ai 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 c
13. 1 0 lt Y2 100 X 2 1 A vere 101A i RM lt 92 180 Y1 2 1 180 X A 2 1 1 Y1 18 X v X 181 Y1 18 10x Y2 1 lt 92 8 Y2 1 Unsimplified Verification Condition MAIN 2 100 X m lt 101 A X 10x1 92 6 lt 1 Unsimplified Verification Condition MAIN 3 8 lt 2 X V lt 101 Part 1 Introduction to the Stanford Pascal Verifier 1 10 2 lt 92 100 lt 1 2 1 100 lt 1 10 10 X 181 A Y1 10 91 Unsimplified Verification Condition MAIN 4 0 lt 2 1880 X A Y2 1 A 1 X 181 Y1 10xY2 92 100 Y1 188 lt X 2 1 1 1 11 lt 101 Y1411 10 2 1 lt 92 A 0 Y241 simplify Simplified Verification Condition MAIN 1 TRUE Simplified Verification Condition MAIN 2 TRUE Simplified Verification Condition MAIN3 TRUE Simplified Verification Condition amp TRUE 20 Part 1 Introduction 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 maxof x a 4 7 to be true if x is the maximum of the array elements ali with sisr We can give a formal definition of maxof as maxof x v df Vi sisr ali sx 3f lt lt alf x From this definition the
14. 1 3 ISDERIV STRT IMBED SOURCE BEGIN STRT KIND NONTERMINAL STRT INFO2 START_SYMBOL PUSH MAKE SEQUENCE STRT READ SOURCE LOOK DONE F ALSE INVARIANT ERROR 50 1 DONE SOURCE8 CONCAT SOURCE READ CON1 LOOK giles A ISDERI V STRT CONCAT SOURCE READ STACK DONE EMPTY SOURCE A SOURCE8 SOURCE READ WHILE NOT OONE DO BEGIN 33 Part Introduction to the Stamford Pascal Verifier TOP T IF T KIND TERMINAL THEN IF T INFO1 LOOK THEN ERROR ELSE BEGIN WR I TE SOURCE READ LOOK X virtual IF EOF SOURCE THEN DONE TRUE ELSE READ SOURCE LOOK END ELSE BEGIN ISRHS T LOOK PUSH END END IF NOT EHPTY STACK 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 a qe eo 1 DONE SOURCEB CONCAT SOURCE READ 1 LOOK SOURCE ISDERIV STRT CONCAT IMBED SOURCE READ STACK DONE EMPTY SOURCE a SOURCE SOURCE_READ a EMPTY STACK ERROR MSG i a EMPTY STACK STACK CONI T 0 STACK 21 Ja 0 STACK ACK 2 TOP STACK T STACK _B KIND TERMINAL 0 NFO1 LOOK RROR MSG 1 ERRORMSG 1 DONE 3 SOURCE CONCAT SOURCE READ CON1 LOOK SOURCE I SDERI V STRT CONCAT SOURCE READ STACK 2 A DONE E EMPTY SOU
15. Approximately the maximum number of forward case splits which will be allowed Ail others will be ignored This value does not include splits which are eliminated due to case reduction TRACE switch If this switch is set a proof summary will be printed after simplification of a verification condition TRACEFACT switch If TRACE and TRACEFACT are both set the proof summary will 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 SHOWGOA L switch 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 42 7 SHOWTEST switch The theorem prover will show ail instantiated literals which
16. B H h 1 0 j A G B H A hg Os pa 4 Appendix C Verification Condition Generator Example consider the declaration PROCEDURE p d mi VAR e m2 VAR f m3 INITIAL dedO f f0 ENTRY EXIT 40 0 BEGIN body END Then for the call p a bli xt f we have Q t eselector Li toe selector cx2 f I a bli atcx gt f A O a b_0 t_O aetex gt f a b_O p j ablilstexo f a t_O po a bli etex gt f be lt b t jb 05 te lt st to at_0 gt R a b x t Q p a bli xt f The assignment rule reduces the upper formula to Q gt Ia bli tex gt f A O a b_0 at_0 a atex gt f a b_O p j a bliletcx gt f a t_O po a bli etex gt f gt R a b i b 0 x et cx f at 0 FUNCTIONS A Function declaration has the form FUNCTION f U m ENTRY I U EXIT O U f BEGIN 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 sien in 0 it has its usual interpretation the function f c 5 Appendix C Verification Condition Generator The system checks the consistency of a function declaration by proving the formula O U f fn A new variable f_fn is introduced and the assignment statements
17. CONCEPTS FORMAL THEORY RUL SPECIFICATIONS ULES if VERIFICATION4 DOCUMENTED PROGRAM Y COMPILED CODE 5 1 First example understanding VCs This is a simple example in constructing documented programs and reading very simple V Cs We hope eventually to automate aids for analyzing V Cs We begin by constructing a procedure that multiplies a given value parameter Y by a global value N and stores the result in X its specifications are PROCEDURE CONSTHULT VAR X INTEGER Y INTEGER GLOBAL EXIT XeYxN 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 YxZ to be an invariant of the loop This shouldbe sufficient internal documentation Finally try calling CONSTMULT X N to compute the square of Part Introduction to the Stanford Pascal Verifier PASCAL VAR N Z INTEGER PROCEDURE CONSTMULT VAR X INTEGER Y INTEGER GLOBAL N EXIT X YxN VAR Z INTEGER BEGIN 2 0 INVARIANT 7 WHILE Z N DO BEGIN XeX Y ZeZ41 END END EXI T Z NxN BEGIN CONSTMULT 2 4 END For CONSTMULT to be consistent with its documentation there are two VCs that must be proved VCs 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 We c
18. ENTRY TAG n TAG Yt E X I T TAG RESULT N a BEGIN NEW RESULT RESULT note implicit application of to convert INTEGER to type U X END 41 2 USER COMMANDS A system command consists of a command keyword possibly followed by some arguments anda 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 1 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 rulefiles 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 commands 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 a
19. Y SENTINEL n YeNIL E XIT REACH AWORD ROOT SENTINEL VAR 2 REF BEGIN NEN 2 Zt NEXT NEXT Yt NEXT Z END The entry assertion implies that the list from ROOT to SENTINEL is oopfree and Y is a pointer 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 oopfree This property of INSERT is easily verified using the rules for data structures and some rules defining Reach Here are three examples of rules defining Reach Ri INFER REACH D X Y FROM REACH D X Z n REACH D Z Y R2 REPLACE REACH D cX5 COUNT E Y ZH BY REACH D Y Z R3 INFER REACH D cY2 NEXT Z gt X W FROM REACH D X Y n REACH D Z W n INBETHEEN D Y Z Rule R I is implied by the transitivity of Reach Rule R2 states that operations on the COUNT field i e E preserve oopfreeness Finally rule states some conditions under which the assignment eZ preserves loopfreeness between X 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 7 Yt NEXT Z Z NEXT END The result of the a
20. a lt r where part gt WHERE a 6 Appendix A Verifier Syntax A 2 3 Expressions that appear inrulefiles lt r_case_exp gt gp o5 ion CASES lt expression E w express gt M LU 3 mE r disjunction lt r conjunct ion E V w conjunction T4 r conjunct ion r not expressi 3 lt not expression lt r not expression gt ENG i ional r relational r simple expression germ RR UN A 7 Appendix A lt r_relop gt lt gt lt gt J i i lt sinple expression r term lt _ gt lt r_term gt lt r_f ac MS Earn oe ai er _mulop gt ser_fac tors lt r_mulop gt DIV MOD 4 4 4 lt r factor gt lt number gt string r expression r variable A 0 Verif ier Syntax Appendix A Verifier Syntax r variable scm cs c qr advo RRI U mm r select lt r_modfn gt gt lt exl gt lt r_select gt lt identi fier r variable 9 o identifier lt exlist 1 r gt Lad r exlist lt r_exlist gt ue CU lt r_data_triple gt lt r variable y Reena lt r_tripxps
21. 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 NFO1 1501 INFER 15 SEQUENCE X 1502 INFER ISDERIV X CONCAT Z CONCAT R T FROM ISDERIV X CONCAT Z L T A I SPROD L R IMB1 REPLACE I MBED MAKE SEQUENCE X BY MAKE SEQUENCE 1MBED X 2 REPLACE IMBED CONI X Y BY CONI IMBED X IMBED Y IMB3 REPLACE CONCAT 1 IMBED Y BY IMBED CONCAT X Y IMB4 REPLACE IMBED CONCAT X Y BY CONCAT IMBED X IMBED Y IMBS REPLACE APPEND X IHBEU Y BY IMBED APPEND X Y IMB6 REPLACE APPEND X Y BY APPEND IMBED OO IMBED Y IMB7 WHENEVER IMBED X FROM TRUE INFER X IMBED X INFO1 IMB8 WHENEVER X INFOI FROM TRUE INFER 1 X INFO 1 WHENEVER EMPTY X FROM EMPTY X INFER X NULL SEQUENCE NS2 FROM TRUE NFER IMBED NULL SEQUENCE NULL SEQUENCE NS51A WHENEVER EMPTY X FROM EMPTY X INFER XzNULL SEQUENCE MSi REPLACE CONCAT MAKE SEQUENCE X Y BY CONI X Y 1 REPLACE APPEND NULL SEQUENCE X BY MAKE SEQUENCE X WHENEVER FIRST X FROM TRUE INFER CON FIRST OO REST 00 X CON1 REPLACE CONCAT X CONI U V BY CONCAT APPEND X U CON2 REPLACE CONCAT APPEND X U V B
22. and Wirth Pascal User Manual and Report second ed Springer Veriag New York 1975 16 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 17 J King and R W Floyd Interpretation oriented theorem prover over integers Second ACM Symposium on Theory of Comp Massachusetts 1970 18 D E Knuth The art of computer programming Vol Ill Sorting and Searching Addison Wesley Publishing Company Reading Mass 1973 19 D C Luckham and N Suzuki Automatic program verification IV Proof of termination within a weak logic of programs Al Memo AIM 269 Stanford Artificial Intelligence Laboratory Stanford University Oct 1975 also Acta Informatica 8 1977 21 36 20 DC Luckham and N Suzuki Automatic program verification V Verification oriented proof rules for arrays records and pointers Al Memo AIM 278 Stanford Artificial Intelligence Laboratory Stanford University March 1976 revised Verification of array record and pointer operations in Pascal Dec 1978 211 7 Manna Mathematical Theory of Computation McGraw Hill Book Company New York N Y 1974 22 C G Nelson and DC Oppen Fast decision procedures based on congruence closure Al Memo A 309 Stanford A rtificiai Intelligence Laboratory Stanford University Feb 1978 also Proceedings of the 18th Annual I
23. 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 4 however unless there is rule which expresses 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 rules had been ordered NI 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 gt 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 subgo
24. base type PEN axiom lt invisible part gt INVISIBLE in i t END eee Appendix A Verifier Syntax lt basetype dec gt BASE TYPE lt visible item dec gt lt visible proc dec visible fun deest visible proc dec PROCEOURE E s pone lt visible fun dec gt FUNCTION lt identifier gt lt fun params 1 Pascal types gt E fun lt axiom dec gt AXIOMS 3 ae FOR ALL axiom spec J axiom spec t lt identifier gt A i4 Appendix A lt boundaries gt lt iant DOE eel invi lt invariant stmt gt INVARIANT lt expression 1 invis basetype BASETYPE c oeldenti fiers lt Pascal type mod init BEGIN comnound tal I A 2 8 Module and condition variable instantiation create dec CREATE t lt identifier gt lt cond dec gt CONDITION 1 T Verifier Syntax Appendix A A 2 9 Pascal type declarations lt Pasca type gt simple type 4 array type record type pointer type union type file type simple type identifier identifier cident tiers lt ident i f ier 1 2 lt signed number gt lt signed number
25. bool signal whenever a depth bound is reached PROOFDEPTH natnum maximum backward proof depth RULE bool enable rulehandler SHOWFACT bool enable assertion display during proof SHOWGOAL boot enable subgoal display during proof SHOWTEST bool enable display of tests made during proof SUMMATCH bool enable special sum matching extra subspace instance TERMINAL bool if set file output from SIMPLIFY and PRINT VC is also displayed on the terminal TRACE bool enable proof tracing TRACEFACT bool enable display of assertions made in trace output TRACEVC bool enable display of intermediate VCs during proof works only if TRACE is set 45 Part II Chapter 2 User Commands Current default values can be found using the SHOW command OPENFILE The command OPENFILE opens a backup file 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 FOO NOT Note that output cannot go to two different files simultaneously Thus the backup file has to be closed 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 take
26. consideration If we could not have eliminated this case semantically the formula would not simplify to TRUE because this case represented propositionally is TRUE FALSE or FALSE Thus data base contexts always 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 example the rules FROM B4A INFER D and FROM D INFER C are used to prove the verification condition AAB 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 the 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 condition and a contradiction is now evident Thus gt C has been proved using the two rules To prove AAB gt CaD multiple data base contexts would be used First a contradiction would be derived fr
27. discussion Appendix B Parser Error Messages VARIABLE MUST APPEAR IN GLOBAL STATEMENT PRECEDED BY VAR 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 GLOBAL 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
28. gt lt global d fun dec FUNCTION lt identifier gt lt fun params Pascal type 1 fun assert ions 4 params VIRTUAL E fun params 1 lt identifier gt L VIRTUAL 2 i 1 Appendix A Verifier Syntax globals GLOBAL VAR zl 4 J 7 1 fun assert ions errr globals gt lt fun globals gt GLOBAL in out assertions 4 ae lt in out assertions gt t stmt gt lt initial Ree sitos initial stmt INITIAL lt identifiero dq UAR NE 242 lt entry stmt gt ENTRY lt a_expression gt gt lt exit stmt gt EXI T lt a_expression gt gt Appendix A Verifier Syntax A 2 7 Module and Scheduler declaration lt module dec gt MODULE lt identifier gt lt visible part module invisible gt EXTERN module invistble part INVISIBLE lt invisible part gt BY lt identifier gt lt cond EMI scheduler dec SCHEOULER identifier 1 sched visible part invisible part gt EXTERNAL EXTERN sched visible part ue Zee part RECEIVES s lt identifier gt gt J lt visible part gt VISIBLE item mp lt
29. gt gt lt r_select gt lt r_tripxp gt is the same as r expression except that at the level of r_relop the relational operator gt 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 Verifier Syntax A 2 4 Outer structure of Pascal programs lt declarations gt lt specificat eee lt specifications gt eee deed Leane atuto lt main block gt lt in out assertions gt BEGIN compound tai l gt A 2 5 Norrexecutable statements lt 1 1 dec LABEL MNT M lt const dec gt CONSTANT lt identifier gt signed number 9 string CONST decl stmts lt type gt var dec module dec schedu er dec create dec A 10 Appendix A Verifier Syntax lt type dec gt TYPE lt identifier gt Pascal type gt lt var dec gt VAR 1 Pascal type gt VIRTUAL J lt procs gt dec gt lt fun ges BEGIN compound tail gt EXTERNAL decl CR EXTERN FORWARD A 2 6 Procedure declarations and associated assertions lt proc dec gt PROCEOURE ORAE E t ogee asser tlons
30. 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 1 FROM P x A INFER 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 this 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 ATOM FROM ATOM x INFER x CONS y z will cause the prov
31. 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 the module It 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 parameter It must be declared as a condition variable 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 Appendix C Verification Condition Generator Notation x_0 is a fresh identifier t is a reference class C 1 Assertion statements ASSERT LoR P ASSERT L R ASSUME PAQ2R P ASSUME QJR COMMENT P gt Q R P COMMENT QJR C 2 Basic executable statements ASSIGNMENT PIX x e where x is an identifier X O x f e gt PIE 0 where x is a record a O ai e gt PB o where a is an array st O et cx2 e gt Pit 0 P where xf has type t Appendix C Verification Condition Generator CASE for 1 n QASSUME cee S R
32. of VCGEN is presented in 14 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 Part 1 Introduction to the Stanford 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 GOTO labels There are other required assertions e g for global variables and the details of these are in Part 11 Chapter 1 It is easy to modify
33. of the above axioms The 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 In 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 In addition to lt we allow lt as a predicate symbol but define x lt y to be x I lt 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 and there is some ad 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 record prover handles expressions involving storing into and selecting from records and record fields The following axioms are implemented 49 Part Il Chapter 3 Description of the Simplifier lt r gt r r f el f e2 lt r f e2 gt r f e f e
34. of the numbers of cases propagated 4 2 5 Backward rules One way to think about a backward rule in this environment is to consider itas the contrapositive of a forward rule Thus the backward rule INFER C FROM D could be considered to be equivalent to FROM C INFER D Now suppose we write a backward rule Cl INFER A FROM Ba The contrapositive of gt A is A gt This could be written as the forward rule C2 FROM A INFER CASES B C END 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 ORD INFER Ordered a i j FROM i lt j Ordered aj j 1 alj 1 salj ORD2 INFER Ordered a i j FROM i lt ja Ordered a i 1 j alijsali 1 63 Part li 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 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 do 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
35. see Part Il Section 4 2 13 Finally proof of the procedure call depends on the VC Unsimplified Verification Condition MAIN 1 Z_ CONSTMULT_X Z N N A Z 0 2 This is trivially true but it is instructive to note what VCGEN is doing in constructing the VC itis of the form Z0 FUNCTION lt initial values of all parameters CONSTMULTEXIT Z_0 N EX 2 0 7 0 is the final value of the actual VAR parameter Z note this is the outer 2 This VC states that the result of the procedure call i e the EXIT assertion of CONSTMULT instantiated to the final 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 191 Part 1 lutroductiort to the Stanford Pascal Verifier 5 2 Concepts documentation and verification As next example we will verify a simple greatest common divisor gcd program The concept of the gcd is of course well known and we can base our documentation on the standard mathematical properties by using the following lemmas for non negative x and ged x 0 x gcd x x x ged x y ged y x
36. the reference class D 3 2 3 Axioms for data structure term selection and assignment functions satisfy the following axioms all the free variables are universally quantified A xi Y U lt X Z gt U Z Ax 2 YU X Y Z gt UJ X U 3 lt X Y Z gt Ve 2 4 lt 2 gt 0 XU where Y and U are distinct identifiers 5 Y U X cY Z cU Z Ax 6 Y U3 lt X Z2cU 2 XcU The extension function obeys three axioms 7 DuXuY DuYuX 8 X 4Y 3 DuX cY gt DcY gt 9 XzY lt D cY Z gt uK lt DuXx lt 27 gt Similarly the predicate Pointer To X D obeys the following axioms Ax 10 Pointer To NIL D Ax Il Pointer To X x12 Pointer To X D cY gt E Pointer To X D Ax i 3 Pointer To X DuY Pointer To X D Part Introduction 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 lt A I 1 gt be obtained as follows lt A 1 AU if and only if Y lt A 1 ALT We prove by cases Suppose Then lt A 1 gt from Ax 2 Suppose J l Then from Ax 1 in both cases lt 1 Therefore Vj lt 1 These axioms form a first order theory of data structures
37. 1 This function is recursively defined as f x if x 100 fhen x 10 else f f x 11 It can be shown that this recursive function computes f x if x 100 then x 10 else9 1 Now we want to show that the following program computes the same function 17 Part Introduction to the Stanford Pascal Verifier PASCAL LABEL 1 VAR X V1 P Z INTEGER ENTRY TRU EET TER Z X 10 v lt 101 27 91 YleX 2 ASSERT 27223 IF 1 gt 100 THEN IF NOT Y2 1 THEN BEGIN Yie Y1 10 Y2 Y2 1 GOTO 1 END ELSE Z Y1 10 ELSE BEGIN YieYi ll Y2 Y241 GOTO 1 END END The entry and exit assertions simply state that the program computes the same function as the recursive 9 l function The difficult part is to find a suitable invariant at The key of course is to first understand the operation of the program Each time label 1 is reached the program starts computing f There are two possible cases depending on Y 1 If the initial value of Y 1 gt 100 the program terminates immediately In the other case function f calls itself recursively i e f f Y 141 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 ti
38. 1 lt Ea Ordered L 1 NFER Ordered A 1 I F R O M 1 1 1 4 gt 1 11 JNFER Ordered K I E J LUF R O M J l A L Ordered K J 1 1 Ordered 141 L a 1 1 sE a JNFERKILIsK TU FROM Ordered I JAIsLaL Ma 141 1 A 1 J 1 1 1 I 57 Part Il Chapter 4 The Rule Language Unsimplified Verification Condition INSERTSORT 2 ORDERED 1 J JsN lt N lt 1 1 B lt I A 1 lt PERMUTATION K 11 X 0 lt 1 1 m 2 KL 11 SX K 2 K 1 141 K 1 1 gt ORDERED K 2 1 J lt X lt K_2 Ul 141 A 0 lt 1 1 I 1 J A PERMUTATION K 2 1 11 gt 0 Presimplified Verification Condition INSERTSORT 2 ORDERED K 1 J a lt 1 1 a 8 l n I J A PERHUTAT ION K 17 gt A 2 lt l A KU 1 X a K_2 lt K UJ KU 1 4 ORDERED K_2 1 J a X K 261 A PERMUTATION lt K_2 1 11 gt 0 Simplified Verification Condition INSERTSORT 2 TRUE 58 Part Il Chapter 4 The Rule Language Proof summary for INSERTSORT 2 Assertions made by rules DATA1 2011 1 1 PERM3 lt K_2 1 1 X EXCHANGE 11 gt 1 1 1 Top level goal ORDERED K_2 1 J Proof from backwards rule ORDS Subgoa lt _2 11 Proved without backwards rules Top level goal PERMUTATION K 2 H 13 X gt K Proof from backwar
39. 3 Forward rules Forward rules also express an implication GF but they differ from backward rules in the way they are used in proof searches These rules are written FROM G INFER F Forward rules can be used to derive consequences from a set of known facts Example The inference rule given in 4 1 can be rewritten as GCDAF FROM Y gt J NFER GCD X Y GCD MOD X Y Y y 10 Part 1 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 gt 0 becomes true during a proof 4 4 Differences between 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 INFER The reason for this is that rules not only express logical facts they also contain information for the prover how and when to use those facts Part Il 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 xxy gt 0 if x50 and y gt 0 We could write FROM gt 0 Y gt 0 J NFER XxY gt 0 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 be asserted From x 04 gt 0 we deri
40. AS changes the default PPN to ALIAS prints out the current default PPN 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 for TRUE RESET sets parameters to their default values this command accepts only a list of parameter names as argument Examples SET TRACE PROOFDEPTHE5 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 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 integer greater than or equal to zero bool a LISP flag T or F NIL internally ASSERTDEPTH natnum maximum forward assertion depth CASEDEPTH natnum maximum depth of nesting of forward cases DEPTHTALK
41. 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 INTRODUCTION TO THE STANFORD PASCAL VERIFIER 1 Overview Section 2 gives 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 Il Chapter 1 and this information 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 IJ 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 m
42. C 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 The syntax of the arguments is the same as for SIMPLIFY see below for ex a mples SIMPLIFY commands 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 The command can be abbreviated to S Examples SIMPLIFY simplify all current VCs and display them on the terminal S TRACE PROOFDEPTHS5 simplify all VCs with TRACE turned on and PROOFDEPTH set to 5 SIMPL FOO I SHOWGOAL simplify VC lof FOO and display subgoals during the proof SIMPL TO FILEEXT A FOOJ simplify current VCs and write simplified V Cs onto file FILE EXT A FOOJ SIMPL 2FILE EXT A FOO same as previous example 5 may be used instead of TO SIMPL MAIN COPY TO AAA simplify VCs of MAIN write simplified V Cs onto file AAA and display on terminal The R
43. CONCAT Z CONCAT R T from I SOERIV X CONCAT APPEND 2 1 a ISPROD L R Two rules for verifying a context free parser ISDERIV X Y means there is a derivation from X to Y ISPROD L R means there is a production from L to X 52 Part Il Chapter 4 The Rule Language 4 1 2 Forward rules FROM rules SYNTAX whenever TR I TR 2 from B infer A whenever TR 1 TR 2 from B infer cases CASE I CASE 2 end A the INFER clause a conjunction of literals B the FROM clause a conjunction of iiterals TR i a trigger expression CASE I 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 TRUE There must be at least one case in a CASES clause LOGICAL MEANING BoA B C I 4 D I v C 24 D 2 v 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 literals 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 befor
44. DURE PUSH X T NT SEQUENCE GLOBAL STACK INI TIAL STACK S8 ENTRY TRUE EXIT STACK CONCAT X 50 EXTERNAL This function converts an element into a sequence of one element FUNCTION MAKE SEQUENCE 1 TEM T NT SEQUENCE ENTRY TRUE EXIT TRUE EXTERNAL Main program X INI TIAL SOURCE SOURCEO ENTRY ERROR MSG 1 A EMPTY STACK a EMPTY SOURCE READ a EMPTY SOURCE EXIT ERROR MSG 1 ISDERIV STRT SOURCES BEGIN STRT KIND NONTERHINAL STRT INFO2 START SYMBOL PUSH MAKE SEQUENCE STRT READ SOURCE LOOK INVARIANT ERROR_MSG 1 SOURCE8 CONCAT SOURCE READ CON1 LOOK SOURCE a I SDERIV STRT CONCAT IMBED SOURCE READ STACK WHILE NOT EGF SOURCE 00 BEGIN TOP T IF T KIND TERMINAL THEN IF T INFO1 LOOK THEN ERROR ELSE BEGIN WR 1 TE SOURCE READ LOOK virtual 96 READ SOURCE LOOK END ELSE BEGIN 15 5 R T LOOK PUSH R END END IF NOT EMPTY STACK THEN ERROR END An attempt 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 to TRUE ERROR MSG 1 a EMPTY STACK a EMPTY SOURCE READ A EMPTY SOURCE SOURCE SOURCEO A 32 Part I Introduction to the Stanford Pascal Verifier STRT_3 lt STRT KIND NONTERMINAL STRT 2 STRT 3 INFO2 START SYMBOL STACK 7 PUSH STACK MAKE SEQ
45. E gt 0 BY MOD X Y Y i Rewriting these rules as backward rules leads to the following rulefile which is not sufficient for the proof of all the verification conditions RULEF ILE GCD GCD1 INFER GCO X 6 X GCD2 INFER GCD X X X GCD3 INFER X Y GCD Y X GCD4 INFER GCO X Y GCD MOD X Y Y FROM gt 0 Two verification conditions require commutativity 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 prove a formula that matches the pattern of the INFER clause If we change the rule GCD3 into GCD3 INFER GCD X Y Z FROM GCD Y X Zi we greatly increase the number of possible matches in fact using this modified rule one can verify the gcd program 5 3 A hard invariant 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 In 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 9i function 2
46. EEE Symposium on Foundations of Computer Science 1977 23 C C Nelson and D C Oppen Simplification by cooperating decision procedures Al Memo AIM 31 1 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 25 W Poiak Verification of the in situ permutation program forthcoming IEEE Software Engineering July 1979 26 N Suzuki Verifying programs by algebraic and logical reduction Proceedings of Int l Conf on Reliable Software IEEE Oct 1975 473 481 27 N Suzuki Automatic verification of programs with complex data structures Ph D Thesis Computer Sci Dept Stanford University 1976 76 Appendix A Alternate notation assignment OF t greater or equal 2 or gt implication sign or gt negation history sequence concatenation e or or A 1 Command syntax lt command gt lt imperative_command gt setparm command information command QUIT LISP lt imperative command gt read command print command simp command load command lt dump command gt lt delete command gt setparm command lt alias command gt
47. ESIMPLIFY command takes the last VC returned by the simplifier and has another go at it Sometimes this will have a beneficial effect DUMP commands The group of DUMP commands includes the commands DUMP DUMPVC and DUMPRULE A DUMP command produces a file containing VCs DUMPVC or rules DUMPRULE in 43 Part li 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 The short command DUMP dumps both 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 write a file FOOCVC containing current VCs DUMPVC FOO BAR write a file FOO BAR containing current VCs DUMPVC FOO P PROJ write a file FOO P PRO containing current VCs DUMPRULE write a file FOO CRL containing current rules DUMP FOO write files FOOCVC and FOOCRL containing current VCs and rules respectively If more than one rulefile
48. INTER TO NIL PNT8 FROM POINTER TO X 4 POINTER TO Y A INFER XY 5 Verification 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 include 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 requirements code documentation testing by a topdown method Despite these attempts normal programming activity seems well described by the diagram CONCEPTS PROGRAM COMPILED CODE Y TESTING In designing verifiable programs we advocate a completely different process Again we start out with concepts But before writing any code we develop a formal theory of the concepts involved Often the concepts are already axiomatized e g arithmetic and one can use well known formal theories In 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 ou
49. N complex data type variables are introduced Select ion x y array selection r f record selection Dcq pointer selection Assignment lt x y z gt array assignment r f z record assignment lt D q gt z gt pointer assignment Extension Duq Part Introduction to the Stanford Pascal Verifier The new terms formed by composition of these new functions must obey the Pascal type compatibility requirements Thus is legal only if x is of array type and y is of the correct index type Similarly lt x cy gt z gt is legal only if x is of type reference class and x y z have compatible types To do this the new functions have types The type of x y is the type of elements of the array term x The type of x yJz is the same as that of x If the type of x is reference class of T the type of xcy is T The type of lt x cy gt z gt 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 1 ail Pascal variables 2 ail terms obtained from i 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
50. NCHECK veg 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 expects only to find two numbers N OT a boolean etc INVALID CONSTRUCTOR OR SELECTOR FOR UNION TYPE Union 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 JNVALID SUBRANGE ITEM 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 in 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 of type R EA L or a subset of
51. Pascal structured types A RRAY RECORD and POINTER For example a data structure term of the form lt A I E gt denotes the array obtained from A by placing E in the ith position lt A I E gt J denotes the jth element of lt I E gt We have similar terms denoting assignments to dereferenced pointers For each pointer type declaration TYPE T 1TO the verifier introduces a reference class called TO of all elements of type TO Pointers of type T are related to TO just as array indices are related to arrays Example The reference class resulting from Xf E is denoted by the term lt T0 cX gt E gt 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 Reference class identifiers We introduce new individual variables called reference class identifiers into the assertion language They have the form s 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 to be reference class of T 3 2 2Functionsand predicates on data structures New function symbols corresponding to the Pascal selection assignment and new operations O
52. RCE A SOURCE SOURCE_READ 5 1 T E M PART II i DIFFERENCES FROM STANDARD PASCAL The verifier accepts most of the constructs of Pascal modified in some cases for assisting verification What follows is a list of the known differences between the language accepted by the verifier and standard Pascal as presented in Jensen and Wirth 15 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 4 signs Thus comments may be added to code in this manner 1 2 Program files 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 13 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 PROCEDURE P VAR X INTEGER Y REAL GLOBAL A VAR Z XHere the global Z may be changed by this procedure the global A may be referenced by this procedure INITIAL 0 7 20 ZXO and YO may appear only in assertions ENTRY EXIT MUMBLE X X0 Y a BUMBLE A Z0 Functions may not have an INITIAL statement 35 Part li
53. Stanford Verification Group March 1979 Report No 11 Edition 1 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 March 1979 Report No 11 Edition 1 Computer Science Department Report No STAN X 79 73 1 STANFORD PASCAL VERIFIER USER MANUAL by STANFORD VERIFICATION GROUP D C LUCKHAM S M GERMAN F W v HENKE R A KARP P W MILNE D C OPPEN POLAK W L SCHERLIS 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 T he views and conclusions contained in this document are those of the authors and should not be interpreted as necessarily representing the officia policies ether expressed or implied of Stanford U niversity or any agency of theU S Government P W Milne is employed by CSIRO Division of Computing Research P O Box 1800 Canberra City ACT 2601 Australia CONTENTS PART I 5 Foreword Overview The Verifier 21 VCG 2 2 The theorem prover The Assertion Language 3 1 Kinds of assertion statements 3 2 Data structure terms The Rule Language 4 1 Backward rules 4 2 Replacement rules 4 3 Forward rules 4 4 Differences between rules 4 5 Rules for data structure terms
54. TITY NOT OF TYPE RECORD Following an entity the notation lt identifier gt 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 identifierl c identifier2 gt was found The entity identifierl was not the name of a reference class known by the parser You need to declare a type that is a f identifier 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 Appendix 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
55. The following Iwo rules are equivalent CS 1 FROM INFER CASES Qi x y Q2 x y END CS2 FROM P x INFER CASES Qi x y Q2 x z END 4 2 12 Semantic matching Suppose we had a rule 1 INFER 1 FROM P x A Q x If we wanted this rule to apply in proving P 2 A from P At 1 and 1 the pattern matcher would need to have some knowledge of properties of addition We eallthis type of matching Semantic Matching The matcher used in the rulehandler makes use of properties of addition multiplication arithmetic relations and equality The matcher assumes that all variables 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 assumption makes X20 and Xt 1 gt 0 equivalent In fact the prover stores all inequalities of given sign internally in the form E20 for some expression E This means that the pattern gt will match A B lt F C G D binding x to C and y to A B G D 1 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 Thus the rule 71 Part Il Chapter 4 Th
56. The printout may tell you the type ex pected 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 cont
57. 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 L 2 A I AU CJ 2 gt gt K 2 is a theorem of this theory By axiom 2 Kel lt lt 1 J 2 gt gt IK B2IXL A QJ AUT J 22 UTE Axiom implies A 1 JJ 222 IDXL A CJ 2111 and finally L lt CJ 2211 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 type TO 1T Terecord Next 70 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 3j Reachstep D x y j Reachstep D x y 0 df x y Reachstep D x y j 1 g 32 Reachstep D z j a Dez gt Nextey 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 semantic
58. UENCE STRT 2 SOURCE READ A STACK 7 MAKE SEQUENCE STRT 2 SOURCE 4 READ FF SOURCE COOK LOOK 4 READ X X SOURCEB LOOK LOOK 4 F IRST SDURCEO SOURCE 4 REST SOURCEO A EMPTY SOURCE 31 A SOURCEB APPEND SOURCE READ 2 LOOK 31 A ISDERIV STRT_2 CONCAT IMBED SOURCE_READ_2 STACK 61 A EMPTY STACK 61 E ISDERI V STRT 2 IMBED SOURCE One way to prove this formula is to show that imbed source0 concat imbed source read 2 stack 6 Given that source 3 and stack 6 are both empty this means showing imbed ap pend source read 2 look_3 imbed source read 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 loop 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 look 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 Main program INI TIAL SOURCE SQURCEE ENTRY ERROR MSG 1 STACK EMPTY SOURCE READ SOURCE EX I T ERROR MSG
59. UMAUX INFER INST x Since INST 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 proverto 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 restric
60. 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 tis yx 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 rulehandler 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 rule
61. Y CONCAT X CONI U V 1 CON3 REPLACE CONI X NULL SEQUENCE BY MAKE SEQUENCE X CON4 REPLACE CONCAT X NULL SEQUENCE BY X CON5 REPLACE CONCAT NULL SEQUENCE X 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 Introduction to the Stanford Pascal Verifier PASCAL TYPE TOKEN EMPT IOENT NUMBER PLUS SYMBOL AND HANY MORE NONTERM START SYMBOL AND 50 MORE TOKEN SEQUENCE FILE OF TOKEN TERM OR NOT NONTERMINAL TERMINAL TEM RECORD KIND TERM OR NOT 01 TOKEN NF02 NONTERM END T NT SEQUENCE FILE OF ITEM VAR SOURCE SOURCE READ TOKEN SEQUENCE R STACK T NT SEQUENCE STRT T ITEM LOOK TOKEN DONE BOOLEAN PROCEDURE ERROR ENTRY TRUE EXIT ERROR_MSG 1 EXTERNAL PROCEDURE ISRHS VARR T NT SEQUENCE T ITEM L TOKEN ENTRY TRUE EXIT ISPROD T R EXTERNAL Procedures implementing a stack X FUNCTION EMPTY ST T NT SEQUENCE BOOLEAN ENTRY TRUE EXIT TRUE EXTERNAL Return the of the parsing stack this element PROCEDURE TOP VAR X ITEM GLOBAL STACK INITIAL 5 50 ENTRY TRUE EXIT EMPTY 50 2S0 CONI1 X STACK a EMPTY 50 gt ERROR HSG 1 EXTERNAL Part Introduction to the Stanford Pascal Verifier Push x on the parsing stack note that we push whole sequences rather than single elements PROCE
62. 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 MUL2 WHENEVER xxy FROM x20 A gt 0 INFER xxy20 says that whenever a product appears in the data base an instantiated version of MUL2 will appear MUL2A FROM A20 A B20 INFER gt 0 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 Thus 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 prove A20 A B20 gt A 1 xB20 while MULI would not While they have different heuristic meanings logically MUL2 and MULI express the same fact One v amp y common application of WHENEVER is asserting equalities between terms For example GCDI WHENEVER GCD x y FROM x MOD y 0 INFER GCD x y y Another way of writing this rule is d GCD2 REPLACE GCD x y WHERE x MOD y 0 BY y This rule is seman
63. aining more condition variables concurrent version only 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 may be referenced within functions without appearing in a GLOBAL statement indeed this statement is prohibited within functions See the next error for further
64. als in the rule 4 2 7 Introduction to matching Logically rules are universally quantified statements with quantification over all variables which appear Thus the rule 1 FROM INFER R x represents the logical statement Vx P x AQ x gt R x 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 Q B A Q C a A B gt R B The first literal asserted to the data base is P A At this point MI fires and waits for to be asserted One way of viewing this is that a new rule 65 Part li Chapter 4 The Rule Language MIA FROM INFER 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 Q A is fully instantiated in resolution terminology it isa ground literal This means we can TEST its validity directly rather than merely waiting for instances Thus if we had a forward rule M2 FROM TRUE INFER Q x this rule would apply during the test of Q A and MIA would assert R A Had the literals in M l 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 ba
65. an be expected to prove a large variety of valid verification conditions involving Ordered Suppose we wish to express the following fact about Ordered x VA 4 j Ordered A i 1 j a i lt j a AUISA i 1 gt Ordered A i j That is if the array A is ordered in it 1 j and Afi is not greater than the smallest element of A in the interval namely A i then A is ordered in i j It would be nice if we only had to provide logical statements like x and proofs of valid verification conditions were forthcoming However the theorem prover does not have much 60 Part II Chapter 4 The Rule Language 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 app
66. an recognize which paths are in the VC by the values of loop and conditional tests and assertions appearing in the VC Unsimplified Verification Condition CONSTMULT 1 O YxO X 0 YxZ 8 A 2 80xN _ This VC is of the form INVARIANT O Y 0 a INVARIANT X_0 Y Z_0 a LOOPTEST Z_0 N EXIT X_0 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 X Z 0 this requires O Yx0 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 VCGEN has given these final values the new names 0 and 2 0 Part I Introduction to the Stanford Pascal Verifier Unsimplified Verification Condition CONSTMULT 2 7 Z N 7 1 This VC is of the form INVARIANT X Y Z ALOOPTEST Z N s INVARIANT X Y Y Z 1 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 may be expressed by a rule as follows RULEF ILE DISTRIBUTIVITY DIST REPLACE Ax B4C BY AxB AxC It should be emphasized that such arithmetical rules can sometimes lead the prover into deducing many irrelevant facts for this rule to have the desired effect the verifier parameter SUMMATCH must be turned on
67. applications as an aid to programming and to have 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 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 manual The manual is divided into two parts 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 is an introduction to the verifier Jt contains a short survey of its features and components and examples of its use The reader who has completed Part 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 is a manual for those users who embark upon serious exper
68. are T ESTed during proof if this switch is set see Section 4 2 7 56 Part Il Chapter 4 The Rule Language 4 1 6 Anexample Here is a sample rulefile and two proofs which make use of it The ruiefile is not particularly efficient though it does demonstrate severai features of the rule language The verification conditions come from an insertion sort program The TRACE TRACEFACT and TRACEVC switches have been set It took three seconds to prove INSERTSORT 2 and seven seconds to prove INSERTSORT 3 If only the rules ORD3 and ORD9 are included proof of INSERTSORT 3 takes only two seconds RULEFILE INSERT Rulefile for insertion sort PERM1 PERM2 PERM3 1 DATA2 ORD1 ORD2 OROS ORD4 ORDS 0806 OR07 ORD8 ORDS ARR INFER Permutation I 1 INFER Permutation Exchange 1 J B FROM Permutation A B REPLACE P1 P2 P1 P3 P3 BY Exchange P1 P21 P4 P2 P3 REPLACE A D X tK WHERE K J BY X REPLACE lt A J AtJJ gt BY A INFER Ordered K 1 J FROM 2J INFER Ordered K 1 J FROM Ordered K J L aOrdered K L J Ordered K 1 J F R O M Ordered K A Lsl A JM NFER Ordered K LJ E 1 L FROM l J Esk E41 4 Ordered INFER Ordered A EIDJ ACE 11 1 J FROM i lt lal lt Ja Ordered J J NFER Orderec lt A 1 AlI l gt 1 J FROM I JaOrdered A 1 J lt gt 1 J L a K L
69. 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 are not equivalent for this reason These rules are logically equivalent but not 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 1 infer from P x a Q y N2 infer N x y from S x y N3 infer from N y x infer from N C x C y The easier non recursive rules appear first When trying to prove N A B non N subgoals 64 Part Chapter 4 The Rule Language would be tried in the following order assuming none were provable P A S A B P B 5 P C B 5 P C A S C A C B and so on Q x is never tried since the P x case always fails rule N3 will not loop forever When 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 again setting up the goal N A B But setting up a goal means denying a fact to the data
70. athematical 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 examples of verification experiments are given in the references at the end of Part Il 2 The Verifier The verifier employs the inductive assertion method due to Floyd 7 for reasoning about programs Floyd s method was developed into a logic of programs by Hoare 11 and others 3 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 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 Ifa VC is incorrect this may reveal a bug in the program or insufficient documentation at some point A modification is made to the inpu
71. c formula 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 Il Chapter 4 The Rule Language 4 1 1 Backward rules SYNTAX infer A from whenever TR 1 TR 2 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 BoA 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 techniques If A is the propositional constant FALSE a contradiction will be derived if the FROM clause can be proved Triggers in the WHENEVER clause restrict situations in which the rule will be applied to those in which instances of each trigger have occurred as subterms Proof of the literals in the FROM clause proceeds from left to right EXAMPLES infer A div lt from AsNa B21 infer Ordered a i f ro m Ordered a i k Ordered a k j infer ISDERIV X MAKE_SEQUENCE X infer ISDERIV X
72. ction 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 Three external procedures 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 error 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 xe TUNT and converts it into lt x gt e TuNT 5 8 4 Specifications As might be obvious by now we cannot prove that the parser will accept every legal input string because we have not made strong enough assumptions about isr s Instead we will prove the following statement if the parser terminates and does not issue an error message then the input string 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 reliability and correctness With a suitable implementation of isrhs the parser will reliably parse any legal input string an implementation of the procedure error can guarantee a reasonable recovery from syntax errors thus making the program robust In the case Where the parser terminates without an error m
73. cutable statements The history sequence operator e is prohibited record fields indicated by a period may not a parameter list following the fieldname These restrictions have the effect of prohibiting module history sequence statements lt number gt is an unsigned constant lt string gt is a character string lt identifier gt is a sequence of letters and digits starting with a letter Appendix B Parser Error Messages B 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 iscorrect 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
74. der rules appear in the file Is more or less the order in which they will be applied by the theorem prover EXAMPLE rulefile sample constant NULL EMPTY CONSTI CONST2 Declare various identifiers to be pattern constants CONST from TRUE infer CONSTI 4 CONST2 Assert that CONSTI CONST2 to the data base X NEQ infer X580 fro m X 0A X28 Rules like this may be required sometimes X APNULL e APPEND NULL X by X NULL is a constant X GINFO replace G X where X INFO EMPTY by NULL INFO is a record field identifier and therefore not a pattern variable X 55 Part Il Chapter 4 The Rule Language 4 1 5 Switches and 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 The SHOW switches are particularly useful for debugging ruiefiies In the default case ail trace switches are off The SHOW command see Section 2 3 can be used to determine the default settings of the depth bounds DEPTHTA LK switch Jf this switch is set to true the prover will print a message whenever it reaches a depth bound during search PROOFDEPTH integer This value is approximately the maximum depth of nesting of backward rules A SSERTDEPTH integer This value is approximately the maximum depth of nesting of assertions made by forward rules CASEDEPTH integer
75. dn 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 s base type c identifier gt 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 e identifieri c identifier2 gt or some qualified form equivalent to this Either identifier2 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 GOTO statement If you need unlimited branching you will have to create your control structure entirely with GOTO 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 w
76. ds rule PERI2 End of proof summary for INSERTSORT 2 Unsimplified Verification Condition INSERTSORT 3 ORDERED K 1 J lt N A X lt K 1 1 A B l A I lt J A PERMUTATION lt K 1 X gt K A 0 1 1 3 K E 11 X gt 1 lt 1 141 X gt ORDERED K 1 1 J 1 1 1 lt 1 A 2sJ 1 PERMUTATION K_1 K Presimplified Verification Condition INSERTSORT 3 ORDERED K 1 J a JsN A X K 141 A lt l A I lt J A PERMUTATION K 13 X K8 A 251 A 11 lt 1 lt 11 gt 59 Part Il Chapter 4 The Rule Language ORDERED K_1 1 J Simplified Verification Condition INSERTSORT 3 TRUE Proof summary for INSERTSORT 3 Top level goal ORDERED K 1 1 J Proof from backwards rule ORDS Subproofs Subgoal ORDERED 141 J Proof from backwards rule ORD3 Subgoal ORDERED K 1 1 1 Proof from backuarde rule 0803 End of proof summary for INSERTSORT 3 4 2 Using the rule language In this section we describe techniques for writing rules The primary purpose of the rule 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 intervalli j By giving suitable rules Ordered can be used in assertions in programs and the theorem prover c
77. e Rule Language EQI INFER xey FROM will prove P B A 2A 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 2 Q B with the rule tl FROM INFER 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 AxB aA F C gt Q B C will not be proved by Q2 FROM P xxF y INFER Q x y while A F C a P AxB 2 will This limitation is not a serious one in practice and may be circumvented by using a WHENEVER clause as in Q3 WHENEVER F y FROM xxF y INFER Q x y 4 2 13 Subspace matching When matching a pattern like x y 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 matching x y against A B C produces the specification x y A B C which 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 Thus P x y x y will match P A A 4xB binding x to A 2xB and y to 2 P x y x y and P A A 3xB wilt not match however because x and y are considered to b
78. e and Larsen A standard basis for automatic verification of sorting algorithms forthcoming Al Memo Stanford Artificial Intelligence Laboratory Stanford University D A Fisher Copying cyclic list structures in linear time using bounded workspace CACM V01 18 5 May 1975 251 252 W Floyd Assigning meanings to programs Proc Symp Appl Math Amer Math Soc Vol 19 1967 19 32 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 1978 105 1 18 S M German D C Luckham and D C Oppen Proving the absence of common runtime errors forthcoming A Memo Stanford Artificial Intelligence Laboratory Stanford University 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 A R Hoare An axiomatic basis for computer programming CACM Vol 12 10 Oct 1969 576 580 583 C A R Hoare Proof of a program FIND CACM Vol 14 1 Jan 1971 39 45 Hoare and Wirth An axiomatic definition of the programming language PASCA L Acta Informatica Vol 2 1973 335 355 14 S Igarashi R L London and D C Luckham Automatic program verification 1 Logical basis and its implementation Acta informatica Vol 4 1975 145 182 75 References 15 Jensen
79. e integer variables Subspace matching is a powerful facility but it is not desirable in certain instances Consider the rule DIST REPLACE a b xc B Y axct bxc Since a and b will be part of a subspace specification the BY clause will not be instantiated severely limiting applicability of the rule For this reason a facility has been provided which allows extra specific instances to be generated by the matcher in addition to the 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 AP 3 a P B a P C gt P CtB 72 Part Il Chapter 4 The Rule Language with the rule SUMP INFER P x y FROM 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 could somehow guarantee that P x would be instantiated we would not have this problem One way to do this is to invent a new predicate which does not appear in the theorems to be proved Suppose we replaced SUMP by SUMP2 INFER P x y FROM INST x A P x a P y S
80. e the split is actually done when Its C I formula the formula 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 from P S infer Q X Y S WhenP S is true Q X Y Sl is false for all X and Y whenever from A204 B20 infer AxB20 whenever X Y from Y infer X Yx X Y whenever MIN 1 J K from TRUE infer cases IsJalsK oli JslAJsK 5 end MIN I J K l if IsJ and 1 lt 53 Part II Chapter 4 The Rule Language 4 1 3 Forward rules REPLACE rules SYNTAX replace TR where Al by RP replace TR where by cases C i RP 1 C 2 RP 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 The 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 gt R amp R P A gt C 1 TR RP 1 v C 2 TR RP 2 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 equality 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 fo
81. ed 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 z exists in the data base If it finds an instance say where z 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 and Replace Suppose we desired to assert xxy20 whenever we saw a product and it was evident that x20 and y20 We could write FROM x20 A y20 INFER 0 Consider the effect of this rule Whenever an assertion is made in the data base of the form E20 67 Part 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 E20 and F20 possibly of course the rule will fire asserting ExF20 This adds
82. ements into rules without regard to efficiency can lead to prolonged and wasteful searches 4 2 15 A note on multiplication 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 ixx BY x REPLACE Oxx BY 0 REPLACE fxx BY x REPLACE 2xx BY x x and so on This means that without rules the formula 0 gt P 0 will not simplify while the formula x 0 a P xxy gt P 0 will simplify This unfortunate weakness can often be circumvented partially by adding rules of the sort REPLACE xxy WHERE x l BY y REPLACE xxy WHERE x 2 BY xxy and so on where necessary 74 REFE 1 21 3 415 5 6 7 81 101 11 121 13 RENCES A V A ho J D Ullman The Theory of Parsing Translation and Compiling Vol Pren tice H all Inc Englewood Cliffs 1972 W W Biedsoe Splitting and reduction heuristics in automatic theorem proving Artificial Intelligence Vol 2 1971 55 77 Cartwright and D C Oppen Unrestricted procedure calls in Hoare s logic Proceedings of the Fifth ACM Symposium on Principles of Programming Languages ACM New York 1978 A Cook Axiomatic and interpretive semantics for an Algol fragment Technical Report 79 University of Toronto 1975 R L Drysdal
83. er 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 variables 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 M essages INTERNAL ERROR IN VCG OR RU
84. er appears the system expects more input before It can execute the command for example the terminating 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 DESCRIPTION OF THE SIMPLIFIER 3 1 Introduction The prover has two components a simplifier and a rulehandler which is described in Part Il 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 lt 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 fist structure and the booleans TRUE and FALSE The simplifier is complete that is it simplifies every valid formula to TRUE Thus it is also a decision procedure for the quantifier free theory of reals arrays records and list st
85. er to wait for an instance of CONS y z to become equivalent to A If such an 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 Forward cases In order to increase efficiency of proofs a case elimination mechanism has been built into the forward CASES construct Let A I E represent the array A after the assignment A I E has been performed Thus we have lt 1 gt 1 and jo lt alile gt jl alj This fact can be written as a REPLACE rule ARRAY REPLACE lt a ile gt j BY CASES i jalj END This rule is equivalent to ARRAY 1 WHENEVER a ije j FROM TRUE INFER CASES i j 2 lt aliJe gt jl e izj gt lt alile gt jlealj END Interpret the arrow in the CASES clause as AND Suppose we wish to prove lt A BAUJA The rule splits and considers two cases lt lt 14 A lt A TAM JJ Al Both cases simplify to FALSE proving the theorem In this example the case split is required for proof Suppose however we were proving B 1 2 2 35 17 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 pro
86. essage the program proof will guarantee a correct parsing of the input regardless of the actual implementations of error and isrhs In writing the assertions for this program we use the following functions imbed maps a sequence over T into a sequence over TUNT concat concatenates two sequences append appends a single element to a sequence conl 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 11 177 To be able to formulate the invariant we include a virtual variable source_read which at any point contains the portion of the input read so far 29 Part Introduction 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 concat coni imbed make sequence The rules ISDI and ISD formulate the two lemmas for isderiv mentioned above The rules IMBI through IM B6 express that imbed distributes over make sequence conl etc IMB and IM B8 define imbed for
87. eters 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 was 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 EXPECTED 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 block RECORD FIELD MODIFIES EN
88. example is documented by standard sorting concepts Each concept has a simple first order definition except permutation see 12 26 For example ORDERED A L means array is ordered in the range IL ordered a 1 r df Vi si A i r AU s AU 01 PA RTITION A L 1 R means that each element of A in EL I is smaller than each element of A IN It I RJ partition a l i v df Vj k Ixj i isksr lt AU Rules defining sorting concepts including permutation are given in 5 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 5 ORDGa INFER ORDERED lt A IP X gt L R FROM ORDERED A L R A L P A P R XsAIP 1 gt 1 ORD6a states conditions under which the array obtained from A by placing X in A P 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 5 rules for the theory of data structures are also needed 23 Part 1 Introduction to the Stanford Pascal Verifier PASCAL VAR N INTEGER PROCEDURE DUMMY EXIT TRUE TYPE NARRAY ARRAY El N OF INTEGER PROCEDURE SORT WAR A NARRAY GLOBAL N INI TIAL A A0 ENTRY N21 EXIT
89. 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 dump 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 loads the file FOOCVC LOAD FOOCVC does exactly the same LOADVC loads the file VERIFY CVC LOAD FOO loads whichever or all of the files FOOCVC and FOO CRL exist DELETE commands Rulefiles and rules can be deleted selectively by the commands DELRFILE ist of rulefites gt for rulefiles and DELRULE list of rule names for rules The command DELRFILE without argument deletes all rules so beware 44 Part Il Chapter 2 User Commands 2 2 Set ting 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 ALI
90. 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 1 Appendix B Parser Error Messages BASE TYPE FOR POINTER NOT DEFINED an assertion within a Pascal program you used the notation identifier 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 coul
91. following lemmas are immediate maxof al 1 1 4 1 lt maxof x 0 141 maxof x a 1 r 1 gt maxoflalr 1 a l r 1 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 to The full input submitted to the verifier for this problem is given below Pascal Plus permits arrays in inner blocks to be dimensioned using VAR variables and this is the reason for the enclosing procedure DUMMY Note and e are both accepted as notation for assignment RULEF ILE MAX MI INFER MAXOF A 13 4 1 1 1 H2 INFER MAXOF 1 1 FROM 1 gt 22 1 lt A 1 1 1 M3 INFER MAXOF ATI A 1 1 FROM 1 gt 2 1 gt a MAXOF 1 1 1 PASCAL VAR INTEGER EX T TRUE DUMMY TYPE NARRAY ARRAY El N10F INTEGER FUNCTION A NARRAY INTEGER GLOBAL N ENTRY N 8 EXIT MAXOF 1 VAR TEMP 1 INTEGER BEGIN TEMP A 1 FOR 1 2 to N INVARIANT MAXOF TEMP A 1 1 1 0 IF A T 3 TEMP THEN TEMP eA CT TEMP 21 Part 1 Introduction to the Stanford Pascal Verifier END BEGIN END It is instructive to look at the unsimplif
92. gt EM array type ARRAY S SHE e idi OF lt Pascal lt limited simple type7 lt identifier gt lt identifier gt 3 lt signed number gt L i gned number signed number lt number gt A 16 Verifier Syntax type gt gt Appendix A Verifier Syntax record type RECORD Tp Pascal END 17 lt uni on type UNION c identifier r sca type END lt pointer type gt xidentifier filetype FILE 0 F lt file Pascal type filePascal type is the same as Pascal type except it does not contain pointer tupe Appendix A Verifier Syntax A 2 10 Executable statements compound ta i gt lt number gt gt 3 J 1 statement END APA lt ES express on 17 gt PASSIVE 4 identifier L BEGIN compound tai I gt rs IF expression THEN statement G ELSE EO ee GO TO nunmber GOTO ASSERT a express ion COMMENT ASSUME NEW lt var tables WITH aps 00 statement INVARIANT lt expression WHILE expression 00 lt statement gt for statement repeat statement READ identifier identifier
93. handler 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 11 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 lt 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 2 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 how 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 r les is in Part Il Chapter 4 Part 1 Introduction to t
94. he Stanford Pascal Verifier 3 The Assertion Language 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 11 12 14 The assertion language of the Stanford verifier permits logical statements within the quantifier free first order theories of arithmetic Arrays Records and Pointers ie 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 b
95. hings 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 name for some reason or 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 M essages IDENTIFIER DECLARED MULTIPLY INONE 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 aft
96. ied verification conditions At this stage the properties of maxof declared in the rulefile have not been applied Unsimplified Verification Condition MAX 1 O N 2 lt gt 13 A 1 2 1 HAXOF TEMP 0 1 N 1 1 MAXOF TEMP_ A 1 N Unsimplified Verification Condition MAX 2 B N A N 2 A 1 A 1 N Unsimplified Verification Conditionr MAX 3 I lt N A 2si TEMP A 1 1 1 TEMP A 11 MAXOF 11 1 1 1 1 Unsimplified Verification Condition MAX 4 IsN A 2sl A MAXOF TEHP A 1 1 1 TEMP A I1 MAXOF 1 1 1 1 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 loop A exit FOR loop 22 Part 1 Introduction to the Starrford Pascal Verifier EXIT 0 is the final value of TEMP on leaving the loop 2 corresponds to the path ENTRY bypass FOR loop EXIT MAX 3 and MAX 4 correspond to the two different paths around the loop In practice the initial rulefile is usually inadequate for the proof of all 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 aliVCs are proved 5 5 Specifications for sorting This Bubble sort
97. ilowlng two FROM rules whenever TR from A infer TR RP whenever TR from A infer cases TR RP 1 C 2 29 TR RP 2 end EXAMPLES replace X DIV 1 by X Division by 1 replace b y BxA Commutativity of multiplication This rule will not loop X replace lt A 1 E gt J by cases 1 I amp JoAtJlend Array data structure term simplification X replace SIGN X by cases X20521 X 85 lend Will causea split if neither X20 nor X 8 can be shown X 54 Part Il Chapter 4 The Rule Language 4 1 4 Rulef iles SYNTAX RULEFILE name constant CS 1 CS 2 pattern PT 2 3 RN I RULE I RN 2 RULE 2 RULE i a rule 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 record field identifiers These defaults can be overridden using the CONSTANT and 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 or
98. iments 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 sections The first describes the rule language and how to express mathematical facts as rules the second section gets into the intricacies of writing rules and why rules written one way may lead the verifier into much more efficient proof searches than if they are written another way Section should be enough for many simple examples 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
99. ist 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 Appendix 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 Caused by forgetting to set _ to ERROR IN C_D_U CASE 2 Caused by forgetting to set _to NIL ERROR IN C_D_U THIRD TYPE Now you ve really done It You were warned NOT to use the CONCURRENT Dynamic Underbar 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 allo
100. ith 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 CLASS NAME INCORRECTLY QUALIFIED OR USED A class name 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 TY 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 l
101. l 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 3 Part Il Chapter 1 Differences from Standard Pascal 1 9 Global variables Any global variable that can be changed in a procedure must appear in aGLOBAL statement for that procedure a list preceded by VAR Any global variable that can be referenced in 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 global 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 and Passive statements The word VIRTUAL may precede the word VAR In a declaration or a procedure or function parameter definition In addition the word VIRTUAL may proceed a non VAR parameter definition VIRTUAL entities may appear in documentation ENTRY EXIT ASSERT COMMENT ASSUME PASSIVE or they may be passed to other virtual entities They may no
102. laration has the form PROCEDURE p U VAR V GLOBAL C VAR H INITIAL 0 ENTRY I U G V H EXIT O U G V H X0 BEGIN body END where U 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 XOis 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 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 be changed the body and U variables that remain constant New variables 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 b
103. lication 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 way can be expressed to the theorem prover R 1 INFER Ordered A i j FROM lt Ordered A it LA AUSA 1 1 This has the effect of saying If you are trying to prove that A is ordered in i j for any A and j then first prove that i lt j then Ordered A it 1 j and finally AliJ lt sA i 1 Here is another way of expressing x R2 FROM Ordered A it i lt j AliJsAli 1 INFER Ordered A i j That is for any A and j if you know that Ordered A it 1 j i j and 1 lt 1 1 are all true then you can assert Ordered A i j An equivalent way of writing R2 is R2A FROM Ordered A i j isj Ali 1 sA i INFER Ordered A i 1 f Rules like R 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 Il Chapter 4 The Ruie Language 4 2 2 The the
104. me all remaining outer calls will take the Y 12100 branch Then each time Y will be decreased by 10 and Z will become Y i 10xY2 Since this case Z has to be 91 we propose the invariant Y 1 10 2 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 label in a situation where 2 1 and Y 1 lt 101 1 this case the loop will take the Y 1 lt 100 branch and new recursive calls have to be evaluated Thus the invariant will only be Y 1 10xY2 92 This is still insufficient but the remaining details are fairly easy to find First we have to take care 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 2 gt 0 Altogether we get the invariant gt 100 1 Y1 X V X 101 Y1 10xY2 92 2 gt 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 Part Introduction to the Stanford Pascal Verifier r verify Hi there welcome to the Pascal Version VCG 4 SIMP 24 October 4 HELP for help read itf9l ver Reading file ITF91 PAS VER SYNTAX SCAN COMPLETE PROGRAM PARSED CPU SECONDS 0 383 gt printve gt Unsimplified Verification Condition MAIN
105. nce class after the operation YT CAR 2 which changes one of the ceils in CELL namely the one pointed to by Y So the relationship between them is CELL CELL CELLcY CAR 2 gt gt The assignment of the value of X to Y makes this equivalent to the form that appears in the VC The VC is proved using rules for reference classes given in Section 4 5 5 7 Verification 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 sorting operations on arrays List operations are defined in terms of operations on reference classes The procedure INSERT in the example below inserts a new word into a oopfree list To prove that INSERT preserves loopfreeness we use the Reach concept introduced 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 Dex gt Next DeDcex Next Next 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 Stanford Pascal Verifier PASCAL TYPE REF WORD WORD RECORD COUNT INTEGER NEXT REF END PROCEDURE INSERT ROOT Y SENTINEL REF GLOBAL ENTRY REACH 4WORD Y n REACH UMORD Y SENTINEL
106. nction itis 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 in the path MISSING ITEM IN LOADSYMBOLS INVOCATION The LOA DSYMBOLS command contains two parameters The first is the name of the 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 IDENTIFERIN INVALID CONTEXT Contrary to the usual scope rules once an entity is defined to be a TYPE MODULE or SCHEDULER identifier it may not be redefined as a TYPE MODULE or SCHEDULER 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 called only with exactly as many param
107. om 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 rules triggered by A or B will fire once 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 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 is asserted to the data base obtaining which is false The other case AC 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
108. onverts them into values of the union type 39 Part ii Chapter 1 Differences from Standard Pascal ASSIGNMENTS Use ul u ai valid only if TA 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 TYPE TAGS LISP 0 OTPR RECORD CAR LISP CDR LISP END ATOM RECORD VALUE LISP PLIST LISP END U UNION D INTEGER END PROCEDURE CONS X Y LISP VAR RESULT LISP GLOBAL VAR AU E RESULT D a RESULTT O CAR amp X a RESULT D VAR CELL DTPR BEGIN NEW RESULT CELL CAR X CELL CDR Y RESULT U 0 CELL END FUNCTION CAR X LISP LISP GLOBAL 40 ENTRY TAG Xf D EXIT TRUE BEGIN CAR X D CAR END 40 Part Chapter I Differences from Standard Pascal PROCEOURE PLUS X Y LISP VAR RESULT LISP GLOBAL VAR ZU
109. orem 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 Il Chapter 3 The prover tries to prove theorems by deriving contradictions in a data base Thus if we are trying to prove gt C it asserts A and 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 prove x y gt f x f y We first assert xy Then we assert the negation of the conclusion f x f y 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 and fes f 9 For eac 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 T RUE propositionally The fourth assigning TRUE to x and FALSE to resulted in a contradiction eliminating that case from
110. orward rules may be applied resulting in proof of the literal in the given data base 4 2 8 Ordering within rules Suppose we want to prove A gt 0a P A 1 gt Q A 1 and we know x x gt 0 A px 4050 There are two ways we could write forward rules to express this fact 66 Part Il Chapter 4 The Rule Language AR 1 FROM x 04 P x INFER Q x AR2 FROM P x a gt 0 INFER Q x Consider using AR When gt 0 is asserted AR fires and creates a virtual instantiated rule AR 1 FROM P A INFER 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 1 is asserted the rule instantiates to AR2A FROM A 150 INFER Q A 1 Testing A 150 succeeds since A 0 is in the data base and thus is known to the built in Presburger arithmetic prover Therefore 1 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 ORD3 INFER Ordered a x y FROM x y a Ordered a x z a Ordered a z y ORD4 INFER Ordered a x y FROM x y a Ordered a z y a Ordered a x z Consider using ORD3 to prove say Ordered B I J The first subgoal is I lt which is fully instantiat
111. pagated As soon as only one case remains its facts are asserted immediately In our example the rule ARRAY first applies with a B 112 i 2 6 3 j 1 The first case with i j or 2 1 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 1125 2 3 1 42 A 241 A lt lt 1 2 gt 2 3 gt 1 lt 1 2 gt 1 At this point the rule applies again with 1 2 1 The second case is eliminated by test and the fact lt B 1 2 gt 1 lt 2 is propagated causing an immediate contradiction 70 Part 1 Chapter 4 The Rule Latrguage T hus forward CASES generally cause splitting only when a split is necessary or further splits are required to eliminate cases Forward splits will not occur however within the proof of a subgoal for a backwards rule though case elimination may 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 CAS FROM P INFER CASES Qi 2 Rl 02 R2 Q3 R3 END is equivalent to the set of rules CAS I FROM P A Q2 A INFER QUA RI CAS2 FROM QiA Q2 A R2 CAS3 FROM P A QiA Q2 INFER Q3 A R3 assuming it never splits If any of the Qi or Ri are not fully instantiated when the split is propagated further instantiations will occur only within each case not across cases
112. r 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 theory to justify a particular piece of code Additionally some program statements 0 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 Part I Introduction to the Stanford Pascal Verifier associated invariant The final product will be a program documented by precise formal statements In parallel with writing the program the axiomatic theory defining the programming concepts must be expressed 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 wrong program or 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
113. ructure under the above functions and predicates The following are some examples of simplifications 2 3x5 17 pop x f x gt f f f x TRUE lt td sxa 3xd22ed gt v 2xx d TRUE The simplifier includes a number of cooperating special purpose provers each a decision 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 reflect only the present version 3 2 Prover for arithmetic The axioms of this theory are 48 Part ii Chapter 3 Description of the Simplifier 0 0 x 9 z x y 2 lt lt lt lt lt XSy yszoxsz X 92x42 42z 0 41 0 lt 1 The numerals 2 3 and 2 are defined in terms of 0 1 and lt in usual way We also allow multiplication by integer constants for instance 2 abbreviates x The integers rationals and reals models for these axioms Any formula which is unsatisfiable over the rationals or reals can be shown unsatisfiable as a consequence of these axioms Thus our simplifier is complete for the rationals or reals It is not complete if the variables range over the integers since there unsatisfiable formulas such as xtx 5 which cannot be shown unsatisfiable as a consequence
114. s no argument 2 3 Query commands 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 QU IT QUIT command is provided to allow one to exit gracefully from the verifier QUIT will return you to the monitor LISP Typing LISP 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 Il Chapter 2 User Commands R u ning tire system When loading the system it will print out some more or less useful messages As soon as the prompt character gt 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 charact
115. s used in the verifier is given in Appendix C Part Introduction to the Starrford Pascal Verifier 4 The Rule Language 4 1 Backward rules Backward rules express logical implications and are stated INFER F FROM G The rulehandler component applies these ruies in a depth first backwards chaining search for proofs A rule will apply to a problem if B is an instance of F INFER will then try to prove AG where is the corresponding instance of The rulehandier does not attempt to deduce new rules from the given set Example In 5 2 we formulate a property of the gcd function GCD4 INFER GCD X Y GCD HOD X Y Y FROM gt 0 Again note that this rule will only be applied by the system if an instance of gcd x y ged mod x y occurs as a result to be proven during the proof 4 2 Replacement rules These express logical equivalences between atomic formulas FeG and equalities between terms F G and are stated in the form REPLACE F BY G Whenever an instance of F occurs 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 concat x null sequence occurs during the proof 4
116. se from the theorem is O 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 FROM Q C INFER R C The data base is P A AQ B AP C is now asserted At this point the rule M IA fires since Q B Q A by the built in theory of equality and R A is asserted The data base is now P A A Q B A P C A A B A R A Rule is waiting for instances of P x where x is distinct from A B or C Rule M IB is waiting for Q C 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 are both in the data base a contradiction is indicated Thus we have proved the theorem using the rule 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 in M 1 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 appear 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 f
117. sly 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 Functions and procedures may not be passed as parameters 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 single quote 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 Functions 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 Input Ouput The only I O statements allowed are EOF READ REWRITE and WRITE EOF takes entity of type FILE and returns TRUE or FALSE 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 usua
118. ssume 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 commands A READ command parses source code rulefiles programs V Cs 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 Commands 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 the command READ FOO VC is equivalent to EADVC FOOVC Examples READ parses source code typed in from the terminal READ FOO BAR parses the file FOO BAR REA DVC FOO parses the file FOO VC assuming that it contains VCs R EA D FOO VC 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 command PRINTVC The command PRINTV
119. t 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 modern 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 Input PI i f icat ion Program vos LEN and Documentation Simplified vcs l Modified Problem Fig 1 21 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 logic of programs had been given 121 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 11 Chapter for details The result is an internal tree representation from which the V Cs 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
120. t application Beware of rules that create numerous virtual instances For example LOSS WHENEVER F x F y FROM F x F y INFER P x y wilt create n12 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 space required for proof 73 Part 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 stat
121. t be used elsewhere The PASSIVE statement has been added to permit assignment to virtual variables It is merely an assignment statement preceded by the keyword PASSIVE This is the only way in which a virtuai variable may be assigned to 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 The symbol 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 is the formulas following INVARIANT COMMENT ASSERT ASSUME ENTRY and 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 15 no 38 Part 11 Chapter 1 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
122. tically equivalent to GCD1 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 TWIST REPLACE F x y BY F y x will cause no looping Similarly replacement rules can be provided for both directions of an equality 68 Part Il Chapter 4 The Rule Language A SC 1 REPLACE F x F y z BY F F x y z ASC2 REPLACE 2 BY 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
123. tion 5 8 1 Theory We will briefly review the theory underlying the proof A context free grammar is a tupie lt 7 NT P s gt where T and NT are the sets of terminal and nonterminal symbols respectively The character 5 is a distinguished start symbol in NT and P is a relation over NT x TUNT The sets T NT and P are ail finite Whenever lt r is in P then r is of finite length The relation gt is defined over TUNT x TUNT as follows lt u t U 9 gt gt iff t w gt P 27 Part Introduction to the Stanford Pascal Verifier We use periods to denote the concatenation of sequences over TuNT The relation is defined to be the reflexive and transitive closure of gt The goal of the parser is to determine whether or not a given sequence over T is in the language generated by the grammar i e whether s gt u for the input u TO express the theory in our assertion language we introduce the following two predicates isprod t w iff lt t w gt e P isderiv x V iff xe NT A lt x v gt e gt From the definition of gt one immediately gets two lemmas isderiv x isderiv x u t v isprod t w gt isderiv x u w v 5 8 2 The parsing algorithm The parsing algorithm is standard see 1 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 start symbol s Then
124. ttempted verification is 26 Part 1 introduction to the Stanford Pascal Verifier Simplified Verification Condition INSERT 1 REACH WORD ROOT Y n REACH Y SENTINEL n YeSENTINEL n YeNIL n POINTER TO ROOT WORD n POINTER TO Y WORD n POINTER TO SENT INEL ZMORD n POINTER TO 2 WORD n POINTER TO 7 8 40RD n AWORD_1 lt WORDUZ 0 lt WORDcY gt NEXT 2 0 gt gt n WORD_O lt WORD_1 cZ_ gt lt AWORD_1 Z_ 6 gt NEXT Z_8 gt gt 3 REACH MORD 8 ROOT SENTINEL The identifier Z_0 represents the new value of Z WORD 0 and WORD lare 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 from 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 1 shows that the NEXT field of Y is pointing to Z 0 so this loop is between ROOT and 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 verifica
125. 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 ORD iI 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 3110 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 backward rules
126. type REAL INVALID TYPE FOR CONTEXT WHERE USED An attempt was made to dereference f 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 var 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 Appendix 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 be declared there LABEL DECLARED AND REFERENCED BUT NOT PRESENT Somewhere in your procedure or function you have stated GOTO 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 fu
127. ve not only gt 0 but also gt 0 gt 0 and so on We can avoid this by adding a whenever expression to the rule WHENEVER XxY FROM X 04 Y gt 0 INFER gt 0 The restriction XxY limits the application of this rule to those x and y whose product appears in the formula to be proved Again note that the use of restrictions is explained in Part Il 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 ARRO REPLACE A IJ E J BY 51 gt E I4 2 ALJ END RECO REPLACE A IL E BY CASES II E II4 2 A JJ END PNTO REPLACE A cl E c BY CASES 1 E I4 Ac END Part I Introduction to the Starrford Pascal Verifier REPLACE Aulc WHERE I4 BY Ac J gt PNT2 REPLACE lt A cl gt E gt vJ WHERE 14 BY Auf cio E PNT3 WHENEVER AuX INFER POINTER TO X uX PNT4 FROM POINTER TO X A INFER POINTER TO X A E PNT5 FROM POINTER TO X A INFER POINTER TO X AuY PNT6 FROM POINTER TO X AuY INFER POINTER TO X PNT7 FROM TRUE INFER PO
128. w at least 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 PROCEDURE 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 t
129. we repeatedly take the top element from the stack and if it is a nonterminal symbol we push w on the stack such that isprod t 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 will be an enumerated type called token and the set NT will also be as type nonterm We introduce a special type for this will be a record called item Note that this could well be a variant record our system does not support variant records as such but does provide union types Sequences that is elements from T and TUNT are represented as files i e corresponds to token sequence file of token and TUNT corresponds to 1 nt sequence which is a file of item Note that for an actual implementation we would have to change nt sequence to some type that can be represented in memory e g linked lists However for the presentation of this example we will use files a change in the data structure would not affect the overall structure of the verification 28 Part 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 isprod t w holds The decision of what produ
130. y 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 The declaration is used to describe the values of a parameter before and after a procedure call If procedure p x adds 1 x we cannot simply say x gt 0 p x 1 A con tion denoting tense is needed An INITIAL statement allows naming entry values 0 J NJTIA L x x0 A x gt 0 p x x x0 i The GLOBAL declaration permits the user to declare global variables of a procedure as formal parameters One important application of this is in dealing with pointer parameters If a procedure has a parameter of type it is often necessary to declare the reference class below of ail objects of type T as a global variable This permits the verifier to keep track of any side effects Other kinds of assertion statements are intended for use to avoid having to repeat inductive Part 1 Introduction to the Stanford 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
131. y 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 KU U G V H aX X0aU U0 body O U U0 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 VAR parameter consists of an identifier followed by a possibly empty sequence of component selectors sj The call rule introduces new variables 1 tn to save the values of the selector sequences of the VAR parameters _0 is the set 0 0 6 0 of new variables introduced to stand for the values of the VAR parameters after the procedure call Similarly H_0 is a set hy 0 hy 0 of new variables for the VAR globals The variables actualsy are the actual initial values corresponding to the formal variables in The formula 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 p A G B H is introduced to stand for the final value of each VAR parameter and VAR global Q tjesp 36365 A G BH O A G B_0 H_O actualsy A G B H B_0 H_0 61 lt 8111 81 0 gt By lt B rity By 0 0 R Q p A B R where G B H B_0 H_0 e 61 0 GG B H A 6 0 p A G

stanford pascal verifier user manual

Contents

Download Pdf Manuals

Related Search

Related Contents