Home

an extended semantic definition of pascal

Contents

1. N C I N 1 are DEF where I stands for the value of before entering the second loop Similarly the assertion for the third loop states that C J N CLJ N 1 have been assigned values The system also produces the arithmetic inequalities shown on each loop To be able to prove the exit assertion DEF C it is necessary to show that all of 40 LESSDEF lemma C 1 C 200 have values after the third loop Notice that each invariant only describes the initializations done by its own loop For instance the third invariant only deals with the last part of C and does not repeat the fact that the first part of C is initialized by the first loop Runcheck uses the Lessdef lemma to infer that the first part of C continues to be DEF even though that fact is not included in the later invariants Thus the invariants shown are sufficient to prove that C is fully initailized on exit The documenter s assertions are also sufficient to show that the program executes safely 7 4 Inrange lemma The Inrange lemma says that a program for which P A True holds cannot cause the value of a subrange variable to become out of range when started in a state which satisfies P If a subrange variable is known to always be DEF at some point in a program that executes without errors then the variable must be Inrange at that point To begin we define Inrangex a formula constructor similar to Inrange The difference between the two is that Inr
2. Xn tn tf B O X1 Xn G P Eval Al Eval An Ip A1 An G a O A1 An G gt Q J 7 7 7 7 4 F1 P Eval f A1 An Q which states that evaluation of f A 1 An can be reduced to the evaluation of Al An in order followed by the application of f if If and Of are shown to be valid entry and exit assertions forf G is the set of read only global variables and B is the body of the function f A fine point to be considered at the practical level is that some compilers change the order of evaluation within expressions if there are no side effects If the evaluation of an expression terminates it terminates with the same result under all orderings Since the truth of P Eval E Q depends only on whether evaluation of E terminates and the value of each subexpression all ordersof evaluation are equivalent with respect to P Eval E Q The truth of P Eval E Q can be determined by choosing any possible ordering and considering whether it is true for that ordering Rule Fl above depends on choosing one ordering Thus FI is correct even if there is reordering The situation is different when proving absence of runtime errors Then different possible orders of evaluation must be considered separately For instance an expression such as f x a i might have a runtime error if i is out of range If f x is evaluated first and does not terminate the error cannot occur But if th
3. Ever en ASSIGN P pv e Q where pv is any Pascal variable In order for P pv e Qto hold it is necessary for the assignment to execute without any runtime errors and for Q to be true in the updated state The rule requires the right hand side e to evaluate without runtime error and to yield an initialized value the location calculation for left hand side pv is also required to be free from errors If pv is a subrange variable the Inrange clause requires the value of e to be in the correct range The updated formula Q is formed by substituting e for the Pascal variable pv using the definition of substitution given in section 2 2 Executable statements 27 IF statements P Eval L ASSUME L 1 Q P EvalL assume L S2 a E A IF P IF L THEN S1 ELSE 82 Q CASE statements for iz1 n P Eval X ASSUME X C S Q P Eval X Xe C4 Cn E CASE The C are lists of constants for each branch of the CASE statement The second condition requires the CASE expression X to evaluate to one of the constants in one of the Cj NEW procedure The following axiom states that the effect of the Pascal statement NEW x where x is a variable identifier of a pointer type is to change the value of x to a new pointer value xo and to add the new value xo to the reference class T x T u x0 x where x is an identifier of type tT pointer to object of type T x0 is a fresh identifier not appearing in Q
4. Refer to 3 for a discussion of the problems of variants and the details of our UNION types 2 Introduction error The runtime errors for a langauge are the conditions under which programs cannot continue to execute or continued execution would give undetermined results For a program to be useful one needs to know more about it than that it does not have runtime errors Consider a program which is intended to copy a list made of pointers and records it can have anerror which causes it to produce the wrong result without any runtime errors in the sense we are using Runcheck makes it possible to verify such a program at several levels of detail For the least detailed verification the program is submitted to Runcheck without additional specifications related to list copying In this case Runcheck attempts to prove only that the program is free from runtime errors In general it may be necessary for the user to supply some specifications and invariants even at this level of detail For instance the program may have a control stack overflow unless the input is acyclic User supplied invariants would be needed in case the simple invariants generated automatically by the system are not sufficient to prove absence of runtimeerrors A more detailed verification could be obtained by adding specifications saying that the result of the program is a copy of the input An even more detailed verification could establish bounds on the performance of the
5. all pairs of variables in the set are disjoint 3 Theory of Definedness The Predicate DEF In order to introduce the possibility that a program variable can be uninitialized we 12 Theory of Definedness The Predicate DEF assume the existence of an uninitialized scalar value Q The value of a newly created program variable is unspecified This is explained more fully in section 6 3 Before the program can use the value of a variable it must assign the variable a fully initialized value one such that none of its components is equal to 2 The predicate DEF will be true only of these fully initialized values In the intended model of the first order theory of DEF terms of a simple sort range over a universe of values including Q Values of compound sorts are built up by using the sets of simple values as components For example the possible values of a variable of sort ARRAY s OF INTEGER include arrays with some positions equal to Q Axioms DEF1 DEF8 below describe the properties of DEF and of Pascal types DEF1 for every constant c DEF c is an axiom DEF2 if e is of an enumerated sort cl cn DEF e gt e clv ve cn DEF3a if x is an expression of sort ARRAYLa b OF t DEF x Vi asinisb gt DEF x i DEF3b if r is of a Pascal record sort and f 1 fn are the record field names DEF r DEF r fl Ja ADEF r fn DEF3c if t is of a reference class sort DEF t Vp POINTERSTO t
6. range Similar reasoning is required for other array accesses VAR E V INTEGER PROCEDURE SPANNING IA JA ARRAYL1 El OF 1 V VAR P INTEGER VAR T ARRAY 1 V 1 OF INTEGER ENTRY DEF E a DEF V A1 lt E A 2sV EXIT TRUE VAR I J K C N R INTEGER VAR VA ARRAY 1 V OF INTEGER BEGIN C 0 N 0 FOR K I TO V ZNVARZANT 1 K A K lt V 114DEFRANGE 1 K 1 VA DO VALK 0 FOR K I TO E INVARIANT 1 lt K A KCEF1 AOC NA OKC ANCK 1 a CEK 1 A KE VEN T DO BEGIN IF K N V 1 THEN GOTO 1 IA K J JA K IF VALIJ 0 THEN BEGIN TLK NJ K IF VACJJ 0 THEN BEGIN C 4 1 VALJI C VALI C END ELSE VA T VALJ END ELSE IF VALJJ 0 THEN BEGIN TLK N K VA J VA I END ELSE IF VALI VA J THEN BEGIN TCK N K I VA I J VA J FOR R 1TO V INVARIANT 1 lt R AR lt V 1 DO IF VA R J THEN VAL R 1 END ELSE N N l END 1 P V E N END Inrange lemma 45 Note that IA and JA could have been declared as arrays of INTEGER and the restriction on the values could have been part of the entry assertion Expressing the restriction would involve a quantified assertion such as Yx 1 lt xsE gt 1 lt IA x sv This is both more difficult to write than the subrange type specification and it causes difficulty in theorem proving 8 Generalizations of the extended semantics 8 1 Dynamic subranges There are programming languages more flexible than Pascal which allow declaration of dynamic subranges ADA in parti
7. C J N B J J J 1 END END LESSDEF lemma 39 The system will verify DEF A a DEF B body DEF C i e that the program does not have any execution errors and that no elements of C are missed All ofthe other variables are initialized before the first loop Still it is necessary to prove that they are DEF each time they are accessed In the case of a variable such as l Runcheck uses the Lessdef lemma to infer that it has a value everywhere in the program after the assignment 1 Even though is changed on the first loop it is not necessary to write DEF D or A B J N as an invariant In many array programs the arrays are either supplied as fully initialized parameters or are initialized at the beginning Without the Lessdef lemma it would be necessary to have invariants repeating the fact that an array or other data structure is DEF at various points within a program Consider now the more complicated case of proving DEF C The system automatically generates the statements shown in bold italics By examining the first loop one can see that at any time values have been assigned to the positions C 1 C I J 2 This fact is discovered by the system and is expressed in the invariant as DEFRANGE 1 I J 2 C DEFRANGE is a special predicate used to express that a subrange of an array is DEF Its definition is DEFRANGE x y a Vi xsisy gt DEF aLi The invariant for the second loop states that C I
8. N INTEGER TYPE ARR ARRAYL1 N OF INTEGER PROCEDURE SEARCH KEY INTEGER A ARR VAR I INTEGER GLOBAL N ENTRY DEF N a 1 lt N a NSMAXINT BEGIN ALN KEY I 1 WHILE ALI KEY DO I I 1 END 2 There are cases where the difficulty of proving absence of all runtime errors outweighs the additional benefit A practical approach in such cases is to leave some errors unchecked Introduction 5 This program depends on the fact that A N has the value KEY throughout execution of the loop Otherwise if the key was not found in A the loop would continue and attempt to access A N 1 causing a subscripting error It is necessary to prove that AI N KEY is an invariant of the loop and in our extended semantics such lemmas can be proven together in one step with the proof of absence of runtime errors The procedure SEARCH is presented to the Runcheck system with an ENTRY assertion stating that N has a value between 1 and MAXINT the largest integer The system is able in this case to verify absence of subscripting errors arithmetic overflow and uninitialized variable errors the use of the value of a variable before it has been assigned a value automatically given only the ENTRY assertion and program text as shown in Example 1 In particular the necessary loop invariants including AIN KEY are generated automatically without any effort on the part of the user The reader is warned not to form an opinion of the system s capabilities o
9. Pascal statements containing expressions and variables The statement Eval E corresponds to the action of evaluating the expression E which Expression Evaluation 17 may not have side effects P EvalE Q is defined to mean that if P holds then E evaluates without runtime error and if E terminates then Q will hold Since E does not have side effects P and Qrefer to states with the same values for variables By having two assertions it is possible to make partial correctness statements about function calls For instance if f is a strictly partial function P x Eval f x Q x f x may be a provably true statement about the evaluation of f x while the pure first order statement P x gt Q x f x would not be true since it does not account for divergence of f x The other form of evaluation statement Locate V corresponds to the action of computing the location of a variable The difference between this and evaluating a variable is that to compute a location all of the subscripts must be evaluated and all dereferenced pointers must be evaluated but the variable itself need not have a value For instance to execute the assignment statement A j e the subscript j must have a value in the correct range but the left hand side A j is not required to have a value The definition of A jl e is expressed in terms of Locate A j and Eval e since the right hand side must yidd a value The formula P Locate VJ Q is defined
10. S 500 Of course the extended definition checks that any program that uses the value of S first assigns it a value in the proper range Runcheck makes use of a restriction that the entry assertion for the outermost block of a Inrange lemma 43 program must be DEF convex With this assumption Runcheck can infer bounds on the value of asubrange variable if itis known to be DEF In some cases this can permit lengthly assertions to be omitted For instance if a complex data structure contains subrange variables and the entire data structure is DEF bounds for the subrange variables can be deduced without any additional assertions By induction on the depth of procedure calls the lemma can also be applied to formal parameters when reasoning about a procedure body Since a value parameter v must be DEF on entry Inrangex v t must be true initially Variable parameters do not have to be DEF on entry but if the value is used somewhere in a procedure body it must be possible to prove that the variable is DEF and the Inrange lenma applies at that point Example 5 Constructing a Spanning Tree The following program is a simple algorithm 12 for finding a spanning tree of an undirected loop free graph with E edges and V vertices If the graph is disconnected it grows a spanning forest The graph is entered as a table of edges in the arrays IA and JA so that the vertices of the kth edge are IA k and JA k The program stores the indices o
11. T is the reference class for type T T u x0 stands for the reference class after adding an object pointed to by x0 x0 POINTERSTO a DEF x0 a xOxNIL gt Q 0 INEW x Q NEW1 The antecedents on the left side of the rule state that 1 the value x0 generated by NEW is a new pointer not a pointer tothe reference class T 2 xO has an initialized value and 3 x0 is not the pointer NIL The term T u x0 represents the new reference class after the dynamic variable xOT has been allocated A more complete discussion of POINTERSTO and the operation of adding new elements to a reference class can be found in 11 28 Executable statements The following rule reduces a NEW statement involving a selected variable to a NEW statement with an argument which is an identifier P NEW SO S S0 Q rasmenis e t ias NEW2 P NEw s Q where SO is a new identifier not appearing in the scope P or Q the declaration VAR SO type S is added to the scope WHILE statements Pol I Eval B ASSUME B S I Eval B B gt Q socar ee Sse aaan E WHILE 1 P INVARIANT WHILE B DO SJ Q In this rule the invariant is chosen to be true before each evaluation of the While test B The rule can be rearranged to correspond to other choices of invariants 6 3 Functions and procedures 6 3 1 Function declaration With the function declaration rule one can infer that and are valid entry exit specifications for a function f
12. a syntactic examination of the subprogram body For instance a global variable g which is used in an assignment statement g e must be declared read write Also if the body of p contains calls to q then all globals listed for q must be listed for p Reference classes are a special case of global variables which are implicitly accessed or altered although they do not appear explicitly in the executable program text If a 30 Note on Global Variables subprogram evaluates pT this is considered an implicit access to a reference class An assignment pt e is considered an implicit write to the reference class The system requires all reference classes which are used as globals of a subprogram to be explicitly listed by the user as global parameters The presence of a pointer formal parameter does not necessarily imply that a reference class will be accessed or altered by asubprogram For instance a procedure p with a VAR formal parameter x which is a pointer to an integer TYPE ptr tINTEGER PROCEDURE p VAR x ptr BEGIN x NIL END may assign to x without altering the reference class INTEGER No globals would be listed for this procedure since it changes only the pointer x and not any of the integer variables pointed to On the other hand in a procedure p2 which assigns to xT it would be necessary to list the reference class INTEGER as a read write global TYPE ptr tINTEGER PROCEDURE p2 VAR x ptr GLOBAL V
13. gt lt term gt lt predicate gt lt declared boolean function sign gt lt Pascal built in predicate lt lt gt lt undeclared predicate sign gt lt atomic gt lt predicate gt lt termlist gt True False lt formula1 gt lt formulal gt lt logical connective gt lt formula1 gt lt formula1 gt V lt undeclared variable gt lt formula1 gt lt atomic gt lt statement gt lt Pascal executable statement gt lt assume statement gt lt evaluation statement gt lt statement gt lt statement gt lt assume statement gt ASSUME lt formula1 gt lt evaluation statement gt Eval lt Pascal expression gt Locate lt Pascal variable gt lt subprogram declaration gt lt Pascal function declaration gt lt Pascal procedure declaration gt lt formula of unextended definition gt lt formula1 gt lt formula1 gt lt statement gt lt formulal gt lt formula 1 gt lt subprogram declaration gt lt formula 1 gt lt formula gt lt formula1 gt lt formula1 gt lt statement gt lt formula1 gt lt formula1 gt lt subprogram declaration gt lt formula1 gt Throughout the paper we will distinguish between the type of an expression and its sort in the many sorted first order language By the type of an expression we mean its Pascal type according to the scope By the sort of an expression we mean its sort in the first order
14. invariant of the loop that B can evaluate Safely 2 It makes it unnecessary for the invariant to refer to variables which cannot be changed in the loop This has been previously called a frame axiom 8 14 3 It applies the Lessdef lemma adding to the invariant the information that variables changed on the loop cannot become less fully initialized 4 Runcheck s automatic documenter generates invariants which are valid in the unextended semantics Because proofs in the extended semantics can be separated with part done in the ordinary semantics Specification lemma the extended While rule can assume the validity of documenter invariants without reproving them We now discuss the implementation of these changes 1 From the definition of P Evale Q one can write down a sufficient precondition for e to evaluate without error This formula will be called PRE Evale True As an example if the test of a While loop is f a b lt 0 and f has the declaration FUNCTION f x INTEGER c d ENTRY I x EXIT O x then the condition PRE Eval f a b lt 0 True DEF a a DEF b a l a A O a a DEF f a a csf a sd gt MAXINT lt f a bsMAXINT is added as an invariant of the loop 2 The variable identifiers are divided into a subset X which are not changed in the body of the loop and a subset Y which may be changed A set of new unique variables Y is introduced The extended form of the frame rule is 54 Append
15. program such as the maximum number of times each statement is executed as a function of the input 10 The purpose of Runcheck isto automate the routine aspects of the least detailed verifications while still allowing the user to supply additional information for more detailed verifications Thus although Runcheck is primarily used to perform shallow verifications it provides a general logical framework for proving detailed properties Every program verified by Runcheck is assured to have as a minimum the property that no runtime errors can occur if the entry assertion is satisfied This paper is concerned with an extended axiomatic definition of Pascal which is the logical basis of Runcheck The extended definition is similar to the familiar Hoare axiom system 6 but it takes into account certain restrictions on the computation that have not been considered in previous axiomatic language definitions Introduction 3 Although the details of our semantic definition refer specifically to Pascal most of the ideas are broadly applicable The runtime errors which exist in Pascal are also present in many other languages and the ideas in our semantic definition can be adopted to other languages with additional kinds of errors ADA 7 is an especially interesting case it should be possible to define much of the language by generalizing our definition of Pascal For instance the problem of generalizing our definition to allow dynamic
16. semantics The syntax of formulas is ordinary and is included here mainly for reference A formulal is a pure first order formula The syntactic category of program statements includes all executable Pascal statements plus some additional statements which are used only at intermediate steps during proofs The new statement types known as evaluation statements and assume statements do not initially appear in programs but can be introduced by certain rules during the course of a proof Evaluation statements correspond to the action of evaluating an expression or computing the location of a variable Assume statements are used by some of the proof rules to record previously justified logical assumptions at points within the body of an executable program Implicitly associated with each formula is a set of declarations of constants variables types and defined procedures and functions corresponding to a static scope in a program The syntactic distinction between declared and undeclared symbols is made with respect to the scope It is assumed that all name conflicts in the scope are removed by renaming lt variable gt lt declared variable gt lt undeclared variable gt lt op gt lt Pascal built in function gt lt declared function sign gt lt undeclared function sign gt lt term gt lt op gt lt termlist gt lt variable gt lt constant gt Formulas in the extended semantics 9 lt termlist gt lt term
17. sqrt x gt True which are all true The second part 5 6 can be simplified DEF x a x lt 1 00 Locate a Eval sqrt x O lt sqrt x s1 00 DEF x a x lt 1 00 Eval sqrt x O lt sqrt x s100 by L1 and CONCAT DEF x a x lt 100 Eval x O lt sqrt x sx a DEF sqrt x gt O lt sqrt x s 100 by E6 DEF x A x lt 100 Locate x DEF x a Ossqrt x sx a DEF sqrt x gt Ossqrt x s 100 by E1 DEF x a x lt 1 0 0 gt DEF x a Ossqrt x sx a DEF sqrt x gt Ossqrt x lt 100 by L1 and CONSEQ True 6 Extended axiomatic semantics of Pascal 6 1 Assume statements The meaning of the statement ASSUME L is that L can be assumed to be a true assertion 26 Assume statements at a certain point in a program Assume statements do not initially appear in programs but can be introduced during the course of a proof to record logical assumptions which hold at points within a program For instance the rule for IF statements reduces a formula involving IF L THEN S1 ELSE 2 to two formulas for the two cases of the condition L In one formula the statement ASSUME L records the assumption that L was true and in the other formula ASSUME L records the assumption that L was false PAL gt Q eccevevee ccna ASSUME P ASSUME L Q 6 2 Executable statements Assignment statements The following rule applies to all assignment statements P Evale True ae P Locate pv Eval e Inrange e type pv AQ EET E nemeea
18. such thatinteger arithmetic does not overflow in the range Maxint Maxint Note that many computers use twos complement arithmetic in which the smallest negative integer has an absolute value one greater than the largest positive integer This situation andother possible number systems with asymmetrical ranges can be more accurately modeled by introducing a separate variable Minint to stand for the smallest integer and making the obvious changes in rules E2 E4 and E5 The following rule defines the evaluation of a function call f A1 An where each of the Aiis a value parameter and Gis a listof read only global variables For error free evaluation of the function call each of the Ai must evaluate and yield a value in the proper range The second the third premises of the rule state that if If and Of are valid entry and exit assertions for f then they can be used to show P Eval f A Q If the 22 Expression Evaluation parameters A and G satisfy the entry condition I then Or will hold on exit Also f A G will be DEF and Inrange these properties are assured by the declaration rule for i l n P Eval Ail Irrange Ai ti Ip X1 Xn G Function f X1 ti Xn tn t_ B Of X1 Xn G P Eval Al Eval An Tg A G a O A G a DEF f A G a Inrange f A G te gt Q ewe wenn nn enn ern nn nnn nnn n ne ee nnn MMMM E6 P Eval f A1 An Q Location Validity P Locate v P L1 this is an axiom
19. will run to completion The occurrence of a runtimeerror may depend on the values of data supplied to a program For this reason any technique for assuring the absence of runtime errors must be based on some method for specifying programs Showing the absence of runtime errors iSthus a natural problem in program verification We have been developing an automatic verifier for proving the absence of runtime errors in the language Pascal The Runcheck system takes as input a Pascal program with entry exit and optional invariant assertions and proves that the specifications are consistent with the program and that no runtime errors can occur Invariant assertions are not required in many cases because the system is able to generate simple invariants automatically but more subtle invariants must be supplied by the user The system currently checks for the following kinds of errors accessing a variable that has not been assigned a value array subscripting out of range subrange type error dereferencing a NIL pointer arithmetic overflow division by zero control stack overflow exceeding heap storage bounds and UNION type selection errors The verifier and our semantic definition of Pascal do not yet include REAL or SET types but pointers are permitted Obviously the notion of runtime error doesnot include every kind of programming 1 The language accepted by the verifier includes verifiable UNION types instead of Pascal s variant records
20. AR INTEGER BEGIN xt 0 END because an integer variable accessed by a pointer is changed Observe that depending on the actual argument a call to the procedure p above could have the effect of changing a reference class as in the call TYPE pir tINTEGER ptr2 tptr VAR y ptr2 p yt changes ptr Note on Global Variables 31 which changes the reference class ptrof variables of type ptr which are accessed by pointers In this case ptr isnot considered a global although the call rules do account for the fact that part of ptr is altered by being passed as a VAR parameter Which reference class is altered in this example depends on the call not on the definition of p For example in the call TYPE ptr TINTEGER ptrarray ARRAY 1 100 OF ptr ptrptrarray tptrarray VAR 2 ptrptrarray p zt 50 z is a pointer to variables of type ptrarray zT is an array of pointer variables and zt 50 is a pointer to an integer and hence the correct type to be an argument to procedure p The variable which p changes in this case is an element of an array accessed by a pointer and this causes a change to the reference class ptrarray The ability of a procedure with a VAR pointer parameter to change different reference classes depending on the actual parameter is exactly analogous to the ability of a procedure with a VAR integer parameter to change components of different integer arrays PROCEDURE q VAR x IN
21. DEPTH pt f r lt DEPTH p r 1 where f is A or B The lemmas are provided by the user to the system in the form of inference rules 13 to be used by the theorem prover 48 Procedure Parameters 8 3 Procedure Parameters Procedure and function formal parameters in Pascal have the weakness that the arguments of formal procedures are not declared It is not possible to determine syntactically whether a procedure parameter is called with the right number and type of arguments It is a simple matter to tighten the language by introducing more detailed declarations if this is done the usual syntactic checks can be performed for procedure parameters and they can be included in the axiomatic definition As an example of a program using more detailed declarations Sum a b f computes the sum of f x when x ranges from a to b FUNCTION Sum a b INTEGER f FUNCTION INTEGER INTEGER INTEGER VAR i s INTEGER BEGIN S 0 FOR i a TO b DO s s f i Sum s END Clarke 1 shows that any sound and complete axiomatic definition of procedure parameters in a language with recursion static scoping read write global variables and internal procedure declarations must depend on some method of making assertions about the state of the runtime stack of local variables Such an approach would greatly complicate both the semantic definition and the process of specifying and verifying programs Instead we will make the restriction that funct
22. Stanford Program Verification Group June 1980 Report No 18 Department of Computer Science Report No STAN CS 80 8 11 AN EXTENDED SEMANTIC DEFINITION OF PASCAL FOR PROVING THE ABSENCE OF COMMON RUNTIME ERRORS by Steven M German Research sponsored by Advanced Research Projects Agency and Rome Air Development Center COMPUTER SCIENCE DEPARTMENT Stanford University An Extended Semantic Definition of Pascal for Proving the Absence of Common Runtime Errors by Steven M German We present an axiomatic definition of Pascal which is the logical basis of the Runcheck system a working verifier for proving the absence of runtime errors such as arithmetic overflow array subscripting out range and accessing an uninitialized variable Such errors cannot be detected at compile time by most compilers Because the occurrence of aruntime error may depend on the values of data supplied to a program techniques for assuring the absence of errors must be based on program specifications Runcheck accepts Pascal programs documented with assertions and proves that the specifications are consistent with the program and that no runtime errors can occur Our axiomatic definition is similar to Hoare s axiom system but it takes into account certain restrictions that have not been considered in previous definitions For instance our definition accurately models uninitialized variables and requires a variable to have a well defined value before it
23. TEGER BEGIN x 0 END no giobais The first call in TYPE arr ARRAY 1 500 OF INTEGER VAR vl v2 arr q v1 50 q v2 50 alters part of v1 but the second one alters part of v2 32 Procedure declaration 6 3 3 Procedure declaration I X Y G A DEF X1 A ADEF Xm a Inrange X1 t1 a AInrange Xm tm B 0 x Y G ann nnn nnn nnn nanan nn nnn nnn nn nnn nnn nnn nnn nnn nnn nnn nnn nnn nnn nnn nnn nn nnn nnn nnn PD 1 X Y G Procedure p X1 itl Xm tm VAR Y1 u1 VAR Yn un B O X Y G where p has the procedure declaration PROCEDURE p X1 tl Xm tm VAR Y1 ul VAR Yn un GLOBAL GR VAR GW ENTRY I X Y G EXIT O X Y G B GR are the readoniy global variables GW are the read write global variables G stands for the set of all global variables GR u GW Like the function declaration rule the procedure declaration rule assumes that the value parameters are initialized by each call with values in the correct range On the other hand there is nothing unusual about procedures that work correctly with uninitialized VAR parameters Consider a simple procedure p which is called with an integer j and two array variables x and y and assigns x j the value y j TYPE s 1 100 TYPE arr ARRAYLs OF INTEGER PROCEDURE p j s VAR x y arr BEGIN xj y j END Since the procedure does not test the range of j before executing the assignment a call to p will produce a subscripting er
24. and D Oppen Extended Pascal Semantics for Proving the Absence of Common Runtime Errors unpublished manuscript available from Stanford Program Verification Group 5 Hoare CAR An axiomatic basis for computer programming Comm ACM 12 10 Oct 1969 pp 576 581 6 Hoare C A R and N Wirth An Axiomatic Definition of the Programming Language Pascal Acta Informatica Vol 2 1973 pp 335 355 7 ichbiah J D at al Preliminary ADA Reference Manual in ACM Sigphn Notices Volume 14 Number 6 June 1979 amp Igarashi R L London and D C Luckham Automatic Program Verification Logical Basis and its Implementation Acta Informatica Volume 4 1975 pp 145 182 9 Jensen K and N Wirth Pascal User Manual and Report second edition Springer Verlag New York 1975 10 Luckham D and N Suzuki Proof of Termination Within a Weak Logic of Programs Acta Informatica Volume 8 1977 pp 2 1 36 11 Luckham D and N Suzuki Verification of Array Record and Pointer Operations in Pascal ACM TOPLAS 1 2 October 19739 pp 226 244 12 Seppanen J J Algorithm 399 Spanning Tree Collected Algorithms from CACM May 1970 13 Stanford Verification Group Stanford Pascal Verifier User Manual Report No 11 STAN CS 79 73 1 Stanford University March 1979 14 Suzuki N Automatic Verification of Programs with Complex Data Structures Ph D dissertation Dept of Computer Science Stanford University 1976
25. ange asserts that a subrange variable is in the correct range and is always true for other types while Inrangex asserts that every subrange variable contained as a component of its argument is in the correct range Definition Inrange is a mapping lt pascal variable gt x lt type gt gt lt formula gt For simple types Inrange v t is true if Inrange v t is Inranges v t is true for a compound type if Inranges c type c is true for every component c of v The idea of the Inrange lemma is a characterization of the possible sets of states of programs that always execute without runtime errors Any actual execution must begin in the outermost block with all variables uninitialized Data needed by the program is obtained by a READ procedure which always returns values that are DEF and Inrange Given that the program always runs without errors what do we know about the set of all possible states if it terminates Variables that the program assigns to every time it is run will always be DEF and Inrange at the end Variables that are never touched by the program will be completely unspecified at the end Variables assigned to on some Inrange lemma 41 runs but not on others can be DEF at the end or can have a value dependent on the values of the other variables If the value is dependent on the other variables it must be an Inrangex value The essential point is If a program determines the value of a variable the value must be Inran
26. ants DEF C and also DEF t for terms t formed by selecting components of Cs For each local L L C would be added as a premiss in the declaration rule But this is an unnecessary complication Also it does not accurately mode the implementation of Pascal in which initial values are left unspecified to reduce overhead For this reason it would give confusing results in practice If a program A never used two variables of the same sort X and y and otherwise executed without errors it would be possible to prove that the variables were equal after the program P A3 xzy Such a result differs from the implementation and probably conceals a programming error 6 3 4 Procedure call The procedure call rule requires each value parameter to evaluate without runtime Procedure call 35 error yielding a value in the correct range and each VAR parameter to yield a location without runtime error for iz 1 m P Eval Ai Inrange Ai ti for i 1 n P Locate Vi True X Y G Procedure p X1 t1 Xm tm VAR Y1 u1 VAR Yn un B O X Y G P Eval A1 amp val Am Locate V1 Locate Vn Disjoint set V u G a I A V G a Wz w 0 A z 4R aw gt a V nnn nee ened ee ot See eee PC1 P p A1 Am V1 Vn Q Each of the actual VAR parameters Vi must be a distinct Pascal variable not in GW Note that this definition depends on the definition of substitution when Vi is not an identifier 7 Me
27. applications that could lead to circular proofs For the procedure call conditions 8 4 8 5 and 8 6 are as before Condition 8 7 checks that the actual function parameter c satisfies the specifications of s 8 8 checks the entry exit assertions for the actual procedure d 9 Discussion Our definition of Pascal describes some important aspects of the language that have not been included in previous axiomatic definitions We began by recalling that a proof of P A Q does not give any assurance that a program will be free from runtime errors and argued that a stronger relation P A Q is a better indicator of program reiiability As part of our presentation of Pascal semantics we have developed a precise and comprehensive definition of the evaluation of expressions and Pascal variables using partial correctness statements to account for function calls within expressions Previous 52 Discussion axiomatic definitions have not dealt fully with the semantics of function calls within expressions We then used the definition of evaluation to define Pascal statements procedures and functions The complete definition is very concise although it captures many complicated details of the language One of the crucial advantages of our axiomatic technique is its simplicity absent are the clouds of obscuring notation commonly found in denotational definitions The clarity and simplicity of our approach are of greatest importance when the definition
28. can be accessed The logical problems of introducing the concept of uninitialized variables are discussed Our definition of expression evaluation deals more fully with function calls than previous axiomatic definitions Some generalizations of our semantics are presented including a new method for verifying programs with procedure and function parameters Our semantics can be easily adopted to similar languages such as ADA One of the main potential problems for the user of a verifier is the need to write detailed repetitious assertions We develop some simple logical properties of our definition which are exploited by Runcheck to reduce the need for such detailed assertions This research was supported by the Defense Advanced Research Projects Agency under contract MDA903 80 C 0159 and by the Rome Air Development Center under contract F 30602 80 C 0022 1 Introduction In most programming languages there are various undefined conditions and illegal operations such as arithmetic overflow and array subscripting out of range We call these conditions runtime errors because they are violations of language or implementation imposed restrictions on program execution Current compilers do not attempt to detect runtime errors during compilation though they commonly insert special code to test for certain errors during execution This approach is costly in execution time and compiled program size and of course gives no assurance that a program
29. cannot be used Without this precaution the axioms would give a contradiction Suppose that the induction scheme for integers is 0 a Vn B n gt B n 1 ab n 1 gt Vx BCx P Then from DEF 0 and DEF n gt DEF n 1 ADEF n 1 one could deduce Vx DEF x which contradicts axiom DEF Consistency of the theories of DEF and datatypes 15 Another approach is to use a special axiomatization of arithmetic that allows instances with DEF One such scheme for induction on the integer sort is 0 a Vn B n gt 8 n 1 ab n 1 gt Vx DEF x gt amp x S P 3 2 The relationship between DEF and Inrange In Pascal every subrange type is bounded by two constants ab Thus according to the definition of Inrange Inrange x s implies DEF x if s is a subrange This follows from the properties of the lt ordering of the integers For example it is a theorem in the theories of integer ordering and DEF that Vx 1sx a x lt 4 gt DEF x because the standard properties of integer ordering imply that Yx 15x xs4 gt x 1V X 2 v X 3 v X 4 and each of these constants is DEF Note however that xVyVz DEF x a DEF z a xsy a ysz gt DEF y 3 1 is not a theorem about DEF because it cannot be proven from S P the special form of induction on the integers Indeed there are nonstandard interpretations of the theories of DEF and integers for which formula 3 1 is not satisfied Also note that it is not necessar
30. cular has flexible dynamic type declarations A reasonable extension to Pascal is to permit subrange declarations involving expressions eg TYPE s 1 2 x The expressions for the bounds are evaluated each time the scope is entered and the range of s is fixed for the duration Dynamic arrays can be obtained by using a dynamic subrange as the index type for an array etc The extended semantics can be adopted to handle dynamic subranges by defining Inrange e s to refer to the values obtained when the expressions for the bounds on s are evaluated The declaration rules for functions and procedures would be changed to check for error free evaluation of the expressions in the type declarations Also depending on the restrictions in the programming language renaming would be needed to distinguish between the initial values of the variables appearing in the type declaration and the values assigned after the dynamic declaration was evaluated 46 Bounds on depth of recursion and dynamic variable allocation 8 2 Bounds on depth of recursion and dynamic variable allocation Like the bound for arithmetic overflow bounds on recursion and heap storage are implementation dependent In critical applications the actual bounds may be set in advance and one might want to verify that the available storage will be sufficient In other cases the particular bound is not important but it might be useful to verify that a program does not attempt unli
31. e order is changed and afi Expression Evaluation 19 is evaluated first the error could occur Since different orders of evaluation can give different results we define P EvalE Q to be true iff every order of execution is error free and Q will hold after every terminating execution Another complication is the possibility of short circuit evaluation in Boolean expressions In evaluating an expression such as r AND s when the value ofr is False Pascal permits compilers to omit the evaluation of s The expression r AND s is assumed to have the value False because r is False Observe that if s does not terminate or if it has a runtime error the short circuit has a different partial correctness semantics from full evaluation For example P Evalr AND s False may be truefor full evaluation but not for short circuit Short circuit evaluation is really a form of branching within expressions The axiomatic definition assumes that full evaluation is used Some languages such as ADA permit short circuit evaluation in certain contexts but require the user to explicitly request it This seems to be a cleaner approach and we show below rule E3S how it can be formalized in the extended semantics In summary our detailed semantic definition of Pascal statements will be based on partial correctness assertions about evaluation of expressions and variables It is argued that even in the absence of side effects the definition of expression
32. eory of the integers and with standard theories of data structures with the selection and assignment operations 11 Each of these theories has a standard model containing only the values for which DEF is true in the extended semantics It would be possible to assure the consistency of the combined theories by restricting the axiomatization of data structures to values for which DEF is true Under this approach if Vx P x iS a standard axiom for a certain sort then Vx DEF x gt P x would be chosen as the corresponding axiom in the extended semantics The obvious disadvantages of this approach are that the axioms are more complicated and proofs would have to establish the truth of DEF for every term in orderto apply sort axioms We would like the extended semantics to have the same sort axioms as the ordinary system so we choose to use the standard axioms of data structures and to take advantage of the existence of nonstandard models For instance since all of the standard integers have constant symbols the models of our integer sort under the DEF axioms are the nonstandard models of arithmetic models with extra elements There is only one point that requires some care and that is combining the theories of DEF and arithmetic The standard theory of arithmetic must not contain the symbol DEF If an axiom system for arithmetic is used it must not contain DEF For example if the axiom system has an induction schema instances involving DEF
33. evaluation should as a practical matter account for possible variations in the order of evaluation We will give an axiomatic definition that does not assume any fixed ordering On the other hand function call rule Fl can be used if evaluation order is fixed or if runtime errors are not considered The rules defining P Evale Q are as follows 20 Expression Evaluation Expression evaluation P Locate V DEF V a Q EE E E1 P Evai v Q V is any Pascal variable P Evai a a dianainn duniau E2 P Evai A Q where is one of the monadic operators NOT The following rule for evaluation of an operator expression contains three conditions The first two assert that A and B evaluate without runtime error if P holds These conditions make the rule independent of any fixed order of evaluation by requiring either operand to evaluate correctly if evaluated first The third condition states that after both operands have been evaluated Q must hold Since there are no side effects and the first two conditions have established that the operands evaluate without errors the order in the third condition is not significant Notice though that the first condition is redundant because the third one also requires A to evaluate safely In stating the rest of the rules we will omit redundant conditions such as this P Eval A True P Eval B True P Eval A Eval BJQ P EE E3 P Eval A amp B Q where amp is a
34. f the spanning tree s edges in T 1 T V P where P is setto the number of trees in the spanning forest This example illustrates the use of subranges and the inrange lemma to strengthen the entry assertion of a procedure Since IA and JA are tables of vertices they have been declared as arrays of subrange values 1 V It is typical in graph manipulating programs to use a value stored in one array to compute an index into another array Here the variable is set to IA K and then VA I is accessed For the latter access tobe in the subscript range 1 V of VA on every iteration all enents of IA must have been in the 7 Wn an actual Pascal program no rssumptions an be made about the initial values of variables declared in e outermost block To be strictly realistic the verifier should not permit entry assertions there They are permitted as a small convenience e mrin block with an entry assertion is considered to bea shorthand for a procedure with globals The significance of this is thrt the truth of the entry assertion must be assured by some calling program i e it is possible to declare e procedure with an entry assertion that is not DEF convex but its actual set of entry statesis then e DEF convex restriction of the declared entry condition 44 Inrange lemma range initially Because IA and JA are value parameters their initial values must be DEF and by the inrange lemma Runcheck can infer that the dements are in the correct
35. for any declared variable identifier V P Locate R Q L2 P Locate R F Q where R is of a record type with a F field P Evai Z Z NIL a Q 2 22 L3 P Locate zt Q where Z is of a pointer type P Eval IJ True P Locate A Eval I Jnrange I indextype A Q Sg ee Re Beg Re ce CR gO aa Eg gin DEA L4 P Locate ALII Q where A is of an array type Example 2 Show Q Evalali pt True where Q DEF i a O lt i lt 1 0 0 a DEF alij a Osali s25 a DEF p a pxNIL a pf 6 a 1 OOOSMAXINT with the variable declarations VAR a ARRAY O 1001 OF INTEGER VAR i INTEGER VAR p tINTEGER By applying the inference rules in reverse we can find simpler sufficient conditions for the formula to be true W e will continue to work backwards until we reach sufficient conditions that are obviously true At this point the formula will be proven because it will be possible to construct a formal proof by starting with the final conditions and Expression Evaluation 23 applying the inference rules until the original formula is deduced The first step is to use rule E4 in reverse reducing the problem of proving a statement about Evalalil pt to proving statements about Eval afi and Eval pf Q Eval pt True 5 1 and Q Eval ali Eval pt MAXINT lt a i pt lt MAXINT 5 2 Before finishing the example we pause to mention a fact about the extended semantics which is helpful in renoving redundancy
36. from proofs Since expressions do not have side effects we can assume in proofs that the state does not change when an expression is evaluated The following lemma states this fact in a useful form Lemma P Evale True Iff P Eval e P t P Locate e True iff P Locate e P Another point about redundancy is that when applying the inference rules directly to prove P Eval E Q the proof of error free execution of some subexpressions may appear many times A mechanical evaluator of the preconditions can easily take the repetition into account and only verify each subexpression once Continuing the example show 5 1 Q Eval pt True Q Locate pt DEF pt by E1 Q Eval p pxNIL a DEF pt by L3 Q Locate p DEF p a pxNIL a DEF pt by E1 Q gt DEF p a pxNIL a DEF pt by LI and CONSEQ True by definition of Q Next show Q Eval a i True Q Locate aliJ DEF aLli by El Q Eval i DEF ali and Q Locate A Evali Osis 100 DEF aLi by L4 24 Expression Evaluation These lasttwo formulas are trivially provable since the assertion Qimplies that i has a value andthe whole variable A is always a valid location by L1 Having shown that both ali and p evaluate without any errors we can use the CONCAT rule to infer that one can be evaluated after the other i e Q Eval ali Evalpt True by CONCAT 5 3 It only remains to show that there is no overflow formula 5 2 Q Eval al
37. gex If a variable is always DEF at the end of a program then it must always be Inrangex Definition Let X be the set of simple components of the declared variables For instance if v is declared VAR v ARRAY 1 2 OF RECORD f INTEGER g BOOLEAN END then X will contain the variables v 1 f v 2 f v 1J g vi2 g Note that X is a set of variables not a set of the values the variables A state of a program is an assignment of values to each of the elements of X To refer conveniently to the value of a given variable yeX and the overall state we will use the notation that the y form of a state is a pair lt z Z gt where z stands for the value of y and Z stands for the values of the variables in X y A set S of states is DEF convex for the variable y iff for all Z VZ lt z Z gt S gt DEF z implies Vw lt w Z gt eSy gt Inrange w type y where Sy is the set of states in S represented in y form A set of states of X is DEF convex iff it is DEF convex for every variable in X A formula containing free occurrences of declared variables is DEF convex iff it is satisfied by a DEF convex set of states Examples assume the declared variables are VAR x INTEGER VAR y 1 10 7 1 True False both DEF convex 7 2 y 2 DEF convex 7 3 y 40 not DEF convex 7 4 y 40 DEF convex 7 5 DEF y not DEF convex 42 Inrange lemma 7 6 x 1 gt y 2 DEF convex 7 7 x 1 gt y 40 not DEF convex If Sis the
38. i Eval pt MAXINT lt ali pt lt MAXINT Q gt MAXINT lt ali pt lt MAXINT by CONSEQ and lemma applied to 5 3 True Example 3 User defined partial functions in expressions VAR x INTEGER VAR a ARRAY 0 100 OF BOOLEAN FUNCTION sqrt n INTEGER INTEGER ENTRY True EXIT O lt sqrtsn BEGIN ifn lt 0 then loop forever without execution errors otherwise set sqrt integer part of square root n END Suppose the function sqrt has been defined to correctly return the integer square root of n unless n is negative in which case it loops forever without runtime errors Using the function declaration rule which will be given in section 6 3 it is possible to prove True Function sqrt n INTEGER INTEGER body Ossqrt n lt n 6 4 The entry and exit specifications of sqrt can then be used to show that if sqrt is called with an argument x whose value is less than 100 the location of the variable af sqrt x can be computed without runtime error Expression Evaluation 25 DEF x a x lt 1 00 Locate alsqrt x True e DEF x a x lt 1 00 Eval sqrt x True 5 5 and DEF x a x lt 1 00 Locate a Eval sqrt x O lt sqrt x lt 100 by L4 5 6 Using the function call rule E6 the first part 5 5 reduces to DEF x A x lt 100 Eval sqrt x True DEF x a x lt 1 00 Evai x True and True Function sqrt n INTEGER INTEGER body Ossqrt x sx and DEF x a x lt 1 00 Eval x True a O lt sqrt x sx a DEF
39. if for inputs satisfying the body of the function executes without runtime errors and assigns a final value to the function which satisfies the exit assertion 0 Function declaration 29 I X1 Xn G a DEF X1 a ADEF Xn 4 Inrange X1 t1 a Alarange Xn tn TB O f X1 Xn G a DEF f A Inrange f t where f has the function declaration FUNCTION f X1 tl 3Xn tn te GLOBAL G ENTRY X1 Xn G EXIT O f X1 Xn G B The rule requires that the function have only value parameters XI Xn and a set of read only globals G The rule assumes that each of the value parameters has an initialized value in the correct range this assumption is justified by the call rule which checks the actual parameters If global variables are accessed the entry assertion must assert that they have been initialized In the exit assertion O f X 1 Xn the variable f stands for the value returned by the function The rule checks that the body assigns f a value in the correct range AS we will see in section 7 4 the condition Inrange f tp appearing after execution of the body is redundant Because the declaration rule requires f to be DEF after execution of the body it is not necessary to require f to be Inrange 6 3 2 Note on Global Variables Runcheck requires the user to declare lists of all global variables that could potentially be accessed or altered by each subprogram The system checks the lists by
40. ions or procedures with globals may not be passed as parameters With this restriction procedure parameters can be introduced in a natural manner The specification method will be to declare an Entry and Exit assertion for each formal parameter these will be used in the ordinary call rules when the formal is called When a procedure parameter is passed the call rules will check that the actual satisfies the declared specifications of the formal 8 Thie section discusses extensions planned but not yet implemented in the verifier Procedure Parameters 49 Nesting of procedure parameters is permitted to any finite depth Thus a procedure can have a procedure parameter which takes another procedure as one of its parameters but self application of procedures is not possible The various possibilities are illustrated in the example below a procedure p has value parameters U variable parameters V a function parameter s and a procedure parameter q The procedure q takes a function parameter r The main specification given for p is a set of entry exit assertions p and Op An occurrence in the assertions of the formal function parameter s as a function sign stands for the value of the functional parameter and not for a constant function The assertions may be thought of as first order schemes which the procedure call rule adopts to particular calls by substituting the actual function sign for the formal s To distinguish this kind of substi
41. is actually used to verify programs because program specifications and the proofs are also simple and understandable the user is free to concentrate on the real issues surrounding a program and its correctness Our axiomatic definition has been part of a devdopment with the goal of building a useful automatic verifier This has influenced the definition in several ways One important requirement for useful verification is to have convenient methods for specifying programs In Runcheck specifications are greatly simplified by having a single predicate DEF as the basis of all predicates referring to variable initialization The Lessdef and Inrange lemmas also eliminate the need for certain kinds of detail in specifications Although the idea of derived inference rules is by no means new this technique is more useful in practice than has been previously realized Appendix A Development of the WHILE Rule This section explains the actual While rule used in Runcheck The rule of section sect ion 6 2 Pol I Eval B ASSUME B SJ Eval B B gt Q ae ee ca a ae aa WHILE 1 P INVARIANT I WHILE B DO SJQ does not help to reduce the need for detailed invariants and is not convenient to use in practice The implemented rule has four additional features Appendix A Development of the WHILE Rule 53 1 It adds an invariant referring to the evaluation of the While test B B is evaluated once on each iteration and so it must be an
42. ix A Development of the WHILE Rule P X Y gt 1 Y P X Y al X Y Eval B X Y Assume B X Y S X Y VJ 1 X Y P X Y AI X Y Eval B x Y B x Y gt a x Y P X Y Invariant I X Y While B X Y Do S X Y Q X Y where the Y variables stand for the values of variables before the loop and the Y variables stand for the values of variables during or after the loop 3 For each variable y which can be changed in the body Lessdef y y can be assumed to bea valid invariant 4 Documenter invariants D X Y Y can be assumed valid The final rule is P X Y gt ICX Y aPRE P X Y al X YAPREALessdef Y Y AD X Y Y Eval B X Y Assume B X Y S X Y I X Y APRE P X Y aI X Y JAPREALessdef Y Y AD X Y Y Eval B X Y B X Y gt Q X Y Se E E tae e A ie ea ae te Stee WHILE2 P X Y Invariant I X Y While B X Y Do S X Y Q x Y where PRE is PRE Eval B TRUE Appendix B Simultaneous Substitution for Disjoint Variables In this section we present the definitions of disjointness for Pascal variables and simultaneous substitution for disjoint Pascal variables To begin we need to define the translation of a Pascal variable into a standard representation as a sequence consisting of a main variable identifier followed by zero or more selectors In the following lt el en gt denotes a sequence of n terms and the operator stands for concatenation of finite sequences Appendix B Sim
43. language Except for subranges the sort of an expression is the same as its type Integer and integer subrange expressions are of sort integer Similarly expressions whose type is a subrange of an enumerated type have the same sort as the enumeration A sort will be said to cover both the type with the same name and all subranges of the type 10 Formulas in the extended semantics To be well formed a statement must satisfy the syntax and type requirements of the programming language 9 Because of the correspondence between types and sorts an expression satisfies the type requirements of the programming language iff it is a well formed term according to the sorts A formulal is a first order formula which may contain free occurrences of declared and undeclared variables Each term or atomic formula whose outer sign is declared or Pascal predefined must also satisfy the type requirements of the programming language 2 5 Notation for the extended semantics The axioms and inference rules in the extended semantic definition are actually schemes or infinite sets of axioms and rules In this respect our system is no different from previous axiomatic definitions When a scheme is applied information from the program scope must be substituted in certain places To specify the information that is to be substituted we use a meta notation An expression involving a function or predicate sign in Bold Italics indicates a term or formula to be subs
44. llocation 47 Example 6 Recursive Tree Traversal Type PTR is defined to be a pointer to a record with A and B fields of type PTR The recursive procedure WALK simply does a depth first walk on a tree P To avoid stack overflow P must not lead to any cyclic list structure and there must be enough room on the stack for DEPTH P REC procedure calls so Stacksize must be greater than or equal to Stackptr DEPTH P REC Stackptr and Stacksize are declared as VIRTUAL variables to indicate that they may appear in assertions but may not be used in executable parts of the program ACYCLIC and DEPTH are user defined symbols for documenting programs that operate on trees The assertion DEF REC states that every allocated record in the heap of type REC is fully initialized This assures that WALK will not encounter uninitialized dynamic variables TYPE PTR tREC REC RECORD A PTR B PTR END VIRTUAL VAR Stackptr Stacksize INTEGER PROCEDURE WALK P PTR ENTRY ACYCLIC P WREC aDEF REC a Stacksize gt Stackptr DEPTH P REC EXIT TRUE BEGIN IF PNIL THEN BEGIN WALK Pt A WALK Pt B END END The proof depends on two lemmas about acyclic list structure If p is a pointer to acyclic list structure in the reference class r then pf f points to acyclic list structure If p points to acyclic list structure then the depth of pT f is less than the depth of p ACYCLIC p r A pxNIL gt ACYCLIC pt f r ACYCLIC p r a pxNIL gt
45. logical system Proofs involving the integer sort appeal to the usual properties of integers etc In the extended semantics each sort ranges over a universe including some uninitialized values This section is concerned with the question of how the presence of uninitialized values affects the theories of the sorts One problem that could potentially arise is that the standard properties associated with a sort could imply that all its elements are DEF contradicting axiom DEF 7 Consider the conjunction of axioms DEF and DEF7 Axiom DEF1 says that every constant symbol in the language corresponds to an initialized value Axiom DEF asserts that there are values for which DEF is false Obviously these values cannot be named constants or terms built from constants This raises the questions of consistency and of what the models of the sorts are like In the extended semantics each sort must 3 except for array sorts with no components such as ARRAY 1 0 OF t 14 Consistency of the theories of DEF and datatypes have a theory whose models contain at least one unnamed element This requirement is easily satisfied but it must be taken into account in choosing axioms for each sort For instance axiom DEF permits the models of enumerated sorts to contain extra elements which are not DEF Consequently all finite simple and compound sorts have extra elements that are not DEF The extended semantics is intended to be used with a standard th
46. mited recursion etc To describe bounds on depth of calls two new undeclared integer variables are introduced in the procedure call rule The variable Stksize represents the maximum depth of calling Stkptr represents the current depth The procedure call rule is modified to enforce a restriction that StkptrsStksize Neither variable can be assigned to by the program Stkptr is O on entry to a main program and each level of function or procedure calling increases it by 1 With these additions the procedure call rule is for i 1 m P Eval Ail Inrange Ai ti for i 1 n P Locate Vi True 1 X Y G S Procedure p X1 t1 Xm tm VAR Y1 ul VAR Yn un B O X Y G S P Eval Al Eval Am Locate V1 Locate Vn nia u G AIA V G Stkptr 1 Stksize Vn A YZ GW O A Z GR GW Stkptr 1 Stksize gt a A Stkptr 1 lt Stksize im Zn er ere hee eee ee ee eee eee pc2 P p A1 Am VI Vn Q where S stands for the set of variables Stkptr Stksize Note that in practical applications it might be important to use some measure of the actual amount of stack space used by a program instead of just the depth of recursion It would be simple to define a different function that depended e g on the number and types of variables in the procedure for incrementing Stackptr To measure the heap storage used counters can be added to the rules for NEW statements Bounds on depth of recursion and dynamic variable a
47. multaneously swapping ali with a j and changing i _ayf ali aljl i Ptasi alj ali i 1 E _faldt ja d2 ji ptt t2 t3 dt jd2 Pran Di t2 t3 lac ali li 1 j fl P lt lt a j aliD i alj D gt i 1 j Note that lt lt a j afi gt i a j gt stands for the value of the array a after first assigning the value afi to the jth position and assigning a j to the ith position Example B 2 Swapping two variables accessed by pointers Consider the effect of simultaneously interchanging xf and yf where x and y are pointer variables Appendix B Simultaneous Substitution for Disjoint Variables 57 TYPE ptr tINTEGER VAR x y PTR INTEGERcx gt INTEGERcy gt P x y INTEGER witeGeRcys INTEGERcx gt P x y lt lt INTEGER cy gt INTEGERcx gt gt cx gt INTEGERcy gt gt The final value of the reference class INTEGER is exactly analogous tothe final value of thearray a in example B 1 58 References 1 Clarke EM Programming Language Constructs for Which It is Impossible to Obtain Good Hoare Axiom Systems J ACM 26 1 January 1979 pp 129 147 2 German SM Automating Proofs of the Absence of Common Runtime Errors Proceedings of the Fifth ACM Symposium on Principles of Programming Languages January 1978 3 German SM Verification with Variant Records Unions and Direct Access to Data Representations forthcoming Stanford All Memo 4 German M D Luckham
48. n the basis of this small introductory example alone a variety of more interesting programs have been handled by the system Some of them can be found in section 7 of this paper and in 2 This paper is divided into nine sections and two appendices Section 2 contains important definitions particularly the definitions of the language and notation of the extended semantics Section 3 is mainly concerned with the predicate DEF which is true of expressions having a well defined value Section 4 presents some of the basic inference rules of the extended semantics Section 5 presents a precise axiomatic definition of the evaluation of expressions in Pascal In section 6 the definition of expression evaluation is used as the basis of a definition of Pascal statements functions and procedures Section 7 develops some properties of the extended definition that are valuable when verifying actual programs Section 8 discusses some generalizations of the extended definition including a new method of verifying programs with procedure parameters Following this is a discussion of our general conclusions Finally Appendix A gives details of the implementation of the extended semantics in Runcheck based on the principles developed in section 7 and Appendix 6 Introduction B discusses the details of a definition of simultaneous substitution for disjoint Pascal variables 2 Preliminaries 2 1 General definitions T reference class see Cl 1
49. of the ordinary system The extended definition only places more restrictions cm the allowable computations Consistency of the extended definition is a direct consequence of this lemma 7 2 Specification lemma When proving complicated specifications for a program it is sometimes helpful to prove the specifications without considering possible runtime errors and then prove separately that no errors occur In this way the details about runtime errors can be isolated in the proof The next lemma says that proofs in the extended definition can always be factored in this manner Lemma 7 2 If H P A Q and F P1 AJ Q1 then H PaP1 A Qnat The reason for this is that if both P A Q and P1 A Q1 can be proven separately then it is always possible to combine the proofs to show PaP1 A QnQ1 The design of the automatic Documenter in Runcheck is based on this lenma The Sin the case of built in procedures it is necessary to choose slightly nonstandard definitions if the resulting system is to be complsts with respect to specifications involving DEF The ordinary system that we have in mind has axioms stating that the results of built in procedures such as READ rnd NEW srs DEF Specification lemma 37 documenter constructs inductive assertions that are valid in the ordinary semantics The assertions can then be assumed true in proofs in the extended semantics Thus the documenter does not have to consider possible runtime errors
50. p NIL gt DEF tcp gt DEF4 DEF a ADEF b gt DEF a b where is an operator in lt lt AND OR NOT DEF5 DEF a ADEF b Abx0 gt DEF a b ADEF a DIV b ADEF a MOD b Axiom DEF6 defines equality for compound types DEF6a if x and y are expressions of a record sort and f 1 fn are the field names x y x fl y f 1 a Ax fn y fn DEF6b if x and y are expressions of sort ARRAY a b OF t xzy 2 Vi asisb gt x iJ yLi The following two axioms are not normally needed for proving absence of runtime errors in programs but are included for thoroughness Theory of Definedness The Predicate DEF 13 DEF7 for each sort s 4X DEF X is an axiom where Xs is a variable of sort s Axiom DEFS8 states that the result of selecting a component of an array or reference class using an undefined or out of range index is not DEF DEF8a if x is of sort ARRAY a b of t DEF xLi gt asinisb DEF8b if t is of a reference class sort DEF tcp gt gt DEF p ApeNIL The resulting theory of DEF is still not logically complete eg because it does not say much about the undefined values But we should not expect to find such details in a programming language definition All of the properties needed for proving absence of errors in programs have been included 3 1 Consistency of the theories of DEF and datatypes Each sort has some standard properties which must be included in the complete
51. relation sign or boolean connective Rule E8S formalizes evaluation of ADA conditions In ADA the boolean conditions for controlling IF and WHILE statements etc can have one of the forms lt expression gt AND THEN lt expression gt lt expression gt OR ELSE lt expression gt which indicate that the left hand expression is to be evaluated first after which the right hand expression will be evaluated only if its value is needed to determine the value of the condition The following rule for evaluation of A AND THEN B states that it Expression Evaluation 21 must always be possible to evaluate A and that 1 if A is false Q must hold and 2 if A is true it must be possible to evaluate B after which Q must hold P Eval Al A gt Q P Eval A ASSUME A EvalB Q digas acai aia ape E35 P Eval A AND THEN BJ Q Maxint is an undeclared integer variable representing the range on which integer arithmetic operators do not overflow The axiomatic definition makes no assumption about the values of Maxint In order to prove absence of overflow the user must supply assertions relating Maxint to the computations in the program P EvaiB True P Eval A Eval B MAXINTSA B lt MAXINT a Q an nn nnn nn nanan neem 2 0 E4 P Eval A B Q where is one of the arithmetic operators P EvalB True P Eval A Eval B B 0 a Q a T a a e a a E5 P Eval AB Q where is DIV MOD or Maxint can have any value
52. ror unless j is between 1 and 100 Also the actual variable supplied for y j must have been assigned a value before the call top No other restrictions are needed to assure error free execution In particular p will work regardless of whether x has been initialized and regardless of whether portions of y other than y j have been initialized For instance the following sequence executes without errors Procedure declaration 33 VAR a b arr VAR k INTEGER BEGIN k 50 b k 1000 p k a b now a 50 1000 END The behavior of p can be specified by providing it with entry and exit assertions TYPE s 1 100 TYPE arr ARRAY s OF INTEGER PROCEDURE p j s VAR x y arr INITIAL y yO ENTRY DEF y j EXIT y yOax jl yfji BEGIN x j yLj END The entry assertion states that y j has a value when p is called Note that since j is a value parameter with a subrange type the declaration rule assumes that it will be supplied with a value in the correct range this will be checked by the call rule The Initial statement simply introduces a new name y0to stand for the initial value of y at the time of entry to the procedure The exit assertion states that the value of y is unchanged and that x j is equal to y j To summarize the point of this example all of the rules for subprograms assume that value parameters must be supplied with initialized values in the correct range This is our inte
53. rpretation of what it means to correctly call a subprogram with a value parameter No such assumption can be made for VAR parameters and so it is necessary to describe the behavior of each one by means of entry and exit assertions It is of course possible for there to be implementations of Pascal in which calls with value parameters will produce the desired results in some cases even if the actual parameter is not fully initialized This is merely an artifact of certain possible 34 Procedure declaration implementation techniques Our definition attempts to capture what is meant by the language itself and is intendedto be sufficiently restrictive to be consistent with all possible implementations AS was mentioned earlier the initial value of local variables is not specified by the function or procedure declaration rules Another approach which seems reasonable at first glance is to assert that every local is initially undefined This is not needed in the extended semantics because for P A Qto be valid every variable must be assigned a value which is DEF before its value is used The declaration rules could be modified to specify an initial value for locals but this would unnecessarily complicate the definition and lead to confusion in applying the extended semantics It would be possible to introduce a new constant C for each sort to stand for the initial value The axioms would be changed to state that for each of these const
54. set of final states of a program that does not have runtime errors then S is DEF convex In the examples a program can set y to2 so 7 2 is DEF convex but 7 3 cannot be DEF convex because 40 is out of range Although y 40 is DEF convex it is not a possible set of final states the DEF convex sets include more than final states sets To attempt to characterize only final states would require much more detail than we need here Note that 7 5 is too weak to be a final set of states because it includes both 7 2 a possible set and 7 3 an impossible set Lemma 7 4a If a program is started in a DEF convex set of states and always executes without runtime error then the final set of states will be DEF convex It follows that if a program always leaves a variable DEF when it halts the variable must be Inrangex at the end Lemma 7 4b If B is a Pascal statement pv is a Pascal variable P is a DEF convex predicate and P B DEF pv then P B Jnrangex pv type pv The restriction on P in this lemma is necessary Recall that extended semantics does not specify the initial values of variables and that subrange type variables have the same sort as the base type of the subrange Consequently there is nothing that says a subrange variable cannot be out of range if its value is not assigned by the program The following formula is a a theorem even if the variable S declared with a subrange of only 1 100 S 500 empty DEF S a
55. subrange types is discussed briefly in section 81 Our axiomatic definition of Pascal consists of some first order theories plus axioms and inference rules for reasoning about programs One of the first order theories concerns a predicate DEF x which is true of expressions having a well defined value The other first order theories are familiar ones such as arithmetic Runcheck is more than a direct implementation of these logical components a practical program verifier should provide aS much assistance as possible e g in generating inductive assertions All of the example programs discussed in this paper have been handled completely automatically by the system Practical results with Runcheck have been reported in 2 An earlier approach to formalizing the extended semantics is presented in collaboration with D Luckham and D Oppen in 4 The theorems in the Hoare axiom system are of the form P A Intuitively this formula states that if P holds before executing a program A then if and when A terminates Q will hold In 5 6 and elsewhere the relation P A qQ is taken to be true if there is a runtime error in executing A Hoare chose to make the interpretation that if an error occurred the effect of the program would be undefined as if the program had failed to terminate In our extended semantics PIAJ is defined to mean that if P holds then A executes without runtime errors and if A terminates Q will hold Since vir
56. t necessary to state in the invariant that it continues to be DEF Similar assertions about VAR parameters can be omitted from procedure specifications Example 4 Merging two sorted arrays This example shows how Runcheck uses the Lessdef lemma to reduce the need for repetitious detailed assertions The program takes as input previously sorted arrays A and B of length 100 and merges their contents into the array C which has length 200 The user has supplied only an ENTRY assertion saying that A and B are fully initialized and an EXIT assertion saying that C is fully initialized The interesting aspect of this example is that the initialization of C takes place in two loops The first loop partially initializes C merging elements from A and B until either A or B has been completely transferred Then the initialization of C continues in ether the second loop or the third loop TYPE INARR ARRAYI 1 100 OF INTEGER TYPE OUTARR ARRAYL1 200 OF INTEGER VAR I J N INTEGER VAR A B INARR C OUTARR ENTRY DEF A ADEF B EXIT DEF C BEGIN N 100 I 1 J l INVARIANT DEFRANGE 1 I J 2 C A TKI AN TENFT NITES A SENG WHILE I lt N AND J lt N 00 BEGIN IF ALIJ lt B J THEN BEGIN C I J 1 ALT I 1 1END ELSE BEGIN C I J 1 BLJ J J 1 END END Fel INVARIANT DEFRANGE I N I N 1 C a T SI a I lt N 1 WHILE I lt N DO BEGIN C I N A I I I END J eJ INVARIANT DEFRANGE J N J N 7 C a J SJ A JENE 7 WHILE J lt N DO BEGIN
57. taneously substituting the ai for the xi and the bj for the yj in P If the set X of free variable identifiers of a formula P X is partitioned into subsets XI and X2 then P X1 X2 stands for P X and P A1 A2 where Al and A2 are ordered sets of terms stands for the result of simultaneously substituting in P the terms in Al for the variables XI and the terms in A2 for the variables X2 Substitution for a Pascal Variable v Pi where v is any term denoting a Pascal variable is defined recursively as follows pf where x is an identifier stands for P with t substituted for x vli v eE a t p lt v Li t gt f e elk t i v f o vep gt v P P ATN 2 3 Disjoint Pascal Variables Intuitively two Pascal variables are disjoint iff an assignment to one of them cannot affect the value of the other It is obvious that in languages with array subscripting and pointers disjointness is a dynamic property it depends on the values of variables For instance A i and A j are disjoint iff ixj If vi vn are disjoint Pascal variables it is possible to define the simultaneous 8 Disjoint Pascal Variables substitution P vi s vn ltl tn of n expressions for n Pascal variables in terms of the sequential substitutions defined above in 2 2 This definition and the formal definition of disjointness are needed only for the procedure call rules details are presented in Appendix B 2 4 Formulas in the extended
58. tatheory of the extended definition In this section we discuss some properties of the extended definition which are helpful in reducing the complexity of program specifications and the length of proofs By itself the extended semantics is not a complete solution to the problem of verifying the absence of common errors In practice there are two main kinds of difficulty in doing actual verifications These practical difficulties were carefully consideredin the design of the Runcheck system The problem of redundancy in proofs is solved in Runcheck by a special simplifier which efficiently eliminates redundant verification conditions A more serious problem is the need for lengthly detailed specifications and inductive assertions in programs Several distinct approaches are needed to deal with this problem In Appendix A we discuss the derived WHILE rule which shows how the extended definition reduces the need for detailed documentation The derived WHILE rule and other rules are logically justified by certain simple properties of the theory of 36 Metatheory of the extended definition the extended definition which are presented in the remainder of this section 7 1 Ordinary Semantics Lemma Any specification provable in the extended definition is also provable in the ordinary definition Lemma 7 1 If P A Q then P A Q The significance of this lemma is that all specifications even those involving DEF are theorems
59. tituted Instances of the axiom or rule are formed by evaluating the italicized meta expression to produce a term or formula For example the rule for assignment to a whole variable is P Eval y Inrange y type x AQ p Consider a typical context TYPE s 1 500 VAR g s h INTEGER g h 4 Since g is a subrange variable the assignment statement will cause a subrange error unless h 4 is in the correct range Jnarange y type x is the notation for a formula which asserts that the value of y is in the range of the variable x In the example Notation for the extended semantics ll context the desired instance of the rule is g P 1 lt h 4 lt F evansi vehee Ah 4 lt 500 A Qi p Ig h 4 Q 2 8 Formula Constructing Functions Inrange lt expression gt lt type gt Inrange is a function mapping lt expression gt x lt type gt lt formulal gt The expression must be of a sort which covers the type if type is a subrange a b Inrange expression type gt asexpression A expressionsb otherwise Inrange expression type gt TRUE Dis joint lt Pascal variable gt lt Pascal variable gt The function Disjoint maps a pair of Pascal variables into a formulal which is true iff the variables are disjoint Refer to Appendix B for a detailed definition of Disjoint Dis joint set lt set of Pascal variables gt For any finite set of Pascal variables Disjoint set constructs a formulal which is true iff
60. to mean that if Pistrue then the location of V can be computed without execution errors and if the computation terminates Q will hold The exact meaning of expression evaluation is often a point of confusion in programming languages and definitions The definitions presented here assume that sufficient restrictions are used to prevent side effects Pascal 9 assumes a fixed order of evaluation within statements and expressions so the final value of an expression is well determined even in the presence of side effects It is a simple matter to replace a function definition which has side effects by an equivalent procedure definition by adding a new VAR parameter to return the function value Thus it is possible to 18 Expression Evaluation rewrite a Pascal program in which functions have side effects into an equivalent program in which function calls are replaced by procedure calls and all expressions are free of side effects This transformation would convert the evaluation of an expression with side effects into a sequence of procedure calls involving some new variables to store temporary values Since this transformation can be easily mechanized our Pascal semantics are indirectly applicable even to programs with function side effects If runtime errors are not being considered as in the original Hoare axiom system function calls without side effects can be defined by the following rule I X1 Xn G Function f X1 tl
61. tually all programs are intended to execute without runtime errors a proof of P A J is much more useful 4 Introduction than one of P A Q from a practical point of view If it is possible to verify the absence of runtime errors in a program the implementation can omit the usual runtime error checking code an increase of efficiency without loss of reliability Also the extended semantics is a convenient system for showing the absence of certainerrors in programs that are not intended to terminate Our proof system is general purpose in that any partial correctness specification can be expressed by choosing P and Q Absence of runtime errors is proven together with other properties There are other possible formulations one could develop a proof system based on statements of the form SAFE P A meaning that if P holds beforehand then A executes without runtime error The disadvantage of such a system is that proofs of the absence of runtime errors often require lemmas about more general properties of the program For example consider a simple program which searches in an array A for an element equal to KEY The elements are stored in A 1 A N 1 The fast linear search stores the key in the last position of the array A before searching so that the search loop does not have to test whether the index has become greater than N The result of the search is returned in the variable I Examplei Fast Linear Table Search VAR
62. tution from sustitution for free variables the following notation will be used Notation Q f X is a formula containing the function sign f and free variables X After a particular formula Q f X has been introduced we will write Q g Y to stand for the result of replacing the function sign f by g and substituting Y for X in Q Each formal procedure parameter has a declaration in p of its entry exit assertions The declarations are like ordinary procedure declarations except that the reserved word FORMAL is used in place of the procedure body Since the formal parameter q takes a function r as an argument the declaration of q has a declaration forr nested inside it 50 Procedure Parameters Declarations with procedure and function formals PROCEDURE p U VAR V FUNCTION s Y t PROCEDURE q W Function r Y t FUNCTION s Y t specifications of formal parameter s ENTRY Is Y EXIT Os s Y s FORMAL PROCEDURE q W Function r Y t specifications of q Function r Y t specifications of formal parameter of q ENTRY Ir Y EXIT OrLrl Y r FORMAL ENTRY Iqfri wW EXIT OqLr W FORMAL GLOBAL GR VAR GW ENTRY Ip s u V G EXIT OpLs U V G specifications of p BEGIN pbody END executable statements of p Notation In the following rules entry exit assertions enclosed in brackets 1 0 are included in the procedure headers as an abbreviation for the full procedure declarations as shown abo
63. ultaneous Substitution for Disjoint Variables 55 The function Seq v lt Pascal variable gt gt lt term sequence gt is defined as follows Seq id lt id gt if id is an identifier Seq v f Seq v o lt f gt Seq v i Seq v o lt i gt Seaq vt lt t v gt where t is the reference class Definition of Disjoint v w Let v and w be Pascal variables and Seq v lt v0 vn gt Seq w lt w0 wm gt and assume m lt n Then Disjoint v w is the following formula if vO and wO are distinct identifiers then Disjoint v w gt True otherwise Disjoint v w gt vlewlv v vmewm The current implementation of Runcheck uses a much more restrictive definition of disjointness it only compares vO and w0 this restriction is not essential and will be removed in a later version Simultaneous Substitution We can now define a simultaneous substitution of n terms el en for disjoint vl vn Let Seq vi lt vig Vigy gt fori 1 n Let tl tn and di for 1 1 n j 1 mi be new identifiers not appearing in P the vi or the ei Define Unseg lt term sequence gt gt lt Pascal variable gt to be the inverse of Seq Unseq Seq v v 56 Appendix B Simultaneous Substitution for Disjoint Variables Then we can define vi vn P ay e1 en unseq lt v19 d11 d1 m1 unseq lt vngo dn1 sdnmn Pi t1 tn i im i imn etaha vta laar O bmg Ivnn Example B 1 Si
64. used to represent the set of values of a dereferenced pointer of type fT TcP gt value of the variable Pt where P has type tT Throughout this paper first order language terms of the form RcP gt will denote Pascal expressions of the form Pt Any Pascal expression involving pointers can be translated into this notation provided that the types of the pointer variables have been specified For further details refer to 11 POINTERSTO set of all pointer values of type tT lt A I E gt value of the array A after assigning the value E in the Ith position lt R F E gt value of R after R F E lt T cP gt E gt value of T after Pt E where P has type TT Functions mapping Pascal expressions into types type E the type of an expression E indextype A value is R if A has type ARRAYLR OF S Phrases used in a special sense The phrase simple variable is synonymous with both variable identifier and declared variable A selected variable is a component of a variable identifier eg A I is a selected variable A Pascal variable is either a variable identifier or a selected variable 9 Notation for Substitution 2 2 Notation for Substitution Simultaneous Substitution for Identifiers If P X Y is a formula where X xl xn and Y y1 ym are ordered sets of free variable identifiers then P A B where A al an and B b1 bm are ordered sets of terms stands for the result of simul
65. ve The idea of the declaration rule is to use the declared entry exit specifications of the formal parameters in this case s and q to prove the specifications for p Then for calls to p the call rule will check that the actual function and procedure parameters satisfy the specifications declared for s and q Example Procedure declaration is Y Function s Y t FORMAL Os s1 Y s 8 1 Iqfr W Procedure q W r lt Ir Or gt FORMAL Oq r 1 W 8 2 Ip s U V G a DEF U a Inrange vi ti pbody Op s U V G 8 3 Ip s U V G Procedure p U V s Is Os gt q W r lt Ir Or gt Ig 0q gt pbody Op s U V G Procedure Parameters 51 Example Procedure call for i 1 m P Eval Ai Inrange Ai ti 8 4 for i 1 n P Locate Bi True 8 5 Ip s U V G Procedure p U V s lt Is Os gt q W r Ir Or gt lt Ig 0q gt pbody Op s U V G 8 6 Is Y Function c Y t cbodyL Y Os c1 Y c 8 7 Iq r X Procedure d X r lt Ir Or gt dbody X r Oqfr X 8 8 P Eval A1 Eval Am Locate B1 Locate Bn Disjoint set B u G A Ip c A B G B1 Bn ee A NZAW OPLE NAZ GR GWI SO Fae aa Sa P p A B c d Q In the declaration rule the specifications of the procedure parameters s and q are used as assumptions 8 1 and 8 2 for proving the entry exit specifications of the main procedure p This rule can be justified by the type requirements which do not permit self
66. while constructing the invariants 7 3 LESSDEF lemma One of the basic properties of the extended definition is that if P SJ Q holds S cannot assign an uninitialized value to any variable Over any sequence of statements that executes without runtime error the extent of variable initialization cannot decrease LESSDEF x y a predicate for two terms of the same sort is defined to be true if y is at least as completely initialized as x LD1 if x and y are of the same simple sort LESSDEF x y DEF x gt DEF y L02 if x and y are of the same record sort and the field names are fl fn LESSDEF x y LESSDEF x f 1 y f 1 a ALESSDEF x fn y fn LD3 if x and y are of sort ARRAYLa b OF t LESSDEF x y Vj asjsb gt LESSDEF x j yLi LD4 if x and y are of sort REFCLASS t for some t LESSDEF x y VpePOINTERSTO x LESSDEF xcp gt ycp gt The LESSDEF lemma says that for any variable in a program that executes without errors the final value will be at least as fully initialized as the initial value Lemma 7 3 If H P A True and v is a declared variable identifier then tPA v v A LESSDEF V v where v is a new identifier not appearing in P A or the scope 6 Refer to 2 for dstrib of ths documenter 38 LESSDEF lemma In Runcheck the lemma is used to reduce the need for detailed assertions on loops and procedures If a variable is known to be DEF before entering a loop it is no
67. y for a variable to be Inrange if it is DEF under the axioms of DEF there can be a variable of a declared subrange type whose value is both DEF and not Inrange In the definition of P AJ Q no program is permitted to assign a value to a subrange variable unless the value is Inrange If P A Q holds a subrange variable can only be out of bounds before it has been assigned a value 4 More flexible languages are discussed in section amp 16 Fundamental inference rules 4 Fundamental inference rules The following two rules are included in both the unextended and extended definitions Concatenation of programs CONCAT P A Q Q B R P Ia a a B R PIA BIR PIA BIR Consequence rule CONSEQ P gt Q Q A R R gt S pe a A R Ras P A S PAIS These rules will be used implicitly beginning in the next section on the semantics of expression evaluation Later after P A Q has been defined we will develop its logical relationship to P A Q in more detail 5 Expression Evaluation This section introduces and defines evaluation statements Evaluation statements have the forms Eval lt Pascal expression gt Locate lt Pascal variable gt and in the extended semantics they can be combined with Pascal statements and assertion statements to form the general statements which appear inside brackets in a formula P A Q Evaluation statements will be used in section 6 to define the conditions for error free execution of

Download Pdf Manuals

Related Search

Related Contents

Mise en page 1  Portable Fridge/Freezer User Manual  AC/DC LiPo Charger Instructions  Lexmark 24B6035    Service Manual, C546 Self Powered EFX.fm  Model 700-40 Manual - Controls Warehouse  Hasbro 82576 Games User Manual    Behringer ULTRABASS BX2000H Quick Start Guide  

Copyright © All rights reserved. Failed to retrieve file