Home

(ESCJ 27:\240 ESC/Java User`s Manual)

1. 2 6 0 ghost pragma A ghost pragma is a declaration pragma It is allowed where the declaration of a class or interface member is allowed It has the syntax ghost M T VD i opt where Tis a specification type see section 3 0 vp is a Java VariableDeclarators JLS19 8 2 and mis a sequence of modifiers In other words the pragma is like an ordinary Java variable declaration preceded by the word ghost In the current ESC Java m must include the modifier public and vp can declare only one identifier The only other modifier allowed in mis static No initializers are allowed in vD The pragma is like the Java declaration M TVD opt except that it is visible only to ESC Java not to the compiler The variables declared by a ghost pragma are called ghost variables Fine points No field declared in vp may have the same name as a field including a ghost field or a field declared in a supertype already declared for the type in whose declaration the pragma occurs The current ESC Java does not implement local ghost variables A ghost field declared in an interface 7 is multiply inherited by classes that implement 7 and interfaces that extend z If a ghost variable f is declared in an interface 1 and 7 is extended by interfaces J and x and a class c implements 1 J and x and if x is a variable of type c then the expressions 1 x f J x f K x and x all denote the same ghost field That is c gets only one
2. a synchronized statement synchronized O O0rathrow statement throw o where o evaluates to null Any of these would result in a Nul1lPointerException being thrown at run time JLS 11 5 1 1 14 17 15 10 15 11 15 12 Remark JLS doesn t say that throwing nu11 results in a Nul1lPointerException but experimentation with javac 5 and java 5 reveals that it does Tips If the expression ois a formal parameter consider adding a non_nu11 pragma to the parameter s declaration or supplying a requires pragma stating that the parameter must be non null under certain conditions If ois a field access P g consider adding a non_nu11 pragma to g s declaration supplying an invariant pragma stating that g is non null under certain conditions or if P involves parameters of the current routine supplying an appropriate requires pragma If ois an array access consider supplying a requires OF invariant pragma using nonnullelements see section 3 2 12 If ois a method call consider annotating the called method with ensures result null Orf ensures Q gt result null for some appropriate condition Q See the second example in section 2 6 2 for an example of pragmas guaranteeing that an element extracted from a container will be non null 4 14 ownerNull warning As described in section 3 2 17 every constructor has the implicit postcondition this owner null An OwnerNull warning warns that a constructor may return an object whose
3. 3 2 7 Lock order lt and lt Within specification expressions the relations lt and lt are extended to apply to locks as well as numbers The order they refer to is called the lock order For some examples of use of the lock order see section 2 7 2 3 2 8 max 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes An expression of the form max s where s is a specification expression of type LockSet is a specification expression of type Object It denotes the maximum element of s in the lock order To insure that max is always well defined ESC Java assumes that lock sets are always nonempty and that their elements are always totally ordered by the lock order lt Since locks must be acquired in increasing order and since there is no way to write a program that releases the fictitious maximum element of the lock set of a thread that really holds no locks the preceding assumptions are invariantly true if they are true initially 3 2 9 Implication gt An expression of the form gt F where and F are specification expressions of type boolean is a specification expression of type boolean It denotes the condition that implies F that is z F The operator gt has less binding power than and but binds more strongly than the ternary conditional operator t The binding precedence of operators in Java is implicit in the grammar for
4. We can prevent ESC Java from complaining by declaring the field n to be spec_public 3 spec_public int n This will allow n to be mentioned in requires pragmas of public routines as well as in pragmas occurring in other packages that import the Bag class Of course actual Java code in other packages will not be able to read or write the n field directly as would be allowed if n were declared with a Java public modifier 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes Fine point By declaring n with a spec_public pragma the implementer of the Bag class expresses a design decision that users of Bag are supposed to know about the n field even if their Java code cannot access it directly This design decision could cause problems if implementer later decided to change the implementation to represent a Bag using a data structure that did not include an explicit count for example a linked list See the first example in section 2 6 2 for further discussion of this issue 2 5 1 readable_if pragma A readable_if pragma is a modifier pragma It can occur only as a modifier of a field declaration or of a local variable declaration It has the form readable_if E opt where is a boolean specification expression The pragma causes ESC Java to check that is true just before any read access of any of the variable s declared in the declaration The pragma thus
5. forall int i n lt i amp i lt 10 gt a i null 57 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 58 of 86 8 ObjStack 9 n 0 0 a new Object 10 1 2 3 requires n lt 10 4 void Push Object o 5 a nt 0 6 7 8 requires n gt 0 9 Object Pop 20 Object o al n 21 a n null 22 return o 23 24 25 The elements of a stack x are the first x n elements of the array x a To avoid retaining pointers to garbage we insure that the remaining elements of x a are null as specified by the invariant pragma on line 6 If we run ESC Java on the source above it produces the following complaint ObjStack Push java lang Object ObjStack java 16 Warning Possible violation of object invariant Invariant A Associated declaration is ObjStack java line 6 col 6 invariant forall int i n lt i amp i lt 10 gt a i null A Possibly relevant items from the counterexample context brokenObj lt 2 gt this brokenObj refers to the object for which the invariant is broken For a basic explanation of counterexample contexts see appendix A What is going on here is that ESC Java has found a scenario in which the Push method fails to maintain the instance invariant on line 6 The line brokenObj lt 1 gt this tells us t
6. ola x means the value of x in the pre state The static type of ola x is the same as the static type of x An expression x used as an argument of old may not itself contain applications of old or fresh More precise details are given below Fine points Postconditions of a synchronized method apply to the state after the release of the lock Except for formal parameters identifiers used in postconditions of a routine and not within old denote their values in the post state While Java allows a routine body to include assignment to the routine s formal parameters thus using the parameters as local variables such assignments have no effect as seen by the caller since parameters are passed by value Therefore ESC Java interprets occurrences of formal parameters in postconditions as denoting the original pre state actual parameter values A single routine declaration may be modified with any number of ensures pragmas The effective postcondition is the conjunction of all the postconditions given but any resulting warning message indicates the specific ensures pragma giving rise to the warning and warnings arising from each pragma can be suppressed individually In a postcondition an expression of the form old x where x is a specification expression denotes the value denoted by x except that 1 any occurrence in x of a target field see section 2 3 1 0 of the routine is interpreted according to the pre state value of the field
7. supplying an axiom pragma see section 2 4 2 about the lock order as in the following example public class Tree public monitored Tree left right public monitored non_null Thing contents axiom forall Tree t t left null gt t lt t left axiom forall Tree t t right null gt t lt t right Tree non_null Thing c contents C requires max lockset lt this public synchronized void visit contents mungle if left null left visit if right null right visit Fine points Note that the axioms above are inconsistent if a so called Tree can in fact be cyclic Note also that inconsistency or incompleteness can arise from the possible mutation of variables mentioned in the axioms namely the fields left and right For example given the axioms above ESC Java will generate a spurious Deadlock warning for the following method requires max lockset lt this public synchronized void wiggleWoggle Perform a rotation on this right but give up and just return if this right or this right left is null Li this this le ee x fave v gt v y u x i IN u w w y Tree x this right if x null return synchronized x Tree v x left if v null return synchronized v x left v right v vright x this rig
8. JLS 10 10 15 25 1 which ESC Java treats as an error The ArrayStoreException cannot arise in the method if the parameter a always has actual type exactly T The programmer can express this intention with the pragma requires elemtype typeof a type T or equivalently with the pragma requires typeof a type T Note that requires typeof a type T would not be legal since the form ng makes sense only when wis a specification type not a specification expression of type TYPE A weaker but still sufficient precondition for avoiding the ArrayStoreException would be to require that the array a merely have an actual element type adequate to hold the value of x This precondition is expressed by the pragmas requires x null typeof x lt elemtype typeof a Note that the pragma requires x null x instanceof elemtype typeof a is not legal since the right hand argument of instanceof must be a type not a specification expression of type TYPE 3 2 5 lockset The special identifier lockset is a specification expression of type LockSet It denotes the set of locks held by the current thread 3 2 6 Membership in lock sets An expression of the form s z where sis a specification expression of type LockSet and Lisa specification expression of a reference type is a specification expression of type boolean It denotes that Lis amember of s
9. UNIX is a registered trademark in the United States and other countries exclusively licensed through X Open Company Ltd Windows is a registered trademark of Microsoft Corporation PostScript is a registered trademark of Adobe Systems Inc All other trademarks or registered trademarks mentioned herein are the property of their respective holders Abstract The Compaq Extended Static Checker for Java ESC Java is a programming tool that attempts to find common run time errors in Java programs by static analysis of the program text Users can control the amount and kinds of checking that ESC Java performs by annotating their programs with specially formatted comments called pragmas This manual is designed to serve both as an introduction to ESC Java and as a reference manual It starts by providing an overview of ESC Java through an 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 2 of 86 illustrative example of its use and a summary of its features and then goes on to document all the pragmas supported by ESC Java and all the kinds of warnings that it generates Appendices provide a brief sketch of ESC Java s implementation information about obtaining ESC Java and some discussion of its limitations Preface The Compaq Extended Static Checker for Java ESC Java is a programming tool that attempts to find common run time errors in Java programs by static analysis of
10. and 2 if any modification target of the routine has the form A i or A then all array accesses within x are interpreted according to the pre state contents of arrays Note that in the normal postcondition of a non void method result always refers to the method s result even when result occurs in an argument to old Similarly occurrences of this in a normal postcondition of a constructor always refer to the constructed object See sections 2 3 3and 3 2 15 for further discussion of the semantics of old It is a source of potential unsoundness for a postcondition to mention a variable that might not be spec accessible section 3 3 to an override of that method and ESC Java may forbid such postconditions In particular ESC Java forbids postconditions of a method that mention private variables except when the routine is static is final is private or is declared in a final class or when the private variables mentioned are declared spec_public section 2 5 0 The current ESC Java doesn t forbid for example postconditions of public methods from mentioning package variables but future versions of ESC Java may not be so lenient A method declaration that overrides another method declaration cannot be modified with an ensures pragma but inherits the postconditions of the overridden method See also the also_ensures pragma described in section 2 3 5 Since Java guarantees that a constructor call returns a newly allocated object ESC Ja
11. expressions JLS 19 12 3 2 10 forall An expression of the form forall T v E where Tis a specification type see section 3 0 vis a nonempty comma separated list of identifiers called bound variables and is a specification expression of type boolean is a specification expression of type boolean It denotes that is true for all substitutions of values of type r for the bound variables If ris a reference type the quantification ranges only over allocated objects that are instances of r Note that this excludes nu11 If ris either of the types int or long then the quantification ranges over all mathematical integers regardless of whether they are in the ranges of possible values for Java variable of those types Fine points Just as Java forbids declaration of an identifier as a local variable within the scope of a parameter or local variable of the same name JLS 14 3 2 so ESC Java forbids declaration of an identifier as a bound variable within the scope of a parameter local variable or bound variable of the same name ESC Java also forbids declaration of lockset or result as a bound variable The same restriction applies to variables bound by exists section 3 2 11 If a specification expression has an application of forall as a not necessarily proper subexpression then may occur only in one of the following contexts e as an neuer argument to one of the following operators the ESC Java implication op
12. v grep classpath on Unix systems or escjava classpath xxx v find classpath on Windows systems 5 1 2 Specification spec files There are times when the specification that ESC Java can derive automatically from a class file is inadequate but when it is inconvenient or impossible for the user to add pragmas to the java source file For example the user s file system may not contain a copy of the java file In such situations the user can supply the needed pragmas in ESC Java specification spec files which are similar to java source files except that 1 ESC Java always uses spec only mode when reading a specification file so routine bodies may always be omitted from specification files and 2 a specification file T spec may contain a declaration of only the single type T Since Java compilers do not look for files with extension spec one can use the same class path for the Java compiler as for ESC Java with no danger of inadvertently pointing the compiler at a crippled source file Caveat When ESC Java reads a spec file it does not check that the contents of that file are in any way consistent with those of a java or class file that a compiler might find on the same class path 5 1 3 How ESC Java decides which files to read and in which modes In this section we describe how ESC Java decides which files to read and which modes to read them in The short version of the story is that ESC Java uses its c
13. 2 0 about the need for judgment regarding the use of assume pragmas are at least equally applicable to nowarn pragmas 2 2 3 A helpful tip Experiments with assert and assume pragmas can help you understand ESC Java s behavior and debug your annotated code As illustrated in the example of section 0 using ESC Java will often be an iterative process You run ESC Java on your program it reports some warnings you address the warnings by changing either the Java code itself or the annotations you run ESC Java again and so on until ESC Java reports no warnings At some point in this process you may find that you can t figure out why ESC Java is issuing some warning or why the change you made to address some warning isn t making the warning go away In such cases experiments with assert and assume pragmas can be useful in the same way that displaying intermediate results is useful in ordinary debugging Suppose for example that the problem seems to be that ESC Java is missing some critical fact that should be obvious You might try adding an assert pragma for the supposedly obvious fact and see whether ESC Java really warns that the assert could fail Or you might try adding an assume pragma to see whether supplying the supposedly critical missing fact really eliminates the warning Such experiments can also clarify your own understanding of your program Consider for example the situation described in section 0 7 where ESC Java contin
14. 2 3 0 requires pragma A requires pragma is a routine modifier pragma It has the form requires E i opt where is a boolean specification expression The pragma makes a precondition of the routine the pragma modifies When checking the body of the routine ESC Java assumes that holds initially When checking a call to the routine ESC Java issues a warning if it cannot establish that holds at the call site Fine points If the routine is synchronized then is assumed to hold before acquisition of the lock If the routine is a constructor then is assumed to hold before the implicit superclass constructor call if any and thus also before execution of instance variable initializers Except for the formal parameters of the routine the variables mentioned in must be spec accessible see section 3 3 anywhere the routine itself is accessible For example a precondition of a public method may not mention a private variable unless the variable is declared spec_public see section 2 5 0 A method declaration that overrides another method declaration cannot be modified with a requires pragma but inherits the overridden method s preconditions as described above Multiple inheritance can lead to unsoundness in some cases as discussed in section C 0 5 A single routine declaration may be modified with any number of requires pragmas The effective precondition is the conjunction of all the preconditions given but any resulting
15. 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 30 of 86 exsures T E i opt where Tis a subtype of java lang Throwable t if included is a an identifier and is a boolean specification expression The identifier t if included is in scope in where it has type r The pragma makes an exceptional postcondition of the routine the pragma modifies That is it specifies that z holds whenever the routine completes abruptly by throwing an exception t whose type is a subtype of T When checking the body of the routine ESC Java checks that holds whenever the routine completes abruptly by throwing an exception t whose type is a subtype of 7 When checking code that calls the routine ESC Java assumes that the holds just after the call if the call completes abruptly with an exception whose type is a subtype of T Fine points Like normal postconditions exceptional postconditions of synchronized methods apply to the state after the release of the lock The identifier t may not be the same as any formal parameter of the routine and quantified expressions see sections 3 2 10 and 3 2 11 within may not use t as a bound variable name The expression can include uses of fresh and old which have the same semantics as in an ensures pragma However cannot mention result since an abruptly terminating routine invocation returns no result Similarly cannot mention this if the ex
16. 33 were not present This behavior could be quite confusing for a user attempting to use assert pragmas as a debugging aid as suggested in this section We have since made changes to ESC Java to prevent such behavior or at least greatly reduce its likelihood If you observe a case where addition of an assertion inhibits ESC Java from warning about a potential error earlier in the execution path we would like to know about it See the instructions on reporting bugs in appendix B 2 3 Pragmas for specifying routines In this section we describe those pragmas called routine modifier pragmas that explicitly supply specifications for individual routines Fine points The reader should be aware that these pragmas are not the only ones that give rise to routine specifications In this regard we direct the reader s attention particularly to the descriptions of the non_null and invariant pragmas in sections 2 4 0 and 2 4 1 as well as to the description of the axiom pragma in section 2 4 2 All routine modifier pragmas have a number of properties in common ESC Java allows modifiers for a routine declaration to appear not only in the usual place for modifiers near the beginning of the declaration but also just before the opening left brace of the routine s body or before the final semicolon if there is no body as in an interface abstract class or sometimes in a spec file see section 5 1 2 For example the requires pragma that we introdu
17. A m and B m where c is a class and either a and B are both be interfaces that c implements or one is an interface that c implements and the other is a class that c extends and suppose that some method r contains a call of the form m where has static type a but might evaluate at run time to a value of type c When checking the body of c m ESC Java will assume that all preconditions for m declared in or inherited by either a or 8 hold initially On the other hand when checking the call m in the body of r where expression has static type a ESC Java will only check the preconditions of A m and not those of B m Similarly when ESC Java checks code after the call it will assume that the call modifies at most the modification targets specified for A m This would be a source of unsoundness even if ESC Java checked that the body of c m modified only its declared modification targets C 0 6 Arithmetic overflow ESC Java reasons about integer arithmetic as though machine integers were of unlimited magnitude This is both an unsoundness and an incompleteness but it simplifies the checker and reduces the annotation burden for the user while still allowing ESC Java to catch many common errors The Simplify theorem prover used by ESC Java see appendix A includes a decision procedure for linear rational arithmetic based on the simplex algorithm If integer operations in Simplify s simplex module result in overflows they w
18. Java release includes spec files for only a few JDK libraries and even the spec files supplied do not fully capture the informal semantics of the specified routines see also section C 0 10 According to rules of the Java type system if neither of two distinct classes s and T is a subtype of the other then s and r have no non null instances in common ESC Java s modeling of the Java type system is good enough to enforce this disjointness for explicitly named types but not for all types such as the dynamic element types of array variables As mentioned in section C 0 6 the Simplify theorem prover may exhibit unsoundness due to integer overflow In order to reduce the likelihood of overflow occurring in the prover ESC Java treats all integer literals of absolute magnitude greater than 1000000 as symbolic values whose relative ordering is known but whose exact values are unknown Thus ESC Java can prove the assertions 2 2 4 and 2000000 lt 4000000 but not 2000000 2000000 4000000 While ESC Java recognizes the Java 1 2 expressions of the form T class where ris a Java Type JLS 19 4 ESC Java s semantics for such expressions is extremely limited For example ESC Java can determine that int class is a non null instance of java lang Class but not that it is distinct from short class or even that it is equal to Integer TYPE The implementers of ESC Java currently have no plans to significantly strengthen its semantics for java lang Cla
19. Simplify reaches its time limit after reporting one or more potential counterexamples then ESC Java will issue one or more warnings but perhaps not so many warnings as it would have issued if the time limit were larger You can set the time limit to n seconds where n is a positive integer by setting the environment variable PROVER_KILL_TIME to n If PROVER_KILL_TIME is not set ESC Java sets it to 300 before invoking Simplify There is also a bound on the number of counterexamples that Simplify will report for any conjecture and 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 83 of 86 thus on the number of warnings that ESC Java will issue for any routine You can set the bound to a positive integer n setting the environment variable PROVER_CC_LIMIT to n If PROVER_CC_LIMIT is not set ESC Java sets it to 10 before invoking Simplify C 0 15 Integer arithmetic bug in Simplify Simplify includes a complete decision procedure for linear rational arithmetic and some heuristics for integer arithmetic We have recently learned that one of the procedures implementing the integer arithmetic heuristics is buggy in a way that leads to unsoundness This unsoundness in not one that we intended to design into the checker and we are investigating the problem further For an unrelated source of unsoundness the discussion of arithmetic overflow in section C 0
20. The Java Specification Language by James Gosling Bill Joy and Guy Steele JLS supplemented by the Inner Classes Specification ZCS except for some limitations described in section 6 of this manual ESC Java has a command line interface like the Java compiler s An invocation of ESC Java has the form escjava options sourcefiles The escjava 1 man page in the ESC Java release see appendix B includes descriptions of ESC Java s command line options and of environment variables that affect ESC Java s operation For now we mention only the cLASSPATH environment variable whose effect on ESC Java is similar to its effect on javac 5 and the suggest command line option which causes ESC Java to offer suggestions of pragmas that might eliminate certain kinds of warnings Section 5 contains further description of these features but not all command line options and environment variables 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 14 of 86 e ESC iayas issues warning messages for potential run time errors o The current ESC Java checks only method and constructor bodies The current ESC Java provides no warnings for potential run time errors in static initializers JLS 8 5 or in initializers for static fields or in anonymous classes o ESC Java treats exceptions thrown by the Java run time system as run time errors Some of the potential error conditi
21. User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 34 of 86 Fine points ESC Java does not fully enforce the discipline just described partly because it would be too strict for many programs which may have legitimate reasons for temporarily breaking object invariants and partly because such checking would be very expensive Instead it performs less expensive and potentially unsound checking Essentially ESC Java assumes object invariants for all objects on entry to a routine body and checks objects invariants for all objects at the end of the body however at call sites ESC Java checks object invariants only for parameters and static fields and assumes of the call only that it doesn t break any object invariants and that it establishes object invariants for freshly allocated objects More precisely when checking the body of a routine R ESC Java chooses from all available object invariants a set of invariants to be considered relevant to the checking of R The heuristic used to choose the relevant object invariants is fairly complicated and subject to change so we don t explain it in this manual ESC Java assumes that at the start of R s body all relevant static invariants hold and all relevant instance invariants hold for all allocated objects For every routine call in the body of R ESC Java checks that all relevant to R static invariants hold before the call ESC Java checks that the va
22. User s Manual http gatekeeper research compaq com pub DEC SRC technical notes Note 1997 007 January 1997 Available on the web at http gatekeeper dec com pub DEC SRC technical notes abstracts src tn 1997 007 html Cited in sections 2 3 4 2 4 1 and C 0 2 LS99 K Rustan M Leino and Raymie Stata Virginity A contribution to the specification of object oriented software Information Processing Letters 70 1999 pages 99 105 Cited in fine points of section 3 2 17 Reflection Reflection section of JDK documentation Sun Microsystems on the web at http java sun com products jdk 1 1 docs guide reflection Cited in section C 1 1 SLSOO Silvija Seres with K Rustan M Leino and James B Saxe ESC Java Quick Reference Compaq SRC Technical Note 2000 004 October 2000 Available on the web at http gatekeeper dec com pub DEC SRC technical notes abstracts src tn 2000 004 html Cited in the preface and acknowledgments 86 of 86 08 02 2005 17 56
23. classpath command line option if any on the command line or else e the value of the CLASSPATH environment variable if one has been set or else e a default value and bootclasspath is e the argument of the bootclasspath command line option if any on the command line or else e a default value The default values of classpath and bootclasspath are subject to change At the time of writing the T WW default classpath is and the default bootclasspath includes a directory of selected spec files see 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 73 of 86 section 5 1 2 for selected library classes and interaces together with directories for the normal Java system libraries the same default versions used by srcjava 1 Fine point If a command line contains multiple occurrences of the classpath option as in escjava classpath P1 classpath P2 sourcefiles only the last one P2 in the example is used The same applies for multiple occurrences of bootclasspath Tip The v verbose command line option makes ESC Java output various information including the full classpath Thus you can learn the current default value of either classpath Or bootclasspath at your site by setting the other to a known value and looking for the other in the output produced with v For example you can learn the value of boot classpath by typing escjava classpath xxx
24. do and you may make better use of its capabilities by employing a less extreme and more fine grained treatment of unchecked exceptions Suppose for example that your program calls a library method with the declaration Returns the element wise sum of a and b Throws a NullPointerException if either a or b is null Throws an IndexOutOfBoundsException if a and b are not of the same length public static int add int a int b throws NullPointerException IndexOutOfBoundsException gu and that it is your intention never to supply arguments that give rise to exceptions and therefore not to bother with code to detect and handle the exceptions at run time In this case you might get some useful checking from ESC Java by creating a spec file see section 5 1 containing a declaration for aaa with the throws clause removed and a requires pragma supplied in its place JAE os lt esc gt requires a null amp b null amp amp a length b length lt esc gt xx public static int add int a int b Alternatively you might supply exsures pragmas specifying the conditions under which the exceptions may be thrown lt esc gt exsures NullPointerException a null b null exsures IndexOutOfBoundsException a null amp b null amp amp a length b length 66 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Man
25. f owner this then it follows that at any point where the invariant holds we cannot have x y f for two distinct objects x and y of type T since the conditions x f owner x y f owner y together with x f y f would imply x y Example Here is an example of a situation in which it is useful to specify that a field is unshared Note Understanding this example may require more than a cursory reading While we usually relegate such material to sections marked Fine points the scenario described here is of a sort that most ESC Java users are likely to encounter as soon as they try to check code with invariants of any complexity specifically invariants involving both 1 quantification including the quantification implicit in all instance invariants and 2 indirect references like x f g or x a i including cases where an expression like g or ati implicitly means this f g Or this a i A few minutes working through the details with pen or pencil in hand will lead to clear understanding and the time will be well spent Consider the following class whose instances represent stacks of objects to keep the example simple we put a fixed limit of 10 on the size of a stack Input from file ObjStack java 1 class ObjStack 2 non_null Object a 3 invariant a length 10 4 invariant elemtype typeof a type Object 5 int n invariant 0 lt n amp n lt 10 6 invariant
26. in the loop invariant An iteration of a loop includes the termination test and also includes the update code in a for loop Thus loop_invariant E while B S intuitively means while true assert E but giving a LoopInv warning if B break S however see the comments below about loop unrolling Note that the checking of the loop invariant applies to the state before the test of B and before any side effects in the evaluation of B Likewise loop_invariant E do S while B intuitively means 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 37 of 86 while true do assert E but giving a LoopInv warning S if B break and loop_invariant E Gs EO I1y ssy dme By Ulz mz Un S intuitively means t Tip sa Im L while true assert E but giving a LoopInv warning if B break S Uly s p Uns but with any occurrence within s of continue L or simply of continue appearing outside of any nested loop and thus meaning continue 1L transferring control only to the end of s rather than to the end of un In ESC Java loop invariants are optional The checker considers only execution paths in which the loop body is executed at most once and the test for being finished is executed most twice rather than the potentially infinite numbe
27. invariant forall int i n lt i amp i lt 10 gt a i null a Possibly relevant items from the counterexample context 0 lt brokenObj lt 2 gt n 15 6 brokenObj refers to the object for which the invariant is broken Suggestion 16 2 perhaps declare instance invariant invariant this a owner this in class ObjStack near associated declaration at ObjStack java line 6 col 6 Fine points ESC Java does not supply suggestions for all warnings and the suggestions that it does supply are heuristically chosen and may be incorrect For example if the contents of file c java are 1 class C 3 int n 4 5 static int m C a C b 6 if a null 73 return a n 8 else 9 return b n 10 11 12 then the command escjava suggest C java will give a warning about and possible null dereference on line 9 accompanied by the suggestion Suggestion 9 14 perhaps declare parameter b at 5 22 in C java with non null It might actually be better to declare the method m with the precondition requires a null b null since it might be the intention of the programmer to support callers that meet only this precondition and not necessarily the more stringent condition that b always be non null Despite its limitations the suggest option can be of considerable help to users in paring down the initial batch of mostly spurious warnings that ESC Java
28. it to prove each body s verification given the appropriate background predicate If an attempted proof succeeds or if Simplify exceeds specified resource limits in attempting the proof or if ESC Java exceeds specified resource limits generating the verification condition then ESC Java reports no warnings for the body If the proof fails other than by exceeding resource limits Simplify produces a potential counterexample context from which ESC Java derives a warning message Fine points The command line option counterexample makes ESC Java print selected parts of each counterexample sugared into a somewhat Java like syntax For example in section 3 2 17 we gave an example file D java and said of ESC Java s output There is no way to tell from this message whether ESC Java is warning about the case where a has nonnegative x and y fields and b has negative x and y fields or about the case where a s fields are negative and b s are nonnegative If we ran ESC Java on D java with counterexample option the output would include something like Counterexample context y 7 11 a pre 3 6 lt 0 lt x 7 6 b 3 9 y 7 11 b 3 9 lt 0 lt x 7 6 a 3 6 lt 1 gt from which one can infer that ESC Java happens to be reporting the former case As you may also infer from the excerpt above the counterexample option is intended mainly for expert users to give further details about deciphering counterexample contexts fo
29. libraries that it includes The current release of ESC Java includes spec files for a subset of the standard libraries This subset is far from complete but the spec files that are included in the release are intended to correspond to classes and interfaces that are standard for Java 1 2 Fine point While ESC Java accepts almost all of the language constructs described in JLS and JCS the semantics ESC Java ascribes to those constructs differs in numerous details including but not limited to those mentioned in appendix C and other parts of this manual from the semantics specified in JLS and JCS Likewise the annotations in the spec files available in the ESC Java release may fail for various reasons to capture the semantics of the actual JDK libraries see section C 0 10 Appendix A Overview of how ESC Java works This appendix gives a very rough sketch of ESC Java s internal operation The operation of ESC Java consists of the following steps First ESC Java loads parses and type checks the files named on the command line as well as any other files needed because their contents are directly or indirectly used by files name on the command line Section 5 1 describes where ESC Java looks for files not named on the command line Next for each class whose routine bodies are to be checked ESC Java generates a type specific background predicate encoding such information as subtype relations types of fields etc in th
30. line by the Java interpreter in which case args will be non null and all its elements will be non null However it is legal for a Java program to contain explicit calls to main and the value of args supplied by such a call might in some cases be either nu11 or an array containing nu11 as an element It is often helpful to annotate main as follows requires nonnullelements args static public void main String args Given this annotation 1 ESC Java will assume when checking the body of main that args and all its elements are non null and 2 ESC Java will check that any explicit calls to main supply a non null argument with only non null elements Fine points 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 54 of 86 Since an application of nonnullelements does not explicitly include a quantifier it may be used as an argument to and may occur inside an argument of old Note that if ais of type T 1 then nonnullelements A implies that a i is non null if i is in bounds but not necessarily that any Ati j is non null 3 2 13 fresh An expression of the form fresh z where is a specification expression of a reference type is a specification expression of type boolean In a postcondition it denotes that is non null and was not allocated in the pre state of the routine call See also section 2 3 2 3 2 14 re
31. never checks for some kinds of errors such as arithmetic overflow or infinite looping Also ESC Java doesn t check programs for functional correctness properties other than those given by the user in pragmas Finally even when ESC Java checks for a particular kind of errors there may be situations in which it erroneously concludes that the error cannot occur and therefore fails to issue a legitimate warnings In the jargon of proof theory we say that ESC Java viewed as a system for proving program correctness is unsound Section C 0 describes the known sources of unsoundness in ESC Java o ESC Java can give spurious warnings Conversely when ESC Java issues a warning it doesn t necessarily indicate the presence of an error it merely means that ESC Java is unable to conclude that the indicated error will never occur given the annotations that the user has supplied In the jargon ESC Java viewed as a system for proving program correctness is incomplete Section C 1 describes the main sources of incompleteness in ESC Java gt Pragmas give the user some control over ESC Java s unsoundness and incompleteness ESC Java provides pragmas that let the user eliminate spurious warnings that is reduce ESC Java s incompleteness either without loss of soundness as for example the requires pragma we wrote in section 0 2 eliminated the warning about a potential dereference of nu11 in the Bag constructor by imposing a precondition on calls or
32. of special types for example TyPE In the current ESC Java the programmer cannot mention LockSet explicitly 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 3 1 Restrictions Specification expressions must be free of subexpressions that in general may have side effects In particular specification expressions may not contain any e assignment etc e pre increment pre decrement post increment post decrement or e array or object creation new or e method invocation Method invocations are forbidden in specification expressions even when the method is known to have no side effects The next section describes additional constructs that are allowed in specification expressions beyond those allowed in Java expressions Some of these constructs have restrictions on their use We describe these restrictions together with the descriptions of the constructs to which they apply 3 2 Additions 3 2 0 type An expression of the form t ype T where Tis a specification type see section 3 0 is a specification expression of type TYPE It denotes the type T 3 2 1 typeof A specification expression of the form typeof E where is a specification expression whose type is a reference type is a specification expression of type TYPE It denotes the dynamic type of the value of The value of t ypeof E is unspecified whe
33. of some sort though alas not the clearest warnings that one could hope for o ESC Java warning messages may include execution traces Associated with each ESC Java warning message is some execution path that so far as ESC Java can determine may plausibly lead to the run time error mentioned in the warning If certain kinds of interesting events occur on this execution path the message will contain an execution trace listing those events See section 4 0 for details about which events are considered interesting Section 4 of this manual includes descriptions of all ESC Java warning messages e ESC Java issues error messages for badly formed programs Before ESC Java can analyze a program for potential run time errors it must first perform operations such as parsing name resolution and type checking both of the Java code and of any pragmas When ESC Java detects an illegal construct such as the syntactically incorrect pragma shown in section 0 8 above during this preliminary processing it issues an error message Error messages are distinguished from warning messages by the occurrence of the word Error instead of Warning near the beginning of the message Only when its input is free of such errors can ESC Java go on to look for potential run time errors and generate warnings just as a compiler a object code only when the source code is free of compile time errors o ESC Java error messages are like compiler error messages
34. old x f and old x and between old a old i and old a i Note also that while ESC Java does not allow the notation x old to mean the original f field of the current value of x in the pragma the same effect is achieved by the expression old z within the pragma ensures exists C z z x amp old z f old y f For further discussion of old including the interaction of ola and modifies see sections 2 3 2 and 233 3 2 16 lblneg and 1blpos This section may be skipped on first and second reading It describes incompletely a feature of included mainly for use by the implementers An expression of the form lblneg n E Or lblpos n E where is a specification expression of type boolean and n is an identifier called an expression label is a specification expression of type boolean Logically the labeled expression 1b1neg n E or lblpos n E denotes the same thing as E but when ESC Java issues a warning the warning message will mention the label n if in the execution path associated with the warning the expression would evaluate to false resp true ata point where the containing pragma is relevant and in circumstances where the value of the expression is relevant to the pragma as a whole The details of the heuristic definition of relevant are beyond the scope of this manual and are subject to change 55 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual h
35. owner field is non null 4 15 Post warning A Post warning warns that a routine body may fail to establish some normal postcondition on terminating normally or some exceptional postcondition when terminating by throwing an exception of a relevant type The warning is associated with the ensures exsures also_ensures Of also_exsures pragma that gives the potentially violated postcondition Tips If a Post warning seems mysterious the problem might be that the programmer intended to refer to the post state value of some field but forgot to include a modifies or also_modifies pragma naming that field as a target See section 2 3 3 for further discussion of this point It can also be useful to examine the execution trace that accompanies the warning For example you might see that the trace reported be ESC Java involves execution of a return statement in the middle of the method that you had overlooked 4 16 Pre warning A Pre warning warns that control may reach a routine call when some precondition of the routine does not hold The warning is associated with the requires pragma that gives the potentially violated precondition 4 17 Race warning A Race warning warns of a possible attempt to access a monitored field while not holding the requisite lock s The warning is associated with the monitored or monitored_by pragma giving the lock s that should be held Bug limitation If there are multiple monitored and or monitored_by pragma
36. parts of this manual where various topics are discussed in more detail e ESC Java is a checker for Java programs optionally annotated with user supplied pragmas o ESC Java pragmas must occur within pragma containing comments 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 13 of 86 We showed some examples of pragma containing comments in section 0 Section 2 includes all the rules about where the various kinds of pragmas are allowed o ESC Java pragmas can contain expressions that are similar to Java expressions The ESC Java specification language that is the language of ESC Java pragmas includes expressions which we call specification expressions or SpecExpr s While the syntax name resolution and type checking rules for specification expressions are similar to those for ordinary Java expressions there are inevitably some differences The rules for specification expressions are described in section 3 of this manual o ESC Java pragmas record programmer design decisions In addition to giving the user control over ESC Java pragmas serve to record formally some of the programmer s intentions about the function and use of methods constructors and variables for example that the Bag constructor of our example in section 0 was meant never to be called with a nu11 argument These are the same sorts of intentions that good programmers may already record informal
37. pragma An also_exsures pragma is a routine modifier pragma It has the form also_exsures T t E opt 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 31 of 86 or also_exsures T t E opt where Tis a subtype of java lang Throwable t if included is a an identifier and is a boolean specification expression An also_exsures pragma has the same semantics and must obey the same syntactic restrictions as an exsures pragma but may appear as a modifier only of a method declaration that overrides another method declaration while overriding method declarations are forbidden to have exsures pragmas The relationship between also_exsures and exsures is exactly analogous to that between also_ensures and ensures 2 3 7 also_requires pragma An also_requires pragma is a routine modifier pragma It has the form also_requires E j opt where is a boolean specification expression An also_requires pragma has the same semantics as a requires pragma but the declaration of a method c m may be modified by an also_requires pragma only if all three of the following conditions hold e cis a class not an interface e the declaration of c m overrides some method declaration in a superinterfaces of c and e the declaration of c m does not override any method declaration in a superclass of c By contrast a requires pragma may only modify a method or construct
38. recommend that non_nu11 pragmas be used in preference to semantically similar requires and invariant pragmas except in cases where the somewhat stricter semantics of non_null makes its use untenable Limitation Since the current ESC Java does not check static bodies and static initializers it is entirely the user s responsibility to ensure that static fields declared as non_nu11 are in fact initialized to have non null values 2 4 1 invariant pragma An invariant pragma is a declaration pragma It has the form invariant E opt where is a boolean specification expression The pragma declares E to be an object invariant of the class within whose declaration the pragma occurs If z mentions this either explicitly or implicitly then Eis Said to be an instance invariant otherwise is a static invariant Roughly speaking all object invariants are supposed to hold at all routine call boundaries That is 1 if z an instance invariant of class T then forall T t Ethis t should be true at all routine calls and returns where t is a variable not occurring in the universal quantification ranges over all allocated instances T and Etnis t 1s the result of substituting t for all explicit and implicit occurrences of this in z and 2 if is a static invariant of class T then should be true at all routine call boundaries regardless of whether or not any allocated objects of class T exist 08 02 2005 17 56 ESCJ 27 ESC Java
39. routine releases and then reacquires the lock that protects it ignoring the possibility that some other thread might have acquired the lock and modified the variable in the interim C 0 12 Initialization of fields declared non_nu11 There is an unsoundness in ESC Java s checking that constructors assign non null values to fields declared non_null Consider the following program 1 class C 2 non_null Object f 4 C 5 m 6 7 8 modifies this f 9 void m When checking the implementation of the constructor for c ESC Java will assume based solely on the pragmas on lines 2 and 8 that the method m returns with this f set to a non null value While checking the body of m ESC Java will check that any assignments to f indeed assign non null values However if the body of m can complete normally without assigning to this then ESC Java s assumption that this f is always non null after line 6 will be unsound C 0 13 String literals Java s treatment of string concatenation see JLS 3 10 5 is not accurately modeled by ESC Java This is a source both of unsoundness and of incompleteness C 0 14 Search limits in Simplify If Simplify cannot find a proof or a potential counterexample for the verification condition see appendix A for a routine within a set time limit then ESC Java issues no warnings for the method even though it might have issued a warning if given a longer time limit If
40. the possibility that x might fail the warning may also be issued because the annotations are inadequate to imply that x holds because the theorem prover s deductive power is inadequate to complete the proof or because ESC Java s model of Java semantics is incomplete 2 0 Rules about where pragmas may occur 2 0 0 ESC Java pragmas must occur within pragma containing comments ESC Java looks for pragmas within certain specially formatted comments Specifically e When the character e is the first character after the initial or of a Java comment ESC Java expects the rest of the comment s body to consist entirely of a sequence of zero or more ESC Java pragmas e Inside a documentation comment JLS 18 a sequence ESC Java pragmas can be bracketed by lt esc gt and lt esc gt Many pragmas end with an optional semi colon opr If such a pragma is followed by another pragma in the same pragma containing comment then this semi colon is required 2 0 1 There are four syntactic categories of pragmas Pragmas are divided into four syntactic categories according to the places in a program where they can sensibly be used All pragmas in any single pragma containing comment must be of the same syntactic category e Lexical pragmas may occur anywhere that ordinary Java comments may occur It would be more accurate to say that ESC Java allows the occurrence of a pragma containing comment whose body is a sequence of zero or more le
41. the form assert E opt where is boolean specification expression The pragma causes ESC Java to issue a warning if it cannot establish that z is true whenever control reaches the pragma 2 1 2 assume pragma An assume pragma is a statement pragma It has the form assume E opt where is boolean specification expression The pragma causes ESC Java to assume that is true whenever control reaches the pragma In other words for any execution path in which z is false when control reaches the pragma ESC Java ignores the path from that point on Example The usual purpose of an assume pragma is to supply ESC Java with some piece of information that is incapable of deducing on its own thereby preventing ESC Java from generating spurious warnings In the code fragment 22 start complicated computation guaranteed to leave i 0 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 21 of 86 46 end of complicated computation 47 assume i 0 48 if b 49 g h i 50 else 51 h g i g j 52 the assume pragma at line 147 prevents ESC Java from warning that the division by i in lines 149 and 151 may give rise to an ArithmeticException but ESC Java will still generate a warning about the division by j in line 151 unless it can deduce that j will never be zero when control reaches that point Fine points Like the nowar
42. typically produces when it is first run on a body of unannotated code A project currently under way at Compaq SRC is exploring automated techniques for inferring ESC Java annotations FLOO FJLxx 71 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 72 of 86 5 1 Specification spec files and the ESC Java s class path This section discusses the algorithm that ESC Java uses to find declarations of classes and ways in which the user can control that algorithm In order to check the routine bodies of a class c ESC Java may need various information about some other type class or interface 7 This information which we call the specification of T may include both information introduced by pragmas such as invariant and requires and information from the Java language such as routine signatures and types of fields but does not include routine bodies If ESC Java needs the specification for a type T and can find only a binary class file and no source file for T then it can produce a simple specification based on the signature and type information included in the binary file ESC Java can also obtain specifications from specification spec files see section 3 1 2 5 1 0 File reading modes ESC Java has two modes for reading files full mode and spec only mode In order for ESC Java to check the routine bodies in a file it must read the file in full mo
43. where D is a ghost designator and is a specification expression containing no quantifiers or labels The pragma has the same semantics as the Java assignment statement p would have if D and were in Java A ghost designator can have one of the following forms o where o is specification expression of an object type rand Ff is a ghost field of T f where fis a static ghost field or this fis a legal ghost designator of the preceding form Fine point If the field f assigned to by a set pragma is declared with a non_null monitored Or monitored_by pragma then ESC Java will perform the usual checking implied by the modifier pragma generating warnings in case the value being assigned may be nu11 or in case the specified lock may not be held This is the only circumstance in which the current ESC Java generates warning of possible run time errors in the evaluation of pragmas 2 6 2 Examples using ghost variables Example specifying Bag without revealing its implementation As pointed out in section 2 5 0 there is a scoping problem with the Bag example from section 0 Ina realistic situation the implementer of the Bag class may want to make public the routines of the class but not the fields How then are clients of the public method ext ractMin to discharge the precondition requires n gt 1 which mentions the non public field n In section 2 5 0 we showed how to address the problem by declaring n with a spec_public pragma
44. 0 4 Scene 4 We correct a bug in Bag extractMin 0 5 Scene 5 We take no action for a redundant warning 0 6 Scene 6 We supply a precondition for Bag extractMin 0 7 Scene 7 We run ESC Java again and it still issues a warning 0 8 Scene 8 We supply an invariant pragma relating n to a lenght sic 0 9 Scene 9 ESC Java notices a typographical error 0 10 Scene 10 Our efforts come to a happy conclusion 1 An overview of ESC Java and of this manual e ESC Java is a checker for Java programs optionally annotated with user supplied 3 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes pragmas o ESC Java pragmas must occur within pragma containing comments o ESC Java pragmas can contain expressions that are similar to Java expressions o ESC Java pragmas record programmer design decisions o ESC Java s pragmas support modular checking o When Java sources are unavailable users can supply pragmas in spec files e ESC Java is checker for almost all of Java 1 2 e ESC Java has a command line interface like the Java compiler s e ESC Java issues warning messages for potential run time errors o The current ESC Java checks only method and constructor bodies o ESC Java treats exceptions thrown by the Java run time system as run time errors o ESC Java does not warn of potential errors in the evaluation of specification expressio
45. 6 C 0 16 Quantifiers and allocation When Tis a reference type specification expressions of the forms forall T t and exists T t sections 3 2 10 3 2 11 quantify over allocated instances of r If a method allocates new objects but is not annotated with a postcondition mentioning containing an occurrence of fresh section 3 2 13 or old section 3 2 15 ESC Java may infer unsoundly that some property holds for all allocated objects after completion of a call when the property may in fact not hold for objects allocated during the call This unsoundness results from a performance optimization and seems rarely to result in problems missing warnings in practice C 1 Some sources of incompleteness An incompleteness is a circumstance that causes ESC Java to warn of an potential error when it is in fact impossible for that error to occur in any run of the program it is analyzing Because ESC Java attempts to check program properties that are in general undecidable some degree of incompleteness in inevitable In addition ESC Java s implementers have been willing to accept some evitable incompleteness in order to improve performance and keep the tool simple We list here some principal sources of incompleteness in ESC Java but we do not attempt a complete enumeration of sources of incompleteness C 1 0 Incompleteness of the theorem prover The verification conditions that ESC Java give to the Simplify theorem prover are in a
46. 98 Available on the web by permission of the ACM in PostScript at ftp ftp digital com pub DEC SRC publications rustan krm183 oopsla98 ps and in PDF at ftp ftp digital com pub DEC SRC publications rustan krm183 oopsla98 pdf Cited in sections 2 3 8 and C 0 4 LLPRJOO Gary T Leavens K Rustan M Leino Erik Poll Clyde Ruby and Bart Jacobs JML notations and tools supporting detailed design in Java to appear in Proceedings of the 2000 ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications OOPSLA 00 Also available as Department of Computer Science Iowa State University TR 00 15 August 2000 on the web in PDF at ftp ftp cs iastate edu pub techreports TROO 15 TR pdf and in PostScript at ftp ftp cs iastate edu pub techreports TROO 15 TR ps gz Cited in the preface LSS99 K Rustan M Leino James B Saxe and Raymie Stata Checking Java programs via guarded commands in Formal Techniques for Java Programs workshop proceedings Bart Jacobs Gary T Leavens Peter M ller and Arnd Poetzsch Heffter editors Technical Report 251 Fernuniversitat Hagen 1999 Also available as Compaq SRC Technical Note 1999 002 on the web at http gatekeeper dec com pub DEC SRC technical notes abstracts src tn 1999 002 html Cited in section 2 1 2 LS97 K Rustan M Leino and Raymie Stata Checking Object Invariants Compaq SRC Technical 08 02 2005 17 56 ESCJ 27 ESC Java
47. B In this section we describe a small number of options that are of particular importance or that seem to merit more extensive descriptions than those on the man page 5 0 suggest The suggest command line option causes ESC Java to accompany certain of its warning messages with suggestions for pragmas that may eliminate those warnings Examples Running ESC Java with the command line escjava suggest Bag java on the version of Bag java in section 0 0 will produce such suggestions as Bag java 6 Warning Possible null dereference Null n input length Suggestion 6 13 perhaps declare parameter input at 5 12 in Bag java with non_null Running ESC Java with the suggest option on the file T java from section 3 2 4 will produce the following warning and suggestion T java 5 Warning Type of right hand side possibly not a subtype of array element type ArrayStore ali x 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes A Suggestion 5 9 perhaps declare method storeObject at 4 14 in T java with requires elemtype typeof a type T Running ESC Java with the suggest option on the file objstack 4java from section 3 2 17 will produce the following warning and suggestion ObjStack java 16 Warning Possible violation of object invariant Invariant A Associated declaration is ObjStack java line 6 col 6
48. But what if the implementer of the Bag class wanted to leave open the possibility of switching to a different implementation say a linked list in which the representation of a Bag did not include an explicit count of the elements To resolve this annotation question we must first make a design decision about the actual Java code 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual 42 of 86 http gatekeeper research compaq com pub DEC SRC technical notes How in fact are the clients of the Bag class supposed to avoid ever calling the ext ractMin method of an empty Bag One approach the one that we will illustrate here would be for the implementer of the Bag class to provide a method is empty that clients could use to test a Bag for emptiness before calling its ext ractMin method To specify the semantics of the Bag class we would use a boolean ghost field empty that would be true precisely for those Bag s that contain no elements Here s how that annotated implementation of Bag might look like under this approach 1 class Bag 2 non_null int a 3 int n 4 invariant 0 lt n amp amp n lt a length 5 ghost public boolean empty 6 invariant empty n 0 7 8 requires input null 9 ensures this empty input length 0 0 public Bag int input I n input length 2 a new int n 3 System arraycopy
49. ESC Java error messages are similar to compiler error messages and we hope they will be self explanatory Thus they are not fully enumerated or described in this manual We believe that all ESC Java error messages arise either 1 from circumstances that would cause the Java compilers to report compile time errors or 2 from violations of the rules for writing pragmas as given in section 2 and section 3 o ESC Java doesn t detect all compile time errors that Java compilers detect 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 15 of 86 A number of conditions that give rise to Java compile time errors are not detected by ESC Java For example the current ESC Java does not enforce Java s definite assignment rules JLS 16 or all of Java s restrictions on access to protected variables JLS 6 6 2 Thus it is wise to run your code through a Java compiler at least once before trying to run it through ESC Java Tip Sometimes the nature of a syntax error in your program may not be immediately clear from an ESC Java error message In such cases a compiler may detect the same error and offer a better or at least different description of the problem Po A s extended static checking isn t perfect o ESC Java can miss errors When ESC Java processes a program and produces no warnings it is not necessarily true that the program is free of all errors For example ESC Java
50. ESC Java regards as comments or pragmas will be precisely those regarded as comments by Java compilers Each row of the table corresponds to a syntactic form of outer and each column corresponds to a syntactic form of inner Entries tell whether each specific form of nesting is allowed and reference notes giving any additional restrictions on allowed forms of nesting and explanations of why forbidden forms of nesting are forbidden inner IOs eae RE SEE outer inner ok 1 ok 1 ok 2 ok 2 no 3 inner ok 4 ok 4 no 5 no 5 no 5 lt esc gt inner lt esc gt ok 6 ok 6 no 5 no 5 no 5 Notes 1 ESC Java considers inner to extend to the end of the line on which it begins 2 inner must be entirely on one line because Java defines outer to end at the end of the line 3 The current ESC Java might accept this form of nesting but it is strongly deprecated There is no good reason to use it and javadoc 5 will not recognize inner as a documentation comment 4 ESC Java considers inner to extend either to the end of the line or up to the closing of outer whichever is earlier 5 These forms of nesting are forbidden because Java does not allow comments of the form to be nested inside each other Thus Java compilers would interpret the closing of inner as ending outer 6 ESC Java considers inner to extend either to the end of the line or up to the closing lt e
51. ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 1 of 86 SRC Technical Note 2000 002 October 12 2000 ESC Java User s Manual K Rustan M Leino Greg Nelson and James B Saxe COMPAQ Compaq Computer Corporation Systems Research Center 130 Lytton Avenue Palo Alto CA 94301 http research compaq com SRC Copyright 1999 2000 Compaq Computer Corporation All rights reserved Limitation of liability This publication and the software it describes are provided as is without warranty of any kind express or implied including but not limited to the implied warranties of merchantability fitness for a particular purpose or non infringement This publication could include technical inaccuracies or typographical errors Furthermore the Compaq Extended Static Checker for Java ESC Java is currently under development Compaq therefore expects that changes will occur in the ESC Java software and documentation from time to time Compaq reserves the right to adopt such changes or to cause or recommend that ESC Java users adopt such changes upon such notice as is practicable under the circumstances or without any notice in its discretion The Compaq Extended Static Checker for Java ESC Java is not a product of Sun Microsystems Inc Compaq is a registered trademark of Compaq Computer Corporation Java is a trademark or registered trademark of Sun Microsystems Inc
52. P would be the result of replacing dots in P with slashes and c is the first directory on the class path see section 5 1 1 such that file c P T spec exists 2 ina file named c P T java where P is as in 1 above and c is the first directory on the class path such that file c P T java exists 3 ina file named c P T class where P is as in 1 above and cis the first directory on the class path such that file c P T class exists 4 ina java file found by finding a file c P T class as in 3 above and reading the internal field that names the source file from which it was compiled If names of jar or zip files occur as class path components ESC Java acts is if the class path included directories holding the expanded contents of those files ESC Java s ranking of these alternatives is from most favored to least favored 0 1 2 4 3 Note that this means that for example c1 P T spec is favored over c2 P T java even if c2 precedes c1 in the class path If ESC Java doesn t have the declaration already in its cache and needs to read it from a file it will read the file in spec only mode Whenever ESC Java reads a java file in order to get the declaration of a type rT it will also read and cache any other type declarations in that file Remark In accordance with JLS 7 6 implementations may forbid a file T java from declaring a type v other than T when 1 the type vis referred to by code in other compilat
53. Root 1ib specs contains spec files corresponding to selected JDK library files Note The specifications in these spec files may not always match the actual semantics of the corresponding library files see section C 0 10 If you have a question comment or bug report concerning ESC Java or this manual you should start by checking the FAQ on the ESC Java web site If the FAQ does not address the issue adequately you can email the ESC Java group at lt escjava research compagq com gt You can also use this address to let us know if you have produced spec files for additional JDK library files and would like to share them Note Restrictions may apply in distributing annotated or modified versions of Sun s JDK files See the Sun Community Source License agreement at http www sun com software java2 license html Appendix C Sources of unsoundness and incompleteness ESC Java C 0 Known sources of unsoundness An unsoundness is a circumstance that causes ESC Java to miss an error that is actually present in the program it is analyzing Because ESC Java is an extended static checker rather than a program verifier some unsoundnesses are incorporated into the checker by design based on intentional trade offs of unsoundness with other properties of the checker such as frequency of false alarms incompleteness efficiency etc Continuing experience and new ideas may lead to reevaluation of these trade offs with some sources of unsoundn
54. SC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 3 2 11 exists 3 2 12 nonnullelements 3 2 13 fresh 3 2 14 result 3 2 15 yold 3 2 16 lbineg and lblpos 3 2 17 owner 3 3 Scoping name resolution and access control in specification expressions 4 Warnings 4 0 Parts of ESC Java warning messages 4 1 Arraystore warning 4 2 Assert warning 4 3 Cast warning 4 4 Deadlock warning 4 5 Exception warning 4 6 IndexNegative warning 4 7 IndexTooBig warning 4 8 Invariant warning 4 9 LoopInv warning 4 10 NegSize warning 4 11 NonNull warning 4 12 NonNulliInit warning 4 13 Null warning 4 14 ownerNull warning 4 15 Post warning 4 16 Pre warning 4 17 Race warning 4 18 Reachable warning 4 19 unreadable warning 4 20 Uninit warning 4 21 ZeroDiv warning 5 Command line options and environment variables 5 0 suggest 5 1 Specification spec files and the ESC Java s class path 5 1 0 File reading modes 5 1 1 The ESC Java class path classpath CLASSPATH bootclasspath 5 1 2 Specification spec files 5 1 3 How ESC Java decides which files to read and in which modes 5 1 4 depend 6 Java language support and limitations Appendix A Overview of how ESC Java works Appendix B Installing and using ESC Java at your site 6 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper resea
55. ain about the expression a m on original line 17 or the expression a mindex on the left hand side of the assignment on original line 21 However it does not avoid them in all cases A detailed 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes description of the circumstances in which ESC Java will or will not issue multiple warnings with the same underlying cause is beyond the scope of this manual 0 6 Scene 6 We supply a precondition for Bag extractMin We now consider the last of the five warnings Bag java 21 Warning Possible negative array index IndexNegative a mindex a n The problem is that the code in original lines 20 21 removes an element from the bag even when the bag is already empty that is when this n 0 onentry to extractMin ESC Java has called our attention to the need for another design decision do we add special code to handle the situation when ext ractMin is called on an empty bag or do we add a precondition forbidding such calls Let s try the latter course 12 requires n gt 1 13 int extractMin 0 7 Scene 7 We run ESC Java again and it still issues a warning With all the changes described above our example program now reads 1 class Bag 2 non_null int a 3 int n 4 5 requires input null 6 Bag int input 7 n input length 8 a new int n 9 S
56. anner that would be quite tedious awkward and error prone to accomplish with explicit assert and assume pragmas alone 2 2 2 A nowarn pragma suppresses warnings by turning assertions into assumptions Recall from the previous section 2 2 1 that ESC Java s built in checking for null dereferences works in effect by implicitly putting an assertion before each pointer dereference in the program so that the line 209 z x f gets treated as if it were 209 assert x null z x f except that the precise text of the warning message if any is different The way that a nowarn pragma suppresses warnings is by turning the implicit or explicit assertions that would generate the warnings into assumptions Thus for example the code fragment 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 209 z x f nowarn Null 210 w x g is treated by ESC Java like 209 assume x null z x f 210 assert x null w x g By changing the implicit assertion that x is non null on line 209 into an assumption the nowarn pragma not only prevents ESC Java from warning of a possible dereference of nu11 on line 209 but also satisfies the implicit assertion on line 210 thus preventing ESC Java from warning that the evaluation of the expression x g might dereference nu11 It should be clear from the above that the comments in section 2
57. are a partial order in which locks are to be acquired ESC Java will then check that each thread does in fact acquire locks in the given order But the checker trusts the programmer that the declared locking order is actually a partial order 2 7 0 monitored_by pragma 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes A5 of 86 A monitored_by pragma is a modifier pragma It can occur only as a modifier of a field declaration It has the form monitored_by L i opt where Lis a nonempty comma separated list of specification expressions The pragma declares that the modified field is a shared variable monitored by the locks in z That is it causes ESC Java to check that 1 the field is never read except by a thread holding at least one non null lock in z and 2 that the field is never written except when at least one lock in 1 is non null and the writing thread holds all non null locks in x See the first fine points below for an exception the preceding statement If the field declaration modified by the pragma declares an instance field then the expressions in L may mention this explicitly or implicitly When ESC Java checks an access to o f occurrences of this within Z are considered to denote the value of o Fine points When checking a constructor body ESC Java does not require that any lock be held in order to accesses a field of this even if the field i
58. at they may occasionally be useful can have a serious impact on performance Less obviously axioms mentioning Java variables are sometimes useful and ESC Java allows such axioms despite the unsoundness inherent in assuming them when checking method bodies without also checking them at call sites For further discussion of this point see the example in section 2 7 2 involving an axiom about the lock order Axioms may not mention this or lockset When checking a constructor body ESC Java assumes that axioms hold before the implicit superclass constructor call if any and thus also before execution of instance variable initializers When it is clear that the correctness of the program depends on a particular property holding for a particular expression of type T at a particular point in the program it may be better to write an assume pragma assume E at that point in the program in preference to introducing an axiom pragma axiom forall t Tj t 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 36 of 86 stating that the property holds for all values of the type even if it does For one thing the Simplify theorem prover used by ESC Java is incomplete and may not discover the relevant instance of the axiom to apply On the other hand regardless of whether Simplify discovers the relevant instance of the axiom it may spend a lot of time con
59. ation Executed else branch in C java line 14 col 11 Fine points The command line option plainwarning suppresses output of partial counterexample contexts in Invariant warnings The command line option counterexample causes ESC Java to supply counterexample contexts with all warnings The execution trace in a warning mentions the following events on the execution path associated with the warning execution of a return statement provided evaluation of the expression to be returned completes normally execution of a throw statement provided evaluation of the exception to be thrown completes normally execution of a break statement execution of a continue statement commencement of any branch of an if statement including the implicit empty else branch commencement of any branch of a switch statement including the implicit default commencement of evaluation of either arm of a conditional expression short circuit completion of evaluation of a conditional s and expression exceptional completion of a routine call commencement of any iteration of a loop see the fine points of section 2 4 3 for information about ESC Java s treatment of loops entrance to a finally block when the associated try block terminates with a throw return break OF continue exit from a finally block when the block is entered after a throw return break Of continue and the body of the finally block completes normally so that t
60. ava from issuing warnings about line 33 and or 34 because control can reach those lines before reaching line 35 e ESC Java might issue warnings about line 42 and or 43 because control might reach those lines by some path that does not first reach line 35 This can happen if control can reach line 32 with a or b being null and x being non null e ESC Java will not warn of a possible dereference of nu11 at line 44 or of a possible assertion failure at line 45 or 46 Every execution path that reaches line 44 first either reaches line 35 in which case ESC Java considers further execution of that path only for cases where 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 22 of 86 the expression in the assume pragma would evaluate to t rue or reaches lines 39 and 40 in which case the c and a are assigned non null values and e must already have been assigned a nonnegative value at line 31 For a concise formal description of the semantics of assume see LSS99 2 1 3 unreachable pragma An unreachable pragma is a statement pragma It has the form unreachable opt The pragma is semantically equivalent to assert false except for giving rise to a different warning message 2 2 Some remarks concerning assert and assume Readers anxious to cut to the chase may skip this section on first reading Others however may find that this material aids their intuition a
61. bout how ESC Java works The assert and assume pragmas introduced in section 2 1 are in some sense the most basic ESC Java pragmas We make some remarks about them here before going on to describe the rest 2 2 0 The assume pragma should be used with judgment An assume pragma resembles an assert pragma in that each states a condition that the programmer believes to hold whenever control reaches a certain point in the program The difference is that ESC Java checks that is issues a warning if it cannot establish the condition called an asserted condition or assertion in an assert pragma but ESC Java takes the assumed condition or assumption in an assume pragma for granted That is the programmer takes responsibility that assumed conditions will hold Put another way the assume pragma allows the programmer to trade spurious warnings incompleteness for possible missed warnings unsoundness Thus you should use assume pragmas with care lest by supplying an incorrect assumption you suppress warnings of genuine errors For example ESC Java will not warn of any error that might occur downstream in the execution path from the line x null assume x null since there can be no execution path where the assumption holds after the assignment is performed On the other hand there will be cases where assume pragmas or nowarn pragmas which call for similar caution in their use will be the only practical means to eliminate spurious
62. called specification expressions are given in section 3 For now we remark that since specification expressions are not actually executed the unconditional logical operators and are interchangeable except for binding power in specification expressions with the respective conditional operators amp and 0 9 Scene 9 ESC Java notices a typographical error When we run ESC Java again the result is Bag java 4 Error No such field in type int invariant 0 lt n amp n lt a lenght a Caution Turning off extended static checking due to type error s 1 caution 1 error 0 10 Scene 10 Our efforts come to a happy conclusion Whoops Our invariant pragma had a spelling error We correct it to read 4 invariant 0 lt n amp n lt a length and try again This time ESC Java runs without reporting any further complaints The file escjavaRoot examples 0 10 Bag java contains a copy of the final version of the Bag class 1 An overview of ESC Java and of this manual In this section we summarize the principal features of ESC Java While some of the things we say here reiterate points made in our example of section 0 we also describe a number of features of ESC Java that are not discussed at all in section 0 Moreover we address a number of points that were glossed over in section 0 and that possibly raised questions in the mind of the perceptive reader Throughout this section we refer the reader to later
63. ced for the Bag constructor in section 0 2 requires input null Bag int input might equally well have been written after the signature of the constructor Bag int input requires input null with identical semantics except of course that warning messages referring to the pragma would indicate a different source file location Regardless of where a routine modifier pragma appears the parameters of the routine are in scope in any specification expression in the pragma e Inan ensures section 2 3 2 pragma modifying a constructor and in any pragma modifying an instance method specification expressions may mention this denoting the constructed object or the object whose method is being invoked As usual in contexts where this may occur it may occur implicitly a field access this being written simply as unless the name is hidden for example by a parameter name e The pragmas in this section specify preconditions modification targets and normal and exceptional 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 26 of 86 postconditions of routines When a method of a class or interface s inherits or overrides JLS 8 4 6 a method m from a class or interface T the method s m inherits all the preconditions modification targets and postconditions of T m with the formal parameter names of s m being substituted for those o
64. copy of For information about resolution of name conflicts involving ghost variables see section 3 3 In some cases it is useful to declare a ghost variable with a modifier pragma such as non_nu11 In this 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 41 of 86 case the modifier pragma must occur within a nested pragma containing comment for example ghost public non_null T t More precisely within a ghost pragma M T VD i opt an inner pragma containing comment containing modifier pragmas is allowed either as part of m or just after vb The only modifier pragmas that can usefully modify a ghost variable are non_null monitored and monitored_by the current ESC Java may accept others but if it does they will have no effect on the checking performed In addition these pragmas are allowed only in the case where they would be allowed for a normal variable according to the table in section 2 0 1 For example a static ghost variable cannot be declared with the pragma monitored or with the pragma monitored_by E where the expression mentions this ESC Java checks monitored section 2 7 1 and monitored_by section 2 7 0 pragmas for a ghost variable g only where gis assigned to by a set pragma section 2 6 1 not at other places where g is used in pragmas 2 6 1 set pragma A set pragma is a statement pragma It has the form set D E iopt
65. ctically large verification conditions or impractically slow checking Fine point In the unrollings described above execution of a break causes normal completion of the entire loop and execution of continue causes normal completion of the current unrolled copy of s C 0 2 Object invariants When checking the implementation of a method ESC Java assumes initially that all allocated objects satisfy their invariants But when checking a call to a method ESC Java imposes a weaker condition on the caller all actual parameters of the call and all static fields that are in scope are shown to satisfy their invariants but not every object in existence Since more is assumed than is proved this is unsound It seems difficult to design a sound discipline that is not impractically strict the current rule is a compromise that seems useful See LS97 for a more detailed discussion of the interaction of object invariants with scoping Another source of unsoundness in the checking of object invariants arises because as we mentioned in section 2 4 1 when ESC Java checks the body of any routine R it does not consider all invariants but only a heuristically chosen relevant subset If an invariant is deemed irrelevant during the checking of a routine that calls R but deemed relevant during the checking of R then the invariant will not be checked even for parameters at the call site but will nonetheless be assumed to hold initially during the verifica
66. d is said to be a target field of the routine Note that a modification target of the form g makes but not g be a target field 2 3 2 ensures pragma An ensures pragma is a routine modifier pragma It has the form ensures E opt where is a boolean specification expression The pragma makes a normal that is non exceptional postcondition of the routine the pragma modifies When checking the body of the routine ESC Java issues a warning if it cannot establish that holds whenever the routine terminates normally When 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 28 of 86 checking code that calls the routine ESC Java assumes that holds just after the call if the call terminates normally In a postcondition of a non void method the special ESC Java identifier resui1t denotes the result of the method For constructors the constructed object may be denoted only by this not by result The static type of result is the result type of the method Within an expression of the form fresh R where R is a specification expression of a reference type is true if the object denoted by R in the post state is allocated in the post state implying that R null in the post state and was not allocated in the pre state The static type of fresh R is boolean A postcondition may contain expressions of the form ola x Roughly speaking
67. d in sections 2 and 3 of this manual and all the warning types described in section 4 giving very brief descriptions of each While it necessarily omits numerous examples tips motivating discussions and technical details found in the present manual it will still be of interest both the new reader seeking a whirlwind tour of ESC Java s features and to the experienced user seeking a quick reminder about some ESC Java feature Although ESC Java contains a full Java program verifier the goal of ESC Java is not to provide formally rigorous program verification Rather it is to help programmers find some kinds of errors more quickly than they might be found by other methods such as testing or code reviews Consequently ESC Java embodies engineering trade offs among a number of factors including the frequency of missed errors the frequency of false alarms the amount of time used by the tool the effort required to learn and use the annotation language and the effort required to implement the tool In this manual we attempt to give a precise description of the syntax type checking and other linguistic rules of the annotation language as well as a clear though informal description of the meanings of the various pragmas While we discuss potential sources of missed errors or false alarms at various places in the manual including a summary in appendix C we do not attempt to characterize precisely the degree of in accuracy of ESC Java s checking In ma
68. de When ESC Java reads a file in spec only mode it only obtains specifications that can be used to check routine bodies in other files ESC Java can read java files in either mode It can read class files in spec only mode but not in full mode When ESC Java reads a source file in spec only mode it performs very limited processing in particular very liberal syntactic error checking on the bodies of routines We do not specify here the exact degree to which the error checking is liberalized except to state that where a routine body would normally be expected ESC Java will accept at least any of the following when reading a source file in spec only mode asemicolon as in the Java syntax for an abstract method declaration an empty body note that no return statement is required even for a non void method a method body consisting of legal Java code legally annotated by ESC Java pragmas that is a body that ESC Java would accept if it were reading the file in full mode 5 1 1 The ESC Java class path classpath CLASSPATH bootclasspath Like the Java compiler javac 5 ESC Java uses a class path to look for declarations of types classes and interfaces that are not declared in files named on the command line For a description of how ESC Java uses the class path see section 5 1 3 below The full class path is the concatenation of two parts classpath and bootclasspath where classpath is e the argument of the
69. ding reducing ESC Java s memory footprint Tice and getting the build recipe for the Simplify theorem prover to work on multiple platforms Joshi The ESC Java project is a follow on to an earlier extended static checking project at SRC targeting the Modula 3 language DLNS98 and continues to use the Simplify theorem prover developed as part of that project The authors thank our colleagues who have offered comments on earlier versions of this manual Allan Heydon David Jefferson Mark Lillibridge Silvija Seres and Caroline Tice have been particularly helpful in this regard Silvija Seres compiled the initial version of the ESC Java Quick Reference SLS00 from an earlier version of this manual We and the other implementers of ESC Java have benefited from the feedback of early users including Sanjay Ghemawat Steve Glassman Allan Heydon David Jefferson Marc Najork Keith Randall and Silvija Seres Gary Leavens played a major role in our attempt to remove gratuitous incompatibilities between ESC Java and JML and helped us to improve the ESC Java annotation language in the process Contents Preface Acknowledgments Contents Q An illustrative example of using ESC Java 0 0 Scene 0 We write a class declaration 0 1 Scene 1 We run ESC Java and it warns of two potential nu11 dereferences 0 2 Scene 2 We write a requires precondition pragma for the Bag constructor 0 3 Scene 3 We add a non_null pragma for the field a
70. dition for the constructor that is a boolean expression which must be t rue at the start of any call When checking the body of a method or constructor that is annotated with a precondition ESC Java can assume the truth of the precondition to confirm the absence of errors in the body for example the absence of a null dereference during the evaluation of input length in the code fragment above When checking code that calls a method or constructor annotated with a precondition ESC Java will issue a warning if it 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 10 of 86 cannot confirm that the precondition with the values of the actual parameters substituted for the formal parameter names would always evaluate to t rue at the call site 0 3 Scene 3 We add a non_nu11 pragma for the field a So much for the first warning We now turn our attention to the second warning Bag java 15 Warning Possible null dereference Null if a i lt m A Here ESC Java is warning that the array variable a actually this a might be nu11 We could deal with this warning by either of the approaches discussed above in connection with the first warning that is by adding the precondition requires a null to the extractMin method or by adding special code for the case a null However ESC Java offers yet another choice which is to specify that the a field of any Bag is al
71. ds and issues warnings if they might acquire locks out of order A synchronized statement synchronized E is treated roughly like Object e E where e is a variable name not already used assert e null but with Null warning on failure assert lockset e max lockset lt e but with Deadlock warning Insert e into lockset try ch finally Restore former value of lockset The disjunct lockset e in the test for potential deadlocks reflects the fact that Java locks are reentrant that is that a thread that already holds a lock may acquire the lock again without deadlocking JLS 17 5 When checking a synchronized method declaration ESC Java acts as if the body of the method were wrapped in synchronized statement as described in JLS 8 4 3 5 That is ESC Java checks an instance method synchronized T m parameters body as if it had been written T m parameters synchronized this body and ESC Java checks a static method static synchronized T m parameters body in a class c as if it had been written static T m parameters synchronized C class body When a routine that already holds a lock acquires another one ESC Java needs some way of knowing that the first lock precedes the second in the lock order One way to give ESC the needed information is by 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes
72. ds that are declared later in textual order even though they are in scope this restriction does not apply to ESC Java pragmas compare the examples in sections 2 5 1 and 2 7 0 to those in JLS 8 3 2 1 8 3 2 2 When a SpecExpr occurs in a modifier pragma applied to a routine declaration names in the SpecExpr are resolved as if the SpecExpr were placed at the beginning of the routine body Consequently the names of the routine s parameters are in scope Furthermore if the routine is an instance method then this and super can be mentioned and if the routine is a constructor then this and super can be mentioned in ensures pragmas As usual wherever this can be mentioned an unqualified field name f is a synonym for this f e When a SpecExpr occurs in a modifier pragma applied to an abstract method declaration names in the SpecExpr are resolved as if the method could have a body and the SpecExpr were placed there That is the names of the method s parameters are in scope this can be mentioned any unqualified field name f is a synonym for this f and if the abstract method declaration occurs in a class 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 61 of 86 rather than in an interface then super can be mentioned e In any other SpecExpr the same parameters local variables and fields are in scope as in the Java context where the annotation containing t
73. e class to be checked and the classes and interfaces it uses Next ESC Java translates each routine to be checked into a logical formula called a verification condition VC As an intermediate step in this translation ESC Java produces a command in an intermediate 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes language LSS99 based on Dijkstra s guarded commands The intermediate language includes commands of the form assert where is a boolean expression of the language An execution of a command is said to go wrong if control reaches subcommand of the form assert when zis false Ideally when a routine R is translated into a command c and thence to a verification condition v the following three conditions should be equivalent 1 There is no way that R can be invoked from a state satisfying its specified preconditions and then behave erroneously by for example dereferencing nu11 violating an assert pragma terminating in a state that violates its specified postconditions etc 2 There is no execution of c that starts in a state satisfying the background predicate of R s class and then goes wrong 3 vis a logical consequence of the background predicate In practice the translation is incomplete and unsound so there may be semantic discrepancies between R c and v Finally ESC Java invokes the Simplify Simplify 1 theorem prover asking
74. e current ESC Java includes the following modifier pragmas for variable declarations 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes non_null pragma 2 4 0 O spec_public pragma 2 5 0 readable_if pragma 2 5 1 uninitialized pragma 2 5 2 O monitored_by pragma 2 7 0 7 0 monitored pragma 2 7 1 Tie current ESC Java includes the following modifier pragmas for routine declarations O requires pragma 2 3 0 3 0 O modifies pragma 2 3 1 O ensures pragma 2 3 2 O exsures pragma 2 3 4 also_ensures pragma 2 3 5 2 also_exsures pragma 2 3 6 3 6 O also_modifies pragma 2 3 8 3 8 In the current ESC Java there are no pragmas that can modify both variable and routine declarations Fine points A modifier pragma that modifies a routine method or constructor declaration may appear either in any of the following places e near the beginning of the declaration in the usual place where Java modifiers such as private or final may occur e just before the opening left brace of the routine s body or e just before the final semicolon of a routine declaration if there is no body as in an interface in an abstract Class or sometimes in a spec file see section 5 1 2 The semantics of a routine modifier pragma is independent of whether the pragma appears lexically before or after the signature of the routine Routine modif
75. e to j ina pragma in D would be ambiguous since c and 1 both declare ghost fields named j and neither hides the other Note The preceding rules about ghost variables and the restriction against reusing a name in scope as a ghost field name section 2 6 0 are intended to reduce the number of situations where a name unambiguously means one thing in Java code and unambiguously means a different thing in an adjacent pragma Unfortunately some such situations still remain For example if a ghost field and a class have the same name v then the expression n f might refer to a static field of class N in Java code while meaning this N f in a nearby annotation The rules that make names accessible in specification expressions spec accessible are in some cases more liberal that Java s access control rules JLS 6 6 In particular e If a variable s declaration is annotated with a spec_public section 2 5 0 pragma then the variable is spec accessible wherever it would have been spec accessible if it had been declared public e A variable declared as protected is spec accessible in the package where it is declared and in any subclass of the class where it is declared without the additional restriction in JLS 6 6 2 Of course there are also some cases where variables for example ghost variables section 2 6 0 are spec accessible but not Java accessible simply because they are not in scope in Java Finally the label dentifier in a 1blp
76. eb at http gatekeeper dec com pub DEC SRC technical notes abstracts src tn 2000 003 html Cited in sections 5 0 and C 1 2 CS Inner Classes Specification Sun Microsystems on the web at http java sun com products jdk 1 1 docs guide innerclasses spec innerclasses doc html Cited in section 6 JLS James Gosling Bill Joy and Guy Steele The Java Language Specification Addison Wesley Reading Massachusetts 1996 Also available on the web at http java sun com docs books jls html index html Cited in places too numerous to mention LBR99 Gary T Leavens Albert L Baker and Clyde Ruby JML A notation for detailed design in Haim Kilov Bernhard Rumpe and Ian Simmonds editors Behavioral Specifications of Businesses and Systems pages 175 188 Kluwer Academic Publishers Boston 1999 Cited in the preface LBROO Gary T Leavens Albert L Baker and Clyde Ruby Preliminary design of JML A behavioral interface specification language for Java Technical Report 98 06 Iowa State University Department of Computer Science May 2000 Available on the web at www cs iastate edu leavens JML html Cited in the preface Leino98 Rustan M Leino Data groups Specifying the modification of extended state in Proceedings of the 1998 ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications OOPSLA 98 volume 33 10 of ACM SIGPLAN Notices pages 144 153 October 19
77. ecise name for this pragma might be meaningful_only_if 39 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 40 of 86 Remark Perhaps unfortunately ESC Java does not provide a way to say when particular array elements are readable meaningful This could be useful since one could then express for example a i is meaningful only if 0 lt i amp i lt n which says that only the first n elements of array a are in use 2 5 2 uninitialized pragma An uninitialized pragma is a modifier pragma An uninitialized pragma can occur as a modifier only of a local variable declaration that has an initializer The pragma causes ESC Java to check that no execution path reads the variable without first performing an assignment other than the initializer to the variable The intended use of the uninitialized pragma is for situations in which the conservative nature of Java s definite assignment rules JLS 16 has forced the programmer to supply an irrelevant initial value 2 6 Pragmas concerning ghost variables Unlike ESC Modula 3 see SRC Report 159 Extended static checking ESC Java does not support data abstraction But ESC Java does provide a poor man s version of abstract variables called ghost variables We describe here the ghost pragma which declares ghost variables and the set pragma which modifies them and then give an example of their use
78. erator gt see section 3 2 9 o the Java conditional operators s and JLS 15 22 15 23 o the Java logical operators and JLS 15 21 2 o the Java boolean equality operators and JLS 15 20 2 o the Java logical complement operator JLS 15 14 6 e as the entire body of a parenthesized expression o a quantified expression forall E Or exists E see section 3 2 11 or o a labeled expression lblpos n E Or lblneg n E see section 3 2 16 e as a top level boolean specification expression that is not properly contained by another specification expression in a pragma The same restriction applies to specification expressions containing applications of exists section 3 2 11 or of lblneg or lblpos section 3 2 16 In particular a quantified or labeled expression may not occur in an argument to the ternary conditional operator and this restriction cannot be evaded by 52 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 53 of 86 use of the boolean cast operator For example specification expressions of the form boolean exists are not allowed A consequence of these restrictions is that all legal specification expressions containing quantified or labeled subexpressions are of type boolean Note that the preceding rule forbids quantified expressions and labeled expressions within argumen
79. ess possibly being eliminated and others possibly being added in future versions of ESC Java In this section we have attempted to describe or at least allude to all known causes of unsoundness in the current ESC Java If you become aware of any that we have missed please bring them to our attention see appendix B C 0 0 Trusting pragmas The assume axiom and nowarn pragmas allow the user to introduce assumptions into the checking process ESC Java trusts them If the assumptions are invalid the checking can miss errors Besides the possibility of an assume axiom Or nowarn pragma being outright wrong there are the following subtleties e As mentioned in the description of the axiom pragma section 2 4 2 and illustrated in an example in section 2 7 2 axioms can mention mutable state ESC Java assumes that all heuristically relevant axioms hold at the start of any routine body being checked but does not check that they still hold before each routine call or at the end of the routine body being checked 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 78 of 86 e Certain ESC Java warnings for example Null warnings correspond to conditions that would result in Java exceptions for example NullPointerException Ifa program is written intentionally to raise and then handle such an exception the user might put a nowarn pragma on the line where the except
80. et of terms already under consideration In some cases the triggering may be overly restrictive preventing Simplify from finding instances that are actually needed for the proof After Simplify instantiates the body of a universally quantified formula the terms in the instantiated body may match the triggering patterns of other universally quantified formulas triggering instantiations of their bodies and so on To avoid infinite looping Simplify bounds the depth to which such sequences of matching may cascade In some cases Simplify may report a potential counterexample that could in fact have been refuted by deeper matching C 1 1 Incomplete modeling of Java semantics Ideally the verification condition for a routine R would be a formula that was valid if and only if R were free of the kinds of potential errors ESC Java aims to detect In fact the verification conditions that ESC Java generates fall short of modeling the full semantics of Java in many ways For example ESC Java s built in semantics for floating point operations are extremely weak not strong enough to prove 1 0 1 0 2 0 oreven1 0 2 0 ESC Java s built in semantics for strings are quite weak strong enough to prove Hello world null but not strong enough to prove the assertion s 1 after the assignment c Hello world charAt 3 ESC Java treats exceptions thrown by the run time system as errors even in programs that include code to catch them The ESC
81. expresses the programmer s intention that the variable modified by the pragma has a meaningful value only when z is true The specification expression is allowed to mention this if the pragma modifies an instance field declaration or if the pragma modifies a local variable declaration within an instance method or a constructor If the pragma modifies the declaration of an instance field f then for purposes of checking a read access o f occurrences of this in are taken to denote the value of o Fine points If the pragma modifies a local variable declaration then the variables declared by the declaration are not in scope in even if the pragma occurs just before the final semi colon instead of before the type class C boolean b void m boolean b readable_if b b in the pragma above means this b not the local b b in the pragma below means the local b veadable_if b int c If the pragma modifies a field declaration then all fields of the containing class are in scope in even those that are declared in textually later declarations class C extends B readable_if b int a boolean b b in the pragma means this b not B this b If the pragma modifies a field declaration then the free variables of must be spec accessible wherever fields declared by the declaration are accessible according to Java s access control rules JLS 6 6 Remark For the picky a more pr
82. f T m ESC Java desugars implicit references to this as described in the previous bullet before doing the formal parameter substitution so nothing funny happens if only one of the two formal parameter lists includes a name conflicting with a field of this This treatment of inheritance sometimes leads to unsound checking in the presence of multiple inheritance see section C 0 5 When checking code that contains a call to a routine ESC Java interprets the routine s preconditions modification targets and postconditions with the actual parameters values substituted for the formal parameter names and in the case of an instance method call m with the value of substituted for this including of course implicit occurrences of this In cases where evaluation of the actual parameters may have side effects or may raise exceptions ESC Java does the right thing It checks the preconditions of the routine for the program state after the side effects and only for cases in which evaluation of all parameters would terminate normally e When checking code that contains a method call m ESC Java determines the specification preconditions modification targets and postconditions of m based on the static type T of even if E can be proven always to be of some subtype s of r To get ESC Java to use additional specifications of s m beyond those inherited from T m you could rewrite the Java code to cast to type s before invoking m
83. f exceptions being thrown other than by throw statements or in accordance with the throws clauses of called routines Tips The control point associated with an Except ion warning is the end of the routine body rather than the point at which the exception is first thrown This is technically correct because the potential error is not throwing the exception but letting the exception escape the routine body without being caught However in trying to understand why the warning is being issued and what to do about it you are more likely to be interested in knowing where the problematic exception might be thrown as indicated by the execution trace see section 4 0 in the warning message The Java language requires that routines declare all checked exceptions that they might throw JLS 11 2 Consequently ESC Java s Exception warning is of interest only in connection with unchecked exceptions Even if your own code makes no mention of unchecked exceptions it may call library routines whose throws clauses mention unchecked exceptions It may tempting to take the view that unchecked exceptions are unchecked precisely because it is not worthwhile to check for their presence at compile time and therefore always to run ESC Java with the nowarn Exception command line option see the escjava 1 man page for descriptions of ESC Java command line options However the whole purpose of ESC Java is to do more sophisticated static checking than compilers
84. gma An also_modifies pragma is a routine modifier pragma It has the form also_modifies L i opt where 1 is a nonempty comma separated list of specification designators see section 2 3 1 An 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 32 of 86 also_modifies pragma has the same semantics as a modifies pragma section 2 3 1 but may appear only as a modifier of a method declaration that overrides another method declaration while overriding method declarations are forbidden to have modifies pragmas An overriding method declaration may modify both the targets named in its own also_modifies pragmas and any modification targets it inherits from the overridden method Fine points Like the also_require pragma section 2 3 7 the also_modifies pragma is a potential source of unsoundness When writing code that follows a call m where has static type T a programmer may reasonably be expected to cope with the possibility that the call has modified parts of the state named in modifies pragmas that annotate the declaration of T m but it seems unreasonable to expect the programmer to deal with the possibility that the call might modify other parts of the state perhaps parts mentioned in also_modifies pragmas of yet to be written overrides as well The reason that ESC Java includes an also_modifies pragma is that an overriding method may need to modify fie
85. hat the object for which the invariant is broken is not the object this whose Push method is called The problem is that so far as ESC Java can tell there may be some object call it brokenobj such that the following conditions hold at the start of the execution of Push brokenObj this brokenObj a this a brokenObj n this n Now consider the effect of the line 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 59 of 86 15 a nt 0 The evaluation of n increases this n but leaves brokenoObj n unchanged On the other hand the array store does set brokenObj a n where n denotes the value before the increment to o Thus after line 16 we have brokenObj a brokenObj n 0 so that ifo null as may very well be the case the instance invariant on line 6 is violated for brokenObj In fact as illustrated by the example above the correctness of the Push method of objStack depends on an implicit design decision No two distinct objStack s ever share the same a field The correctness of Pop also depends on this design decision though not in a way that is checked by ESC Java given the annotations in the example above The user can take advantage of the owner field to communicate this design decision to ESC Java by adding the pragma 7 invariant a owner this Given this invariant it is no longer possible to have a scenari
86. hat the variable is non null then it will issue a warning for the first dereference of the variable in each arm of the switch statement In order to reduce the likelihood of flooding the user with redundant warnings ESC Java will issue at most 10 warnings for any method or routine before moving on to the next routine Users can change the maximum number of warnings per routine by setting the PROVER_CC_LIMIT environment variable see the escjava 1 man page Section 4 0 describes the parts of ESC Java warning messages The remaining subsections of this section describe all the types of warnings issued by the current ESC Java These descriptions may be skipped on first reading or until the reader is confronted with an ESC Java warning whose meaning or cause is unclear A recommended discipline for using ESC Java is to annotate your program sufficiently so that ESC Java produces no warnings and in this process to resort to the use of nowarn or assume pragmas only in cases where other alternatives are impractical Below we include occasional tips about pragmas that might be added in response to particular warnings The suggest command line option see section 5 1 1 or the escjava 1 man page causes ESC Java to offer suggestions of varying quality for pragmas that might be added in response to some warnings 4 0 Parts of ESC Java warning messages The primary part of each ESC Java warning message gives a brief description of the kind of conditi
87. he SpecExpr occurs this can be mentioned and any unqualified field name f is a synonym for this if the SpecExpr occurs in a Java context where this can be mentioned and super can be mentioned if the SpecExpr occurs in a Java context where super can be mentioned Moreover in a SpecExpr that occurs in a declaration pragma see section 2 0 1 in a class this and super can be mentioned and any unqualified field name is a synonym for this f A ghost field f see section 2 6 0 is in scope in pragmas wherever an actual Java member of the class containing the ghost pragma declaring would be in scope The rules for name resolution are different for ghost variables than for ordinary variables Java variables if in scope hide conflicting ghost variables of the same name regardless of their points of declaration and regardless of whether the Java variable is accessible Ghost variables on the other hand hide neither Java variables nor other ghost variables For example given the declarations Input form file I java interface I ghost public int i ghost public int j Input from file C java class C private int i ghost public int j Input from file D java class D extends C implements I a reference to i in a pragma in D java would resolve to the real field of c rather than the ghost field of 1 and would then generate an error because that field is not accessible in D while a referenc
88. he throw return break or continue is resumed after the finally block ESC Java actually associates some execution path with each warning but if the execution path associated with a warning includes no events of the kinds listed above then ESC Java omits the line Execution trace information from the warning message The command line option not race suppresses output of execution traces The command line option suggest causes ESC Java to accompany certain of its warning messages with suggestions for pragmas that may eliminate those warnings See section 5 0 for some examples 4 1 arrayStore warning An ArrayStore warning warns that the control may reach an assignment aI when the value of is 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 65 of 86 not assignment compatible with the actual element type of a This condition would result in an ArrayStoreExcept ion being thrown at run time JLS 10 10 15 25 1 Tip See section 3 2 4 for discussion of a common cause of spurious ArrayStore warnings and examples of annotations to avoid them 4 2 Assert warning An Assert warning warns that control may reach a pragma assert when the value of Fis false 4 3 cast warning A Cast warning warns that control may reach a cast T E when the value of cannot be cast to the type E This condition would result in a ClassCastExcept ion being thrown at r
89. hod or of T n if the routine is a static method of class T e a field access of the form o where ois a specification expression of a reference type T and f denotes one of the fields possibly a ghost field of T This form allows modification of o f If is a static field o is used only in that its static type disambiguates f e an array access of the form A r where a is a specification expression of an array type and r is a specification expression of an integral type other than long This form allows modification of A 11 an array range of the form a where a is a specification expression of an array type This form allows modification of all elements of a but not of a itself A routine may be annotated with multiple modifies pragmas in which case a call is assumed possibly to modify any state component listed in any of the modifies pragmas If no modification targets are specified for a routine then ESC Java will assume that calls to the routine modify only freshly allocated state if any A method declaration that overrides another method declaration cannot be annotated with a modifies pragma but inherits the modification targets of the overridden method Note that this forbids the overriding method from modifying additional state but see the description of also_modifies below section 2 3 8 2 3 1 0 target fields When a modification target of a routine has the form or simply f meaning this the fiel
90. ht v line a Undo the rotation Tree v this right synchronized v line b 48 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 49 of 86 Tree x v right if x null line c synchronized x line d v right x left x left v this right x line e The problem is that the axiom is assumed to apply at the start of the routine and thus to apply to the values of 1eft and right at the start of the routine According to the lock order thus defined the lock acquired at the line a would precede that acquired at b Despite these caveats our experience with ESC for Modula 3 suggests that axioms like the ones above will do the right thing surprisingly often and rarely cause problems The preceding example also illustrates a possible source of unsoundness in ESC Java s treatment of race detection If the lines marked c and e are deleted and if deadlock checking is left disabled then ESC Java will accept line a without complaint ignoring the possibility that some other thread might have taken advantage of the window between lines a and b to synchronize on v and set its right field to null 3 Specification expressions While specification expressions are generally similar to Java expressions there are a number of differences described below Section 3 0 describes a slight exte
91. ier pragmas are described further in section 2 3 A modifier pragma that modifies a variable declaration may appear either in the usual place for modifiers near the beginning of the declaration or just before the final semicolon The pragma applies to all variables declared in the declaration and its semantics is independent of its position within the declaration For convenient reference here is a table listing ESC Java pragmas that can modify variable declarations the sections of this manual where they are described and the kinds of declarations they are allowed to modify instance static local formal variable field variable parameter non_null 2 4 0 yes yes yes yes spec_public 2 5 0 yes yes no no readable_if 2 5 1 yes yes yes no uninitialized 2 5 2 no no yes no monitored_by 2 7 0 yes yes no no monitored 2 7 1 yes no no no Note that ESC Java sometimes allows modifier pragmas in declarations of local variables including those declared in the ForInit of a for statement JLS 14 12 and formal parameters Particular pragmas may have further restrictions on where they may occur beyond those given above These restrictions are described in the sections describing the respective pragmas 17 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 18 of 86 2 0 2 ESC Java sometimes allows pragmas to contain nested pragmas or comments Situations sometimes a
92. if need be at some risk of lost soundness as in the case of the nowarn assume and axiom pragmas respectively described in sections 2 1 0 2 1 2 and 2 4 2 below o ESC Java issues caution messages in some but not all cases where unsound checking may occur 2 ESC Java pragmas In this section we describe all the kinds of ESC Java pragmas the places where they can occur and informally what they mean We begin by giving some general information about where pragmas can occur and then go on to describe the individual pragmas Many pragmas can contain expressions called specification expressions which are similar to Java expressions but with a few constructs legal in Java expressions being forbidden and a number of added constructs being permitted We mention some of the added constructs in connection with pragmas where they are of use but defer a detailed description of specification expressions to section 3 Most pragmas are ways of asking ESC Java to produce warnings if certain user expectations about the behavior of the annotated program may be wrong We will often say that ESC Java checks that some condition x holds at a particular control point when it would be more precise to say that ESC Java issues a 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 16 of 86 warning message if it cannot prove that x holds at that point Keep in mind that in addition to
93. ill silently be converted to incorrect results This is a potential source both of unsoundness and of incompleteness see also section C 1 0 C 0 7 Ignored exceptional conditions ESC Java checks for specific conditions that could give rise to a Nul1PointerException IndexOutOfBoundsException ClassCastException ArrayStoreException ArithmeticException or Negat iveArraySizeException and warns of those conditions as potential errors It ignores the all other cases where instances of unchecked exception classes for example OutOfMemoryError StackOverflowError ThreadDeath SecurityException JLS 11 2 20 22 might be thrown either synchronously or asynchronously except by explicit throw statements in a routine body being checked or in accordance with the throws clauses of routines called by a routine being checked C 0 8 Constructor leaking There are a number of ways in which a constructor can make the new object under construction available 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes in contexts where its instance invariants are assumed to hold but without actually having established those instance invariants For example e A constructor may terminate abruptly by throwing this without establishing object invariants for this e A supertype constructor may store this into a field of a global variable and then return to the subty
94. ine ESC Java will also check the classes that those classes depend on including indirectly provided that finds their declarations in java files Caveat As currently implemented the depend option is likely to give unsatisfactory results in cases where both a spec file and a java file declaring the same class can be found on the class path When run with depend ESC Java will prefer to read the class declaration from the java file so that it can read in full mode and check the class s routine bodies On the other hand successful checking of clients of the class will likely require use of pragmas found only in the ignored spec file and not in the java file 6 Java language support and limitations The Java Language Specification JLS defines the Java 1 0 language The Inner Classes Specification ZCS specifies the additional language features supported in Java 1 1 and Java 1 2 The current version of ESC Java accepts all Java language features described in JLS it also accepts all Java language features described in JCS with the following two exceptions e When ESC Java reads a class c from file c class and one of c s members is a class c D ESC Java will look for the file c D class only in the directory where it found c class e ESC Java will not check any routine body that mentions an anonymous class Java 1 2 includes the same language features as Java 1 1 but differs from 1 0 and 1 1 in the versions of the standard
95. input 0 a 0 n 4 set empty n 0 5 6 7 ensures result empty 8 public boolean isEmpty 9 return n 0 20 21 22 requires empty 23 modifies empty 24 modifies n al 25 public int extractMin 26 int m Integer MAX_VALUE 27 int mindex 0 28 for int i 0 i lt n itt 29 if a i lt m 30 mindex i 31 m a i 32 33 34 n 35 set empty n 0 36 assert empty n 0 37 a mindex a n 38 return m 39 40 The precondition for ext ractMin on line 22 specifies that it is incorrect to invoke the ext ractMin method of an empty Bag The postcondition for isEmpty on line 17 allows clients and ESC Java to determine that a code fragment like if x isEmpty i x extractMin 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes will never violate the precondition for ext ractMin The invariant on line 6 relates the ghost field empty to the actual field n in the implementation of a Bag and is of interest only to the implementer of the Bag class and not to clients ESC Java uses this invariant to verify that the implementation of isEmpty satisfies its postcondition and to verify that the implementation of ext ractMin when called in accordance with its precondition will not attempt to access a 1 in line 37 The set prag
96. iolation on any call q enqueue where may not be an instance of T On the other hand it will not issue a spurious warning of possible cast failure on T q dequeue Also ESC Java will warn of a possible precondition failure on q dequeue if it cannot establish based on the number of elements enqueued and dequeued done since the allocation of q or the most recent call to q isEmpty that q is nonempty q size gt 1 at the point of the call For more examples of the use ghost variables in specifying container classes read the files Dictionary spec Enumerator spec and Vector spec in escjavaRoot 1lib specs java util see appendix B 2 7 Pragmas for specifying synchronization ESC Java provides support for checking that multi threaded programs respect a locking discipline that prevents race conditions and simple deadlocks A race condition is a situation in which two threads access a variable simultaneously and the accesses are not both read accesses To prevent race conditions the locking discipline requires that every shared variable is monitored by one or more locks If a variable is monitored by a lock a thread is not allowed to access the variable unless it holds the lock and this discipline is enforced by ESC Java A deadlock occurs if there is a cycle of threads each holding a lock that some other thread in the cycle is waiting to acquire To prevent deadlocks the locking discipline requires that the programmer decl
97. ion units of the package in which the type v is declared or 2 the type vis declared public ESC Java does not enforce this restriction Note however that when the restriction is obeyed alternative 4 above will never arise During the process just described various errors may occur For example a file may not contain a declaration of the class suggested by the file name We do not attempt here a complete enumeration of these conditions Also it is beyond the scope of this manual to describe exactly which type declarations ESC Java looks for in order to check a given type 5 1 4 depend Note If you are not an ESC Java wizard and don t aspire to be you should probably skip this section and never use depend The depend command line option causes ESC Java to change its behavior from that described above in the following ways e ESC Java will prefer to read java files rather than spec files That is the ranking given in section 5 1 3 switches from 0 1 2 4 3 to 0 2 4 1 3 e When reading a java file alternative 2 or 4 then ESC Java will read the file in full mode rather 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 75 of 86 than spec only mode This is in contrast to the normal behavior where only java files named on the command line are read in full mode e Instead of checking only classes declared in files named on the command l
98. ion would be raised In such a case the current ESC Java will not check that there actually is a handler nor will it check for any errors that might occur in the handler or dynamically after execution of the handler C 0 1 Loops The current ESC Java does not consider all possible execution paths through a loop It considers only those that execute at most one complete iteration plus the test for being finished before the second iteration as explained in section 2 4 3 This is simple and avoids the need for loop invariants but it is unsound The user can modify ESC Java s treatment of loops by using the 100p command line option The loop option takes an argument of the form n n 0 or n 5 where n is a non negative integer literal The argument specifies the number of loop iterations ESC Java should consider Suppose for example that the program being checked includes the fragment loop_invariant E while B S If you run ESC Java with the 1oop n or equivalently Loop n 0 on the command line it will consider execution paths that include up to n executions of assert E but giving a LoopInv warning if B break S plus one additional execution of assert E If you run ESC Java with loop n 5 on the command line it will consider execution paths that include up to n executions of assert E but giving a LoopInv warning if B break S plus one additional execution of assert E bu
99. k our definition of class Bag with ESC Java we instead type the following similar command line escjava Bag java ESC Java then produces the following output Bag java 6 Warning Possible null dereference Null n input length Bag java 15 Warning Possible null dereference Null if a i lt m A Execution trace information Completed 0 loop iterations in Bag java line 14 col 4 Bag java 15 Warning Array index possibly too large IndexTooBig if a i lt m A Execution trace information Completed 0 loop iterations in Bag java line 14 col 4 Bag java 21 Warning Possible null dereference Null a mindex a n A Execution trace information Completed 0 loop iterations in Bag java line 14 col 4 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 9 of 86 Bag java 21 Warning Possible negative array index IndexNegative a mindex a n A Execution trace information Completed 0 loop iterations in Bag java line 14 col 4 5 warnings Remark Actually the above is the output generated by the command escjava quiet Bag java The normal output of ESC Java also includes various progress messages and timing information which are omitted here Remark Some of the messages above include a part marked as Execution trace information We say more about execution traces below particularl
100. language that includes first order predicate calculus with equality and uninterpreted function symbols along with some interpreted function symbols of arithmetic Since the true theory of arithmetic is undecidable Simplify is necessarily incomplete In fact the incompleteness of Simplify s treatment of arithmetic goes well beyond that necessitated by G del s Incompleteness Theorem In particular e Simplify has no built in semantics for multiplication except by constants e Simplify doesn t support mathematical induction Also first order predicate calculus FOPC is only semidecidable that is all valid formulas of FOPC are provable but any procedure that can prove all valid formulas must loop forever on some invalid ones But it is not useful for Simplify to loop forever since ESC Java issues warnings only when Simplify reports potential counterexamples Therefore Simplify will sometimes report a potential counterexample c even when it is possible that more work could serve to refute c and even to prove the entire verification condition More particularly e The way Simplify makes use of a universally quantified formula say forall T ti tn B is by selectively instantiating the body 8 with substitutions for t1 tn determined by matching 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 84 of 86 certain triggering patterns against a s
101. lass path about the same way that a Java compiler does except that ESC Java prefers spec files over java files See the fine points below for a more complete but not completely complete story Fine points Note Some of the behaviors in described in the next few paragraphs change when ESC Java is run with the depend command line option See section 5 1 4 for details For each filename F on the command line ESC Java looks for the exact file F with relative path names evaluated from the current working directory If ESC Java can t find file F it issues an error message and 08 02 2005 17 56 ESCJ 27 74 of 86 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes goes on to look for the next file if any If ESC Java finds file r then it reads file F in full mode as a Java source file regardless of the filename extension storing the type declarations it reads in an internal cache Once ESC Java has read and cached the type declarations from files named on the command line it may then need the declarations of additional types used directly or indirectly by the types already read When ESC Java needs the declaration of a type P T it can find it in any of the following places 0 already in ESC Java s internal cache 1 ina file named c P T spec where P is the relative path name whose directory path components are the simple name components of P taken in order e g on Unix
102. lds that are not in scope at the point where the overridden method is declared such as private variables of the class declaring the overriding method To reduce the likelihood of unsoundness also_modifies pragmas ought not to name modification targets that are accessible JLS 6 6 from the scope of the overridden method However the current ESC Java does not enforce any such restriction For more discussion of the problem of specifying modification targets in the presence of subclassing and for a sound solution thereof see Leino98 2 4 Pragmas for specifying data invariants This section describes several pragmas that ESC Java provides for specifying properties of variables and data structures 2 4 0 non_null pragma A non_null pragma is a modifier pragma It may modify the declaration of a variable of a reference type The variable may be a static field instance variable local variable or parameter It has the form non_null The pragma causes ESC Java to check at each assignment to the variable that the value assigned is not null and to assume at each use except in one case described below that the value is not null When a formal parameter declaration is annotated with a non_null pragma ESC Java checks at each call site that the corresponding actual is not null Fine points In the case that a non_nu11 instance variable x is declared in a class c and a read access of x occurs in a constructor of c that does not call a sibli
103. lso be useful in their own right see particularly section 2 2 3 2 1 0 nowarn pragma A nowarn pragma is a lexical pragma It has the form nowarn L opt where 1 is a possibly empty comma separated list of warning types from the following list ArrayStore Invariant Post Assert Loopinv Pre Cast NegSize Race Deadlock NonNull Reachable Exception NonNulltInit Unreadable IndexNegative Null Uninit IndexTooBig OwnerNull ZeroDiv The pragma suppresses any warning messages of the types in x that are associated with the line on which the pragma appears If is empty all warning types are suppressed See section 4 for descriptions of the different types of warnings Fine points 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 20 of 86 Some ESC Java warning messages refer to two source code locations namely 1 a location indicating the control point where an error could potentially occur at run time and 2 the location of a pragma or occasionally a Java declaration associated with the warning In such cases the warning can be suppressed by a nowarn pragma on either of the indicated source lines The nowarn pragma is potentially unsound and should be used only in cases where the programmer is willing to take responsibility that the suppressed warnings are really false alarms The primary intended use of nowarn pragmas is where the suppressed warnings co
104. lue of each actual parameter of the call including the implicit this parameter of an instance method call satisfies every relevant to R instance invariant of every supertype of the static type of the corresponding formal parameter ESC Java checks that the value of each static field actually each of a heuristically selected set of relevant static fields satisfies every relevant to R instance invariant of every supertype of the static type of ESC Java assumes that all relevant to R static invariants hold after the call ESC Java assumes that after the call each relevant to R object invariant of type r holds for all instances of r for which held before the call and for all instances of T allocated by the call except that when a constructor calls a superclass constructor ESC Java assumes that the constructed object satisfies the instance invariants of the supertype but not necessarily any additional invariants of the subtype ESC Java checks that at the end of R s body all relevant static invariants hold and all relevant instance invariants hold for all allocated objects except that if R is a constructor ESC Java assumes that the constructed object satisfies all relevant object invariants of R s type including those inherited from supertypes but not necessarily those of any subtypes of R whose constructors may call R as a superclass constructor and furthermore when considering abnormally terminating executions
105. ly in natural language comments o ESC Java s pragmas support modular checking The checking done by ESC Java is modular When checking the body of a routine that is a method or constructor r ESC Java does not examine bodies of routines called by r Rather it relies on the specifications of those routines as expressed by requires pragmas by other pragmas described below and by Java constructs such as signatures return types and throws clauses Conversely to check the body of r ESC Java does not examine callers of r It does however assume that r is called only in accordance with its own specification o When Java sources are unavailable users can supply pragmas in spec files When the file declaring a class T uses a type uv ESC Java may need data invariants of u and or specifications of u s routines in order to check the routines of T If ESC Java can find only a binary class file and no source file declaring v then it will assume simple default specifications for the routines of u based on their signatures The user can supply additional specifications for the routines of u and also invariants for u by putting them in pragmas in a file U spec A spec file is like a java file except that it is allowed to omit method bodies Section 5 1 tells more about spec files Section 2 includes descriptions of all ESC Java pragmas ESC Java is checker for almost all of Java 1 2 ESC Java is targeted for Java 1 2 as described in
106. mas on lines 14 and 35 guarantee that the invariant on line 6 is established by the Bag constructor and preserved by the extractMin method Example specifying a generic queue Consider a class that implements queues of object s There is a constructor that creates an empty queue and there are instance methods for enqueueing and dequeueing elements and for testing whether a queue is empty public class Queue public class Queue public enqueue Object e public boolean isEmpty public Object dequeue throws In the absence of any annotations a number of problems come up when checking clients of the Queue class First there is no check against calling dequeue on an empty queue Second a user may wish to have a queue whose elements are all of some type T a proper subtype of Object Since the result type of dequeue is Object the user will frequently have to cast the result of dequeue to a T TE aor Queue q new Queue q enqueue t u T q dequeue Given the code fragment above ESC Java has no way to know that the cast will succeed Finally it is common for queues and other such container objects to contain only non null elements When a queue is intended to contain only non null elements it would be nice to have ESC Java check that only non null elements are enqueued and on the other hand not issue spurious warnings about potential null dereferences o
107. me kind of warning message Warning Possible assertion failure Assert Implicitly introduced assertions on the other hand give rise to a wide variety of more specific messages e An assert pragma can occur only where a Java statement can occur but implicitly introduced assertions are not limited to statement boundaries For example given the statement p m q q i ESC Java makes sure that the implicit assertion that array q is non null is introduced at a control point after the call to method n and that the implicit assertion that index i is in bounds is introduced at a control point after i is incremented For the user to introduce explicit assertions at these points it would be necessary to modify the Java source code breaking the statement into several parts and introducing a temporary variable for the result of the call to m e An assert pragma introduces a single assertion at the control point where it occurs In contrast a single other pragma or built in checking rule can introduce many assertions throughout the program for example at every call of a given method or at every access to a given variable e The systematic introduction of assertions at certain points in a program sometimes makes it possible for ESC Java safely to introduce assumption at other points In short the various pragmas and built in checking rules provided by ESC Java enable the introduction of collections of assertions and assumptions in a m
108. n evaluates to null 3 2 2 elemtype An expression of the form elemtype E where is a specification expression of type TYPE is a specification expression of type TYPE If denotes an array type T then elemt ype E denotes T Otherwise the value of elemt ype E is unspecified 3 2 3 Subtype lt An expression of the form s lt T where s and T are specification expressions of type TYPE is a specification expression of type boolean It denotes that s is a subtype of T including the case where s is equal to 7 The operator lt has the same binding power as the relational operators lt gt lt and gt 3 2 4 Examples involving TYPE type typeof elemtype and lt Suppose file T java contains the following declaration class T requires a null amp amp 0 lt i amp i lt a length static void storeObject T a int i T x ali x 50 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 51 of 86 When checking the body of the storeobject method ESC Java will produce an arrayStore warning section 4 1 for the assignment The problem is that so far as ESC Java can tell the actual type of a at the time of the call might be s 1 where s is some proper subtype of T and x might not be of type s Consequently the attempt to store x into a i might give rise to an ArrayStoreException
109. n dequeued objects Here is a spec file see section 5 1 2 for the Queue class with annotations addressing the issues described above public class Queue ghost public int size invariant size gt 0 ghost public TYPE elementType ghost public boolean canHoldNull ensures elementType type Object ensures canHoldNull 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 44 of 86 ensures size 0 public Queue requires typeof e lt elementType e null amp canHoldNull modifies size ensures size old size 1 public void enqueue Object e ensures result size 0 public boolean isEmpty requires size gt 1 modifies size ensures typeof result lt elementType result null amp canHoldNull x ensures size old size 1 public Object dequeue The specification expression constructs TYPE type typeof and lt are explained in sections 3 0 3 2 0 3 2 1 and 3 2 3 respectively Given the specification above the user can express the intention to use a queue q to hold only non null elements of type T by writing Queue q new Queue set q elementType type T set q canHoldNull false ESC Java will then warn of a possible precondition v
110. n pragma the assume pragma is potentially unsound and should be used only if the programmer is willing to take responsibility that z holds whenever control reaches the pragma or at least is willing to give up further checking for any execution paths on which is false When faced with the choice of using either an assume pragma or a nowarn pragma to suppress a spurious warning it is preferable to use an assume pragma if it is practical to do so since the assume pragma more explicitly documents your assumptions about the behavior of the program The sentence In other words for any execution path from that point on may have seemed unclear to some readers For some more examples of its meaning consider the following code fragment 31 if u null v null e 10 32 if v null 33 w a f 34 assert b null 35 assume a null amp b null amp c null amp d null amp e gt 0 36 x c f 37 assert d null 38 else 39 C new 40 d v 41 42 y a g 43 assert b null 44 Z C G 45 assert d null 46 assert e gt 0 When ESC Java checks this code e ESC Java will not warn of a possible dereference of nu11 at line 36 or of a possible assertion failure at line 37 because the only way control can reach those lines is by first reaching the assume pragma at line 35 e The assume pragma at line 35 will not prevent ESC J
111. ncern situations that are impossible in practice but for reasons beyond ESC Java s ability to discover Another use would be to suppress warnings for circumstances that are actually harmless and where the programmer is willing to take responsibility that they are harmless For example a nowarn pragma might be used to suppress a warning for a null dereference if the resulting exception would be caught by a handler but in such a case the current ESC Java will not check that there actually is a handler nor will it check for any errors that might occur during or after execution of the handler The nowarn pragma suppresses warnings on a line by line basis ESC Java also provide command line options that enable and disable checking at a much coarser grain see the descriptions of the nowarn warn start routine and routineIndirect options on the escjava 1 man page Unlike warning messages ESC Java error messages cannot be suppressed by nowarn pragmas Error messages report conditions that prevent ESC Java from making enough sense of the program to do further checking Bug The current ESC Java does not allow another pragma to follow a nowarn pragma in the same pragma containing comment Since the only lexical pragma in the current ESC Java is nowarn and since you can say with one nowarn pragma anything that you can say with two this should not cause problems in practice 2 1 1 assert pragma An assert pragma is a statement pragma It has
112. nces nor does it check that they establish or maintain static or instance invariants C 0 10 Class paths and spec files Java javac 5 java 5 and ESC Java escjava 1 when run with the same class path make different choices between spec java and class files The current ESC Java doesn t check that the contents of the file it chooses are related to the contents of the file javac 5 would choose Consider for example a scenario where a file Foo java uses a class Bar and where both a Bar java and a Bar spec file can be found on the class path In response to the command escjava Foo java ESC Java will check the routine bodies in Foo java under the assumption that calls to methods of Bar have the semantics specified in Bar spec ignoring the file Bar java In response to the command escjava Bar java ESC Java will check the method bodies in Bar java against the specifications in Bar java ignoring the file Bar spec In neither case is there any checking that either the specifications or the bodies of routines in Bar java have any connection to the specifications of corresponding routines in Bar spec or even that Bar java and Bar spec declare routines with the same names and signatures Note in particular that the specifications in the spec files available for download via the ESC Java web site see appendix B may disagree agree with the actual semantics of the corresponding JDK classes and interfaces for any of a variet
113. nfers the invariant f null Limitation The static bodies and static initializers of a class are supposed to establish the static invariants declared in the class but the current ESC Java does not check this Thus the responsibility for initial establishment of static invariants lies entirely with the user 2 4 2 axiom pragma An axiom pragma is a declaration pragma It has the form axiom E i opt where is a boolean specification expression The pragma causes ESC Java to assume that which we call an axiom is true at the start of every routine body that it checks Fine points Since the axiom pragma introduces assumptions without introducing reciprocal checks it is potentially unsound and programmers should use it carefully An obvious use of an axiom pragma would be to state some universally true fact For example the built in capabilities of Simplify Simplify 1 the theorem prover used by ESC Java include a decision procedure for linear arithmetic but no rules about multiplication other than by constants Thus there may be cases where ESC Java would be helped by an annotation like axiom forall int x y x gt 0 amp y gt 0 gt x y gt 0 recall that ESC Java doesn t claim to check for arithmetic overflow so an axiom like this is consistent with the view that Java int s behave like the mathematical integers although this view is not true Beware that profligate introduction of axioms in the hope th
114. ng constructor then ESC Java does not automatically assume that the value read will be non null ESC Java allows a non_null pragma to modify a formal parameter even though Java 1 0 syntax does not allow modifiers on parameter declarations A non_null pragma may not modify a parameter declaration of a method that overrides another method Sometimes the same design decision might be expressed either by a non_nul1 pragma or by some other kind of pragma such as a requires pragma or an invariant pragma For example instead of using a 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 33 of 86 requires pragma in section 0 2 requires input null Bag int input we might have written Bag non_null int input and instead of using a non_nul1 pragma in section 0 3 class Bag non_null int a we might have written class Bag int a invariant a null In each of these cases the alternative annotations have slightly different semantics but either alternative would be adequate to enable checking of our example program The differences are that the non_null pragmas are checked at every assignment to input or a whereas the requires pragma would allow assignments of null to input within the body of the Bag constructor and the invariant pragma would be checked only at routine calls as explained in section 2 4 1 We
115. ns o ESC Java warning messages may include execution traces ESC J ava issues error messages for badly formed programs o ESC Java error messages are like compiler error messages o ESC Java doesn t detect all compile time errors that Java compilers detect ESC J ava s extended static checking isn t perfect o ESC Java can miss errors o ESC Java can give spurious warnings o Pragmas give the user some control over ESC Java s unsoundness and incompleteness o ESC Java issues caution messages in some but not all cases where unsound checking may occur 2 ESC Java pragmas 2 0 Rules about where pragmas may occur 2 0 0 ESC Java pragmas must occur within pragma containing comments 2 0 1 There are four syntactic categories of pragmas 2 0 2 ESC Java sometimes allows pragmas to contain nested pragmas or comments 2 1 The most basic pragmas 2 1 0 nowarn pragma 2 1 1 assert pragma 2 1 2 assume pragma 2 1 3 unreachable pragma 2 2 Some remarks concerning assert and assume 2 2 0 The assume pragma should be used with judgment 2 2 1 Most ESC Java pragmas are just fancy forms of assert and assume 2 2 2 A nowarn pragma suppresses warnings by turning assertions into assumptions 2 2 3 A helpful tip Experiments with assert and assume pragmas can help you understand ESC Java s behavior and debug your annotated code 2 3 Pragmas for specifying routine
116. ns of these operators are allowed in specification expressions even though ordinary method invocations are forbidden as stated in section 3 1 Bound variables introduced by forall and exists are scoped like Java local variables as are the variables declared to name exceptions in exsures and also_exsures pragmas For example in a quantified expression forall int k a k 0 the declaration int k introduces the bound variable k whose scope is the SpecExpr aik 0 Furthermore just as Java forbids declaration of an identifier as a local variable within the scope of a parameter or local variable of the same name JLS 14 3 2 so ESC Java forbids declaration of an identifier as a bound variable within the scope of a parameter local variable or bound variable of the same name Consequently the quantified expression forall int k a k 0 cannot occur ina scope where there is already a parameter local variable or bound variable named k The scoping rules of routine parameters fields this and super are slightly different from those in Java In particular e When a SpecExpr occurs in a modifier pragma section 2 0 1 applied to a field names in the SpecExpr are resolved as if the SpecExpr were part of the initializer of the field Consequently if the field is an instance variable then this and super can be mentioned and any unqualified field name f is a synonym for this While Java forbids field initializers from using other fiel
117. nsion to the Java type system Section 3 1 describes notations allowed in Java expressions but forbidden in specification expressions Section 3 2 describes additional notations allowed only in specification expressions Section 3 3 describes how the rules for scoping name resolution and access control in specification expressions differ from those in Java Specification expressions are never actually evaluated when a Java program is run and ESC Java will not produce specific warnings about specification expressions whose evaluation if they were evaluated might dereference nu11 access arrays out of bounds etc Rather the meanings of such expressions for example where if it were actually evaluated would evaluate to nu11 are unspecified functions of the meanings of their subexpressions In most cases attempts to prove things about such unspecified values will fail thus giving rise to warnings of some sort though alas not the clearest warnings that one could hope for For example given the program fragment assume nonnullelements a assert a j null in a place where j might be negative ESC Java will produce an Assert warning section 4 2 rather than an IndexNegat ive warning section 4 6 3 0 Specification types Like Java expressions specification expressions have types which we call specification types A specification type is either a Java type or one of the special types TYPE or LockSet or an array
118. nt m Integer MAX_VALUE 7 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 8 of 86 3 int mindex 0 4 for int i 1 i lt n i 5 if a i lt m 6 mindex i 7 m ali 8 9 20 n 21 a mindex a n 22 return m 23 24 A copy of this program is in escjavaRoot examples 0 0 Bag java where escjavaRoot denotes the site specific top level directory for ESC Java see appendix B The idea is that an object x of class Bag represents a multiset also known as a bag of integers in the form of integer array x a together with an integer x n where the elements of the multiset are the first x n elements of the array In our example declaration we define a constructor that creates a Bag from an array and a single method ext ractMin that finds removes and returns the minimal element of a Bag The ext ractMin method iterates over the first this n elements of this a keeping track of the smallest one in the local variable m After finding the smallest element of this a it copies the element at the highest used position of x a into the position formerly occupied by the minimum element decreases the count of used elements and returns the value that was saved in m 0 1 Scene 1 We run ESC Java and it warns of two potential nu11 dereferences To compile Bag java we would type the command line javac Bag java To chec
119. ny places we cite sections of The Java Specification Language by James Gosling Bill Joy and Guy Steele JLS For example the notation JLS 19 2 refers to section 19 2 of The Java Language Specification The list of references at the end of this manual gives bibliographic information for this and other works cited herein A specification notation and set of tools related to ESC Java is the Java Modeling Language JML LBR99 LBROO LLPRJOO Through a collaborative effort we have attempted to make the JML specification language and the ESC Java annotation language as similar as practical with JML providing a superset of the features of ESC Java The goals of the two languages are different so differences in the notations remain However many programs annotated with ESC Java annotations should be amenable to 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes processing with other JML tools and programmers who learn one language should have little trouble picking up the other as well Acknowledgments ESC Java was originally designed and implemented at the Compaq Systems Research Center SRC by Cormac Flanagan Mark Lillibridge Raymie Stata and the authors Todd Millstein implemented ESC Java s execution trace facility and helped with other aspects of ESC Java Caroline Tice and Rajeev Joshi lent helping hands with miscellaneous aspects of the implementation inclu
120. o in which the conditions brokenObj this brokenObj a this a both hold Having added this invariant the user must also supply a set pragma in order to guarantee that the constructor for 0bjStack establishes the invariant 9 ObjStack 10 n 0 11 a new Object 10 12 set a owner this 13 Without the set pragma ESC Java will generate a warning that the constructor fails to establish the invariant a owner this Fine points Just as all constructors have the implicit postcondition fresh result see section 2 3 2 all constructors including the implicit constructors for arrays have the implicit postcondition this owner null In the example above this implicit postcondition guarantees that this a owner null after line 11 If this a owner could have had some non null value call it brokenob3 after line 11 then the set pragma might cause the invariant on line 7 to be violated for brokenobj Another way to guarantee that no two objStack s share the same a field would be to include in the declaration of 0bjStack the static invariant forall ObjStack x y x y gt x a y a The instance invariant a owner this is not only more succinct than the static invariant above but also stronger To see why suppose we had another class Foo which declared a field b and the instance invariant b owner this Then the invariants a owner this for 0bjStack and b owner this for Foo
121. of this brokenObj lt 3 gt this brokenObj lt 3 gt null In this display some inflected form of the identifier BrokenObj is used to name the object for which the invariant is broken known as the broken object If as in the example above the displayed formulas tell what the broken object is not equal to but don t tell what it is equal to then the likely cause of the warning is that the program modifies some field call it of some object call it t and that ESC Java hypothesizes that this modification might break the invariant for some other object for example a hypothetical object u such thatu t butu f t f Ifthe programmer s intention is that no such sharing of fields can occur the programmer can communicate this intention to ESC Java by supplying an appropriate invariant near the declaration of the field for example invariant this f owner this For a more detailed example of the scenario outlined above see the discussion of the owner field and its use in section 3 2 17 Fine points The command line option plainwarning suppresses output of partial counterexample contexts in Invariant warnings This may be useful in cases where ESC Java s output is read by another program 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 68 of 86 In the partial counterexample context in an Invariant warning for a constructor the object being con
122. of the constructor R ESC Java makes no assumptions about the constructed object It is a potential source of unsoundness for an object invariant to mention fields other than those declared in the class declaring the invariant For example suppose that s is a subclass of T and that an instance invariant of s mentions a field declared in T and consider a routine R containing an assignment x f where x has static type T If x has allocated type s the assignment might break the instance invariant declared in s But neither the programmer of R nor ESC Java can reasonably be expected to enforce the invariants of s since s might not be in scope in R and indeed might be written after R The current ESC Java does not attempt to detect declarations of such unenforceable invariants but future versions 08 02 2005 17 56 ESCJ 27 35 of 86 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes may bring some such declarations to the programmer s attention For a more detailed examination of the unenforceable invariant problem see LS97 When a final field fis declared with a Variblelnitializer JLS 19 8 2 ESC Java may infer some simple invariants automatically For instance if the initializer is a constant expression JLS 15 27 c not of type String then ESC Java infers the invariant c and if the initializer is a string literal an array constructor or an invocation of new then ESC Java i
123. ograms for race and deadlock checking typically requires use not only of monitored and or monitored_by pragmas but of other pragmas as well most commonly requires pragmas section 2 3 0 and axiom pragmas section 2 4 2 involving the locking order lt section 3 2 7 and the lock set lockset section 3 2 5 Rather than leave it to the reader to assemble the big picture from fragments of information scattered over many sections of this manual we present here a few examples to show how the pieces fit together In specification expressions the special ESC Java identifier lockset refers to a special variable called the lock set denoting the set of all objects held as locks by the current thread For testing membership of locks in the lock set we overload the array subscripting notation so that lockset X is true when object x is in the lock set lockset Thus given the instance field declarations T f U g monitored_by f g V h the code fragment x h y h is treated roughly like assert y null Check for null dereference assert y f null amp amp lockset y f y g null amp amp lockset y g Check for race section 4 17 on read assert x null Check for null dereference assert x f null x g null amp x f null gt lockset x f amp x g null gt lockset x g Check for race on write The necessary conditions to es
124. on being warned of including a parenthesized warning type name and indicates a source code location the dynamic location of the warning for the control point at which the condition potentially occurs For some warning types the message additionally indicates the source code location of the first character of the initial keyword of the pragma the warning s associated pragma that causes ESC Java to regard the condition as a run time error If the warning is an Invariant warning the message will usually include a partial counterexample context which may be of help to the user to tell which object that might so far has ESC Java can determine have its one of its invariants violated and why An ESC Java warning message may include an execution trace listing interesting see the fine points 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 63 of 86 below control decisions on some execution path that so far as ESC Java can determine may plausibly lead to the run time error mentioned in the warning Finally an ESC Java might list some labels that occur in pragmas an are relevant to the scenario being warned about See section 3 2 16 for some examples Example Suppose the file c java contains the following class declaration 1 class C 3 int i 4 int x 5 invariant i gt 0 6 gt x null 7 8 9 void m int p int
125. ons detected by ESC Java are conditions that would be detected by the Java run time system and give rise to exceptions specifically NullPointerException IndexOutOfBoundsException ClassCastException ArrayStoreException ArithmeticException and NegativeArraySizeException JLS 11 5 1 1 The current ESC Java treats these conditions as errors and generates warnings for them even if the program actually catches the resulting exceptions Accordingly our use of the word error in this manual includes such conditions Future versions of ESC Java may provide support for checking programs that catch exceptions thrown by the Java run time system The current ESC Java version does support checking of programs that catch explicitly thrown exceptions including those just listed o ESC Java does not warn of potential errors in the evaluation of specification expressions Specification expressions are never actually evaluated and with one exception described in section 2 6 1 ESC Java will not produce specific warnings about specifications expressions whose evaluation might dereference nu11 access arrays out of bounds etc Rather the meanings of such expressions for example o where o if it were actually evaluated might evaluate to null are an unspecified function of the meanings of their subexpressions In most cases attempts to prove things about such unspecified values will fail thus giving rise to warnings
126. ontaining the call ESC Java will use the specification of T m but the actual call even in the absence of other sources of unsoundness might only meet the weaker semantics specified for U m In particular e If u mis declared with an also_modifies pragma the call might modify parts of the state that are 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 80 of 86 specified as modification targets of u m but not of T m but ESC Java will check the implementation of r under the assumption that the call modifies only the targets specified for T m This would be a source of unsoundness even if ESC Java guaranteed that u m modifies only its specified modification targets which it doesn t as just mentioned in section C 0 3 Rustan Leino Leino98 has designed a programming methodology that would avoid this unsoundness but in the current ESC Java we have decided to leave it to the programmer to use also_modifies with care so as to avoid introducing the unsoundnesses described in Leino s paper If u mis declared with an also_requires pragma then ESC Java will use the preconditions specified in the also_requires pragma when it checks the implementation of U m but will not enforce those preconditions at the call m C 0 5 Multiple inheritance ESC Java treats multiple inheritance of preconditions and modification targets unsoundly Suppose that a method c m inherits from
127. or declarations that does not override any other method declaration and neither a requires pragma nor an also_requires pragma may modify a method declarations in classes that overridden declaration in a superclasses or a method declaration in an interface that overrides a method declaration in a superinterface Fine points The also_require pragma is a potential source of unsoundness Suppose method c m of class c overrides method I m of interface 1 When checking a call of the form m where is an expression of type 1 ESC Java only enforces the preconditions of I m and not any preconditions given by also_requires pragmas modifying the declaration of c m However the expression might evaluate to a value of type c causing the call to invoke c m and the correctness of c m s implementation may depend on preconditions given in such also_requires pragmas The reason that ESC Java includes an also_requires pragma despite its unsoundness is that it is often essential for preconditions of a method c m to mention instance variables of class c and Java does not allow instance variables to be declared in interfaces Note however that ESC Java does allow declarations of ghost variables section 2 6 0 in interfaces In addition to the potential unsoundness just described the also_requires pragma shares the potential unsoundness of the require pragma in the presence of multiple inheritance see section C 0 5 2 3 8 also_modifies pra
128. or example if a private field of a class is declared with a spec_public pragma then the field can be mentioned in pre and postconditions of a public method but clients of the class cannot modify the field directly Example Consider the Bag example form section 0 In presenting this example we glossed over the issue of accessibility To allow clients of the Bag class to make use of the routines of the class Bag ext ractMin and others that we might add these routines should be declared public On the other hand the fields a and n used in the implementation ought not to be public For example arbitrary clients ought not to be able to write these fields except by calling routines of the Bag class If we simply declare the routines but not the fields of Bag to be public ESC Java will complain ESC Java input from Bag java 1 class Bag 2 non_null int a 3 int n 13 requires n gt 1 14 public int extractMin ESC Java output Bag java 13 Error Fields mentioned in this modifier pragma must be at least as accessible as the field method being modified perhaps try spec_public requires n gt 1 Caution Turning off extended static checking due to type error s 1 caution 1 error If programmers using the Bag class are not supposed to know that its implementation includes the field n then it is unreasonable to expect them to establish a precondition involving n before calling extractMin
129. os or lblneg expression is part of a separate name space The 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 62 of 86 label does not become available for use inside the SpecExpr A label is permitted to have the same name as an identifier already in scope or as a label in an enclosing labeled expression If a label has the same name as an identifier already in scope it does not hide that identifier 4 Warnings ESC Java issues warnings for conditions that it regards as run time errors and that so far is it can tell might actually occur at run time The potential conditions that give rise to some ESC Java warning types specifically Nu11 IndexNegative IndexTooBig Cast ArrayStore ZeroDiv and NegSize are conditions that would be detected by the Java run time system and give rise to exceptions specifically NullPointerException IndexOutOfBoundsException ClassCastException ArrayStoreException ArithmeticException and NegativeArraySizeException The current ESC Java regards these conditions as run time errors and generates warnings for them even if the program actually catches the resulting exceptions Fine point In some cases multiple warnings may arise from the same cause For example if a variable is dereferenced in multiple arms of a switch statement but is not dereferenced before the switch statement and ESC Java cannot confirm t
130. pe constructor which subsequently terminates abnormally e When a constructor of a class Tis called as a supertype constructor from a constructor of a subtype S the supertype constructor may establish the instance invariants of T for this then perform a method call this m that dynamically dispatches to s m However the correctness of the body of s m might depend on instance invariants declared in s and not established at the call site For a more detailed examination of the constructor leaking problem see LS97 In addition to the problems with invariants described above constructor leaking can result in unsound checking of race conditions When checking a constructor body ESC Java does not require that any lock be held in order to accesses a field of this even if the field is declared with at monitored_by or monitored section 2 7 1 pragma The reason is that ESC Java assumes that no other thread yet has access to this and thus that no actual race can result If this assumption is false for example if the constructor stores this into a globally accessible data structure from which another thread can read it unsound checking in the form of undetected race conditions could result C 0 9 Static initialization The current ESC Java does not perform extended static checking of static initializers JLS 8 5 and initializers for static fields It neither checks for the possibility that they do not give rise to errors such as null derefere
131. pecial identifier result section 3 2 14 may occur within an argument to o1d In this context result denotes as usual the value returned by the method despite the fact that the returned value may not even be allocated in the pre state in which case the meaning of a field access result f or an array access result i is unspecified Similarly any occurrence of this explicit or implicit in a normal postcondition of a constructor denotes the constructed object even within an argument of old 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes The following correctly annotated code example illustrates the semantics of old class C static C x oldx y int f static int oldxf static int a olda b static int oldai static int i requires x null amp y null requires a null amp amp 0 lt i amp i lt a length modifies oldx oldxf x x f olda oldai a ali i ensures oldx old x ensures oldxf old x f ensures old x f old x f 1 ensures exists C z z x amp old z f old y f ensures olda old a amp oldai old a i ensures old a old i old a i 1 static void m oldx x oldxf x f x y oldx f olda a oldai a i a b olda i i Note the distinctions between
132. q 0 10 1 int t 2 f p null 3 t p 4 else 5 t q 6 7 x t 8 3 Then the output from the command escjava C java includes one warning message The primary part of the warning message indicates that the some invariant might not hold when control reaches the end of the method m CC java 18 Warning Possible violation of object invariant Invariant A The next part of the warning message gives the associated pragma an invariant pragma starting on line 5 Associated declaration is C java line 5 col 6 invariant i gt 0 AN The ellipsis indicates that the associated pragma may continue beyond the part that is shown in the message In this case it extends onto the next line of the program Since this is an Invariant warning it includes a partial counterexample context Possibly relevant items from the counterexample context brokenObj this 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 64 of 86 brokenObj refers to the object for which the invariant is broken Here we see that the object whose invariant might be violated is this that is the object whose m method is being executed The final part of the warning message is an execution trace indicating a scenario in which the right hand side c of the assignment on line 12 might in fact evaluate to null Execution trace inform
133. r example the meanings of the inflections pre 3 6 and 3 6 lt 1 gt on the field name a is beyond the scope of this manual Appendix B Installing and using ESC Java at your site The ESC Java group maintains a web site at http research compag com SRC esc The tool may be downloaded from this site for educational and research use After you download the ESC Java release according to the instructions on the web site all files in the release will be in a single directory chosen by you at your site We will write escjavaRoot to denote 76 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 77 of 86 this directory Among the contents of escjavaRoot are the following files and subdirectories e escjavaRoot bin escjava on Unix or escjavaRoot bin escjava bat on Windows contains the execution script for ESC Java The web site includes instructions for setting things up so that a command of the form escjava options sourcefiles will run this script e escjavaRoot doc manl escjava 1 contains the Unix man 1 page for ESC Java e escjavaRoot doc escjava html contains the man page for ESC Java in HTML format e escjavaRoot examples contains some examples of source code on which to run ESC Java including the Bag example from section 0 Subdirectories named after sections of this manual contain examples taken from or pertinent to those sections e escjava
134. r of paths that are really possible Because of this simplification the checker doesn t need an invariant to analyze the loop If you do include a loop invariant ESC Java will check that it holds both initially and after the single loop iteration that the current checker considers Consequently the checking performed on loop_invariant E while B S is actually the same as would be done for assert E but giving a LoopInv warning if B S assert E but giving a LoopInv warning assume B don t check later code for case B true where execution of a continue in s results in normal termination of s and execution of a break in s results in normal termination of the entire code fragment above You can make ESC Java check more or fewer iterations of loops by using the loop command line option see section C 0 1 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 38 of 86 2 5 Pragmas affecting conditions under which variables may be referenced 2 5 0 spec_public pragma A spec_public pragma is a modifier pragma It may occur as a modifier only of a non public field declaration It has the form spec_public The effect of the pragma is to make the fields declared in the declaration be as spec accessible that is accessible in pragmas see section 3 3 as they would have been if the declaration had been public F
135. rch compaq com pub DEC SRC technical notes Appendix C Sources of unsoundness and incompleteness ESC Java C 0 Known sources of unsoundness C 0 0 Trusting pragmas C 0 1 Loops C 0 2 Object invariants C 0 3 Modification targets C 0 4 The also_modifies and also_requires pragmas C 0 5 Multiple inheritance C 0 6 Arithmetic overflow C 0 7 Ignored exceptional conditions C 0 8 Constructor leaking C 0 9 Static initialization C 0 10 Class paths and spec files C 0 11 Shared variables C 0 12 Initialization of fields declared non_nu11 C 0 13 String literals C 0 14 Search limits in Simplify C 0 15 Integer arithmetic bug in Simplify C 1 Some sources of incompleteness C 1 0 Incompleteness of the theorem prover C 1 1 Incomplete modeling of Java semantics C 1 2 Modular checking References 0 An illustrative example of using ESC Java To give the reader a general idea of what ESC Java does and how to use it we begin with an example illustrating some salient features of ESC Java through its application to a simple class declaration deliberately seeded with some errors 0 0 Scene 0 We write a class declaration Our example is the class Bag declared in a file Bag java as follows line 1 class Bag 2 int a 33 int n 4 5 Bag int input 6 n input length 7 a new int n 8 System arraycopy input 0 a 0 n 9 10 11 int extractMin 12 i
136. rise where it is convenient to nest a comment inside a pragma or where it is convenient or even necessary to nest a pragma inside another pragma In particular this is the only way to annotate a ghost field see section 2 6 0 with a modifier pragma We describe here the rules governing such nesting Readers may wish to skip the remainder of this section on first reading of the manual or until occasion for using such nesting presents itself In the current ESC Java a pragma containing comment call it inner may be nested inside pragma containing comment outer only in the following cases 1 each pragma in inner is a lexical nowarn pragma see section 2 1 0 or 2 each pragma in inner is a modifier pragma for a ghost variable declared in outer see section 2 6 0 for further details Furthermore outer must not itself be nested inside another pragma containing comment However outer may be of the form lt esc gt lt esc gt which must of necessity occur inside a Java documentation comment Any pragma containing comment outer even a nested one may have an ordinary i e non pragma containing comment inner nested inside it Also there are some restrictions concerning the syntactic forms of a nested ordinary or pragma containing comment inner and the enclosing pragma containing comment outer as given in the following table and the associated notes These restrictions ensure that the portions of the input file that
137. s 4 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 5 of 86 2 3 0 requires pragma 2 3 1 modifies pragma 2 3 1 0 target fields 2 3 2 ensures pragma 2 3 3 A note on the interaction of modifies and old 2 3 4 exsures pragma 255 also_ensures pragma 2 3 6 also_exsures pragma adel also_requires pragma 2 3 8 also_modifies pragma 2 4 Pragmas for specifying data invariants 2 4 0 non_null pragma 2 4 1 invariant pragma 2 4 2 axiom pragma 2 4 3 loop_invariant pragma 2 5 Pragmas affecting conditions under which variables may be referenced 2 5 0 spec_public pragma 23 1 readable if pragma 2 5 2 uninitialized pragma 2 6 Pragmas concerning ghost variables 2 6 0 ghost pragma 2 6 1 set pragma 2 6 2 Examples using ghost variables 2 7 Pragmas for specifying synchronization 2 7 monitored_by pragma 2 7 1 monitored pragma 2 7 2 Examples illustrating race and deadlock checking 3 Specification expressions 3 0 Specification types 3 1 Restrictions 3 2 Additions 3 2 0 type 3 2 1 typeof 3 2 2 elemtype 3 2 3 Subtype lt 3 2 4 Examples involving TYPE type typeof elemtype and lt 3 2 5 lockset 3 2 6 Membership in lock sets _ 3 2 7 Lock order lt and lt 3 2 8 max 3 2 9 Implication gt 3 2 10 forall 08 02 2005 17 56 ESCJ 27 E
138. s declared with at monitored_by or monitored section 2 7 1 pragma In some cases this can result in unsoundness see section C 0 8 All fields of the class containing the pragma are in scope in even those that are declared in textually later declarations class C extends B monitored_by g S f T g g in the pragma means this g not B this g The variables mentioned in z must be spec accessible section 3 3 anywhere the field itself is accessible JLS 6 6 For example a public field may not be monitored by a private lock unless the lock is declared spec_public see section 2 5 0 A field declaration may be modified by multiple monitored_by pragmas in which case the effect is as if there were a single monitored_by pragma listing all the locks mentioned in any of the actual monitored_by pragmas Bug limitation When ESC Java issues a Race warning for such a field it will mention only one of the monitored_by pragmas and possibly not the right one as the annotation associated with the warning 2 7 1 monitored pragma A monitored pragma is a modifier pragma It can occur only as a modifier of an instance variable declaration It has the form monitored and is semantically equivalent to monitored_by this 2 7 2 Examples illustrating race and deadlock checking 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes Annotation of pr
139. s for the same field f a Race warning for an access to f will mention only one of these pragmas and perhaps not the most relevant one 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 70 of 86 4 18 Reachable warning A Reachable warning warns that control may reach an unreachable pragma 4 19 unreadable warning An Unreadable warning warns that control may reach a read access to a variable when the expression in a readable_if pragma modifying the variable s declaration is false The warning is associated with the readable_if pragma 4 20 uninit warning An Uninit warning warns that control may reach a read access to a local variable before execution of any assignment to the variable other than an initializer in a declaration modified by an uninitialized pragma The warning is associated with the uninitialized pragma 4 21 ZeroDiv warning A ZeroDiv warning warns of a possible attempt to apply the integer division or remainder operator with zero as the divisor This condition would result in an Arithmet icException being thrown at run time JLS 15 16 2 15 16 3 5 Command line options and environment variables The operation of ESC Java is controlled by a variety of command line options and environment variables The primary source of information on these is the escjava 1 man page included with the ESC Java release see appendix
140. s warning may seem surprising the result of interpreting the second occurrence of as the pre state value of this would be even worse Under the latter interpretation ESC Java would issue no warnings about the body of incf but would assume after a call x incf both 1 that x had been incremented in accordance the postcondition and 2 that x was left unchanged in accordance with the unchecked empty set of modification targets Since these assumptions are mutually contradictory the result would be equivalent to assuming false and ESC Java would silently omit all checking after the call As an additional guard against omission of modifies pragmas ESC Java issues a caution message for any occurrence of old x in a postcondition of a method m unless 1 the expression x mentions some target field of m or 2 the expression x includes an array access and m has some modification target of the form A I or A Of course the interactions of modifies and old described above do not entirely make up for the fact that the current ESC Java does no checking of modifies pragmas A method declaration like modifies someOtherObject f instead of this f ensures f old f 1 void incf this f can still effectively disable checking of code following calls to incf 2 3 4 exsures pragma An exsures pragma is a routine modifier pragma It has the form exsures T t E opt or 29 of 86 08 02 2005 17 56 ESCJ
141. sc gt Of outer whichever is earlier 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 19 of 86 Examples Here are some examples of legal nesting of comments and pragmas inside pragmas e ghost public non_null comment Object o e requires a gt 0 comment 1 requires b gt 0 nowarn Pre comment 2 requires c gt 0 comment 3 void m int a int b int c Here are some examples of illegal nesting e ghost public non_null Object o e requires a gt 0 multi line nested comment Tip ESC Java s warning messages for these two examples of illegal nesting fail to give the line number on which the error occurs but do indicate that the problem is an unterminated comment You can localize the error by running a Java compiler on your program which is generally a good thing to do before running ESC Java anyway 2 1 The most basic pragmas In this section we describe the simplest ESC Java pragmas nowarn assume assert and unreachable The nowarn pragma is essentially a blunt instrument for getting ESC Java to shut up about uninteresting warnings thus helping to prevent ESC Java s known imperfections and limitations from becoming major sources of user annoyance The assert and assume pragmas are the fundamental pragmas of which most others are simply more elaborate forms see section 2 2 1 They may a
142. sidering many irrelevant instances Limitation Just as for invariants section 2 4 1 ESC Java limits its use of axioms to a restricted set of axioms considered relevant to the checking of any particular routine R In the current version of ESC Java the only axioms considered relevant are those declared in the same class as the implementation being checked Consequently there is no way for the user to declare libraries of potentially useful axioms 2 4 3 loop_invariant pragma A loop_invariant pragma is a statement pragma It has the form loop_invariant E opt where is a boolean specification expression A loop_invariant pragma must appear before a Java loop statement that is a Java for while or do statement JLS 14 10 14 11 14 12 or a Java labeled statement JLS 14 6 1 s such that sis a Java labeled statement Between the loop_invariant pragma and the associated loop statement there may be no intervening Java code and no intervening pragmas except for nowarn pragmas and other loop_invariant pragmas The pragma causes ESC Java to check that holds at the start of each iteration of the loop Fine points For the purposes of name scoping a loop invariant is treated as if it occurred just inside the associated loop statement That is if the associated loop statement is a for statement or a for statement wrapped within one or more labeled statements then the variables declared by the ForInit JLS 19 11 are in scope
143. ss in the absence of clear need In particular we have no plans for creating any connection between Java s Reflection API Refection and ESC Java s specification type TYPE C 1 2 Modular checking ESC Java s use of modular checking modular checking causes it to miss some inferences that might be possible through whole program analysis When translating a method call m ESC Java uses the spec of m for the static type of even if it is provable that the dynamic type of at the call site will always be a subtype that overrides m with a stronger spec ESC Java makes no attempt to infer method specifications However see FLOO FJLxx 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 85 of 86 References DLNS98 David L Detlefs K Rustan M Leino Greg Nelson and James B Saxe Extended Static Checking Compaq SRC Research Report 159 December 1998 Available on the web at http gatekeeper dec com pub DEC SRC research reports abstracts sre rr 159 html Cited in the acknowledgments FJLxx Cormac Flanagan Rajeev Joshi and K Rustan M Leino Annotation inference for modular checkers to appear in Information Processing Letters Cited in sections 5 0 and C 1 2 FL00 Cormac Flanagan and K Rustan M Leino Houdini an annotation assistant for ESC Java Compaq SRC Technical Note 2000 003 September 2000 Available on the w
144. structed may be named by an inflected form of the identifier Res For example in the objStack example from section 3 2 17 we wrote Without the set pragma ESC Java will generate a warning that the constructor fails to establish the invariant a owner this The warning might be something like ObjStack java 12 Warning Possible violation of object invariant Invariant Associated declaration is ObjStack java line 7 col 6 invariant a owner this a Possibly relevant items from the counterexample context brokenObj lt 1 gt RES 9 13 brokenObj refers to the object for which the invariant is broken Here the equality brokenObj lt 1 gt RES 9 13 indicates that the object whose invariant may be violated is the object being constructed 4 9 LoopInv warning A LoopInv warning warns that some loop invariant may not hold at the start of an iteration of a loop including an iteration in which the The pragma is associated with the loop_invariant pragma that gives the potentially violated loop invariant For more details of ESC Java s treatment of loop invariants see sections 2 4 3 and C 0 1 4 10 NegSize warning A NegSize warning warns of a possible attempt to allocate an array of negative length This condition would result in a Negat iveArraySizeExcept ion being thrown at run time JLS 15 9 4 11 NonNull warning A NonNull warning warns of a possible attempt to assign the value n
145. sult Within a normal postcondition or a modification target of a non void method the special identifier result is a specification expression whose type is the return type of the method It denotes the value returned by the method result is allowed only within an ensures also_ensures modifies Or also_modifies pragma that modifies the declaration of a non void method Fine points Note that although result may occur within a modifies pragma it is not itself a specification designator see section 2 3 1 Thus modifies result is never a legal pragma However pragmas such as for example modifies result f or modifies result i may be legal depending on the type of result 3 2 15 old In a postcondition an expression of the form old z where is a specification expression is a specification expression of the same type as It denotes the same thing as except that 1 any occurrences in x of a target field see section 2 3 1 0 of the routine is interpreted according to the pre state value of the field and 2 if any modification target of the routine has the form x i or x then all array accesses within are interpreted according to the pre state contents of arrays An expression of the form old z may occur only in an ensures exsures also_ensures OF also_exsures pragma The argument may not itself include any uses of old or fresh Fine points In a normal postcondition of a non void method the s
146. sures pragma modifies a constructor since we take the view that the object being constructed should be discarded This view is potentially unsound see section C 0 8 A single routine declaration may be modified with any number of exsures pragmas ESC Java checks that the body obeys each exsures pragma and assumes that calls obey each exsures pragma For example if a routine is modified by the pragmas exsures T1 t El exsures T2 t E2 where T2 is a subtype of T1 then ESC Java checks if checking the body of the routine or assumes if checking a caller that 1 holds whenever the routine completes abruptly by throwing an exception that is an instance of T1 and that both 1 and 2 hold whenever the routine completes abruptly by throwing an exception that is an instance of T2 A method declaration that overrides another method declaration cannot be modified with an exsures pragma but inherits the exceptional postconditions of the overridden method See also the also_exsures pragma described in section 2 3 6 2 3 5 also_ensures pragma An also_ensures pragma is a routine modifier pragma It has the form also_ensures E opt where is a boolean specification expression An also_ensures pragma has the same semantics as an ensures pragma but may appear as a modifier only of a method declaration that overrides another method declaration while overriding method declarations are forbidden to have ensures pragmas 2 3 6 also_exsures
147. t giving a LoopInv warning if B break In either case code following the loop is checked only for execution paths in which the sequences described above terminate by a break out of the loop including the implicit i B break the throwing of an exception or the execution of a return statement ESC Java will not consider code following the loop for execution paths that fall through to the end of the unrollings for example by executing the final if B break in the unrolling for loop 1 5 when s evaluates to true The default behavior of ESC Java is the same as that given by loop 1 5 Larger values of the parameter make ESC Java s checking more nearly sound but not perfectly sound Larger values of the parameter can result in significantly slower checking and increased memory usage especially when checking routines that include large loops bodies and or nested loops Loops that manifestly require many iterations to terminate normally pose a particular difficulty Suppose for example that the program being checked contains a fragment of the form 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 79 of 86 for int i 0 i lt 1000 i Si S2 where si never exits abruptly Then the ESC Java will never consider executions that reach s2 unless it is run with a loop option with an argument greater than 1000 which would almost certainly result in impra
148. tablish such locking assertions can be established explicitly for example by a requires pragma as in requires f null amp amp lockset f void m a Beets read access produces no Race warning Also a synchronized routine body and a synchronized statement always begin by adding a lock to the lock set class C monitored T t synchronized void m T x t no race because starting a synchronized method establishes lockset this void n synchronized this 46 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 47 of 86 Tx t no race The preceding examples deal only with race detection We now turn to the issue of deadlock detection ESC Java supports a synchronization discipline in which deadlocks are avoided by imposing a partial ordering on locks and acquiring locks only in increasing order The arithmetic ordering relations lt and lt are overloaded to compare objects in the locking order The special function max yields the maximum lock in a lock set Without some help in the form of user supplied pragmas it is never possible for ESC Java to prove the absence of deadlock in a program that ever acquires a lock Deadlock checking is therefore disabled by default When deadlock checking is enabled by use of the command line option warn Deadlock ESC Java checks synchronized statements and synchronized metho
149. the program text Users can control the amount and kinds of checking that ESC Java performs by annotating their program with specially formatted comments called pragmas This manual starts by providing an overview of ESC Java through an illustrative example of its use and a summary of its features and then goes on to document all the pragmas supported by ESC Java and all the kinds of warnings that it generates It also provides basic information about running ESC Java This manual documents Version 1 2 2 of ESC Java built on October 12 2000 We sometimes speak of the current ESC Java rather than just ESC Java to emphasize that particular features bugs or limitations under discussion are artifacts of the Version 1 2 2 implementation and may be subject to change in future versions Of course there is no guarantee that all such aspects of ESC Java will in fact change nor that other aspects will remain unchanged as the tool evolves This manual is designed to serve both as an introduction to ESC Java and as a reference manual First time readers may prefer to skip the portions marked Fine point s as well as some other parts that we have indicated On the other hand the extended example in section 0 should be particularly helpful to first time readers For a much abridged treatment of the information in this manual see the ESC Java Quick Reference SLS00 The Quick Reference lists most of the specification language features describe
150. tion There are many situations in which labels are ambiguous For example suppose file D java contains the code class D int a b invariant lblpos foo a gt 0 amp b gt 0 lblpos bar a lt 0 amp b lt 0 requires x null amp amp y null D D x D y a X a b y b Then the command escjava D java yields the warning 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes D java 10 Warning Possible violation of object invariant Invariant a Counterexample labels bar foo There is no way to tell from this message whether ESC Java is warning about the case where a has nonnegative x and y fields and b has negative x and y fields or about the case where a s fields are negative and b s are nonnegative However for this particular example the counterexample switch described in appendix A would resolve the ambiguity 3 2 17 owner The standard spec file see section 5 1 2 for the class java lang Object gives every object o a ghost field 0 owner of type Object ESC Java input from file java lang Object spec ghost Object owner The intended use of this field is for situations is which the programmer wishes to specify that some field f is unshared For example if a class T with an instance field declares the instance invariant ESC Java input from file T java invariant
151. tion of R If ESC Java cautioned the user against unenforceable object invariants of the sort mentioned in the fine points of section 2 4 1 the situation would be partially but not entirely ameliorated Conversely ESC Java might consider some invariant to be irrelevant to R but relevant to a caller In this case ESC Java will not check that the body of R preserves the invariant but will nonetheless assume while checking the caller that the invariant is preserved by the call C 0 3 Modification targets When reasoning about a call to a routine ESC Java assumes that the routine modifies only its specified modification targets as given in modifies and or also_modifies pragmas modifying the routine and any routines it overrides But when checking the implementation of a method the current ESC Java doesn t check that the implementation modifies only the specified targets Thus modifies and also_modifies pragmas are purely a way of describing the programmer s intent in the form that the checker can use as an assumption C 0 4 The also_modifies and also_requires pragmas The also_modifies and also_requires pragma are unsound because they allow an overriding method to have a weaker specification than the method it overrides Suppose that a method u m overrides a method T m and suppose that some method r contains a call of the form m where z has static type T but might evaluate at run time to a value of type u While checking the code c
152. together would imply not only forall ObjStack x y x y gt x a y a and 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 60 of 86 forall Foo x y x y gt x a y b but also forall ObjStack x forall Foo y Object x y gt x a y b If for example ESC Java were checking code that modified a component of the b field of some Foo foo and if that code occurred in a scope where the invariant on line 6 of ObjStack java were considered heuristically relevant see the fine points in section 2 4 1 then ESC Java would need this last consequence in order to eliminate from consideration scenarios in which the invariant on line 6 might become violated for some 0bjStack brokenObj with brokenObj a foo b See LS99 for a different approach to specifying that certain fields are unshared 3 3 Scoping name resolution and access control in specification expressions The rules for scoping accessibility and resolution of names in specification expressions differ in several ways from those for Java expressions We have described most of these differences elsewhere in this manual but repeat them here to have them collected in one place Applications of the ESC Java operators typeof elemtype max nonnullelements fresh and old are parsed like method invocations with the operator taking the role of the method name Of course applicatio
153. ts to old Future versions of ESC Java may liberalize this restriction with quantifications on reference types inside old ranging over objects allocated in the pre state 3 2 11 exists An expression of the form exists T v E where ris a specification type see section 3 0 vis a nonempty comma separated list of identifiers called bound variables and is a specification expression of type boolean is a specification expression of type boolean It denotes that is true for some substitution of values of type T for the bound variables If Tis a reference type the quantification ranges only over allocated objects that are instances of T Fine points See section 3 2 10 for restrictions on bound variable names and restrictions on places where quantified formulas may appear 3 2 12 nonnullelements An expression of the form nonnullelements A where A is a specification expression of an array type is a specification expression of type boolean It is equivalent to A null amp amp forall int i 0 lt i amp i lt A length gt A i null Expressions of the form above came up fairly frequently in our early experiments with ESC Java and we found writing them sufficiently tedious to justify the introduction of a special notation Example Consider the main method of a program static public void main String args The usual way for main to be invoked is with the value of args derived from the command
154. ttp gatekeeper research compaq com pub DEC SRC technical notes Example Suppose file c java contains the following code class C requires lblpos fee i lt 5 lblpos fie i gt 10 ensures lblneg foe result 5 amp amp lblneg fum result gt 0 int m int i return itl Then output from the command escjava C java includes the following warning C java 7 Warning Postcondition possibly not established Post Associated declaration is C java line 4 col 6 ensures lblneg foe result 5 amp amp lblneg fum result gt 0 Execution trace information Executed return in C java line 6 col 6 Counterexample labels fum fee The label fee comes from the positively labeled expression lblpos fee i lt 5 inthe requires pragma for method m and tells us that in the execution path associated with the warning m is called with an argument i such that i lt 5 true The label fum comes from the negatively labeled expression lblneg fum result gt 0 in the ensures pragma for m and tells us that in the execution path associated with the warning m returns a result result such that result gt 0 false Fine points Expression labels are in their own name space so they never conflict with or hide any other kinds of identifiers Labeled expressions are allowed only in those places where quantified expressions are allowed see section 3 2 10 Limita
155. u11 to a variable whose declaration is modified by a non_nu11 pragma or to call a routine with an actual parameter value of nu11 when the declaration of the corresponding formal parameter is modified by or inherits a non_null pragma The warning is associated with the non_null pragma that is potentially violated Tips If the right hand side of the assignment indeed never evaluates to null you must somehow communicate the reason to ESC Java For some ideas about this see the tips given in connection with Null warnings in section 4 13 Alternatively it may be that the non_null pragma associated with the warning is too strong and should be replaced by an annotation that only requires the affected field or variable to be non null under certain conditions See also the comments in section 2 4 0 about non_null VS invariant and requires pragmas 4 12 NonNullinit warning A NonNulliInit warning warns that a constructor may fail to establish a non null value for an instance field of the constructed object when the declaration of that instance field is modified by a non_null pragma The warning is associated with the non_nu11 pragma that is potentially violated 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 69 of 86 4 13 Null warning A Null warning warns of a possible attempt to dereference nu11 for example by field access o f an array access O i a method call 0 m
156. ual http gatekeeper research compaq com pub DEC SRC technical notes 67 of 86 lt esc gt public static int add int a int b With this last specification ESC Java will consider execution paths in which a call to add terminates exceptionally but only if it cannot verify the arguments are non null and of equal length 4 6 IndexNegative warning An IndexNegat ive warning warns that control may reach an array access At 7 when the value of the index ris negative This condition would result in an IndexOutOfBoundsException being thrown at run time JLS 11 5 1 1 15 12 1 4 7 IndexTooBig warning An IndexTooBig warning warns that control may reach an array access A I when I gt A length This condition would result in an IndexOut OfBoundsExcept ion being thrown at run time JLS 11 5 1 1 15 12 1 4 8 Invariant warning An Invariant warning warns that some object invariant may not hold when control reaches a routine call or that some object invariant may not hold on exit from the current body The warning is associated with the invariant pragma that gives the potentially violated object invariant Tip An invariant warning is normally accompanied by a partial counterexample context describing conditions under which so far as ESC Java can determine the indicated invariant might be violated for example Possibly relevant items from the counterexample context typeof brokenObj lt 3 gt type
157. ued to complain of a possible array bounds error even after we fixed the bug in the surrounding for loop ESC Java input from file Bag java 16 for int i 0 i lt n i 17 if a i lt m ESC Java output Bag java 17 Warning Possible array index too large IndexTooBig if a i lt m A 1 warning If we found this behavior puzzling we might consider the experiment of adding an assert pragma between lines 16 and 17 The outcome of the experiment would depend on which of the two obvious assertions we chose assert i lt n or assert i lt a length 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 25 of 86 In either case observing the outcome might take us a step closer to understanding the situation Note Some earlier versions of ESC Java had a bug that sometimes resulted in highly counterintuitive failure to warn of the first potential error on an execution path For example if a program contained the lines 23 assert x lt 10 amp y lt 10 eee 3 statements not modifying x 33 assert x lt 10 then ESC Java might have produced an Assert warning for line 33 but not for line 23 even though the assertion at line 33 could be false after execution of lines 24 32 only if the assertion at lines 23 had been false beforehand and even though ESC Java would have warned about line 23 if the assertion in line
158. un time JLS 5 4 15 15 Tip cast warnings often arise in connection with the use container classes when the programmer intends a particular container to be used exclusively to hold elements of some particular type T a proper subtype of object but the methods for extracting elements are declared to return results of type object The second example in section 2 6 2 shows how the programmer can use a ghost variable to express the design decision that the container will hold only instances of T so that objects extracted from the container can always safely be cast to type T 4 4 Deadlock warning A Deadlock warning warns that control may reach a synchronized statement or a call to a synchronized method that would acquire a lock in violation of the locking order That is it warns of the possibility that a thread might attempt to acquire a lock z when lockset ZL max lockset lt L is false In the current ESC Java Deadlock warnings are disabled by default but can be enabled by use of the command line option warn Deadlock The only way that ESC Java can ever show that the execution of a synchronized statement or a synchronized method body will not result in a potential locking order violation and thus in a potential deadlock is by using information supplied in pragmas The usual way to supply the necessary information is to use an axiom pragma to supply information about the locking order and to use a requires pragma to s
159. upply information about the locks held on entry to any routine whose body includes a synchronized Statement or a call to a synchronized method A Deadlock warning has no associated pragma Typically the warning results from the absence of some pragma that would supply the information needed to show that the locking order is obeyed While a user might sometimes blame a Deadlock warning on a bug in some specific pragma there is no general mathematical rule for uniquely ascribing such blame 4 5 Exception warning An Exception warning warns that a routine may terminate abruptly by throwing an exception that is not an instance of any type listed in the routine s throws clause Note that ESC Java s treatment of unchecked exception classes JLS 11 1 is different from Java s Java s compile time checking never requires a throws clause to mention an unchecked exception class By contrast when ESC Java checks the body of a routine R it considers the possibility of exceptions being 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes thrown by any throw statement in the body of R and by any call from R to a routine with a nonempty throws clause and it issues a warning if so far as it can determine it is possible that R may terminate abruptly with such an exception other than an instance of a type mentioned in R s throws clause However ESC Java does not consider the possibility o
160. va automatically supplies the postcondition fresh this for every constructor 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 2 3 3 A note on the interaction of modifies and old This section may be skipped on first reading The current ESC Java does not check that the body of a routine actually obeys the constraint expressed by the routine s modifies pragmas This lack of checking is one of several potential sources of missed warnings unsoundness The potential for missed warnings is mitigated somewhat by a fact that may have seemed surprising when we mentioned it in the previous section 2 3 2 If a particular field either a static field or an instance variable is not specified as a target field section 2 3 1 0 of a routine then occurrences of that field within arguments to o1d in the routine s postconditions are taken to refer to post state values Consider for example a class with an integer field and a method inc declared as follows with no modifies pragma ensures f old f 1 void incf this f Since f is not specified as a modification target of incf ESC Java will interpret both occurrences of in the ensures pragma as referring to the post state value of this Consequently ESC Java will be unable to show that the method establishes the specified postcondition and will issue a warning to that effect While thi
161. warning message indicates the specific requires pragma giving rise to the warning and warnings arising from each pragma can be suppressed individually 2 3 1 modifies pragma A modifies pragma is a routine modifier pragma It has the form 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 27 of 86 modifies L i opt where Z is a nonempty comma separated list of specification designators A specification designator designates a mutable component of the state It is very much like a Java LeftHandSide JLS 19 12 but generalized as described below The pragma specifies that the routine is allowed but not required to modify any of the state components listed in Z The state components named in modifies pragmas of a routine are called modification targets of the routine When checking code that calls a routine ESC Java assumes that the call modifies only the routine s modification targets with the usual substitutions and possibly also any freshly allocated state regardless of whether the call terminates normally or abruptly However the current ESC Java does not enforce modifies pragmas when checking a routine s implementation Fine points Permissible forms of specification designators are e a simple name n The name must denote a non final field possibly a ghost field see section 2 6 0 This form allows modification of this n if the routine is an instance met
162. warnings Also while it is sometimes possible to eliminate spurious warnings by means that don t carry the same risks of missed warnings some judgment must be exercised as to whether the improved assurance of correctness will be worth the increased effort in any particular case 2 2 1 Most ESC Java pragmas are just fancy forms of assert and assume The ESC Java annotation language includes over twenty different kinds of pragmas but to a first approximation they are mainly more or less elaborate ways of adding assertions i e claims about the program state that are checked by the ESC Java and or assumptions 1 e claims that are taken for granted by ESC Java at different points in the program Indeed one can also think of the checking that ESC Java 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 23 of 86 does in the absence of any user annotations as simply checking implicit assertions before each pointer dereference array access etc so that for example the program fragment x ali is treated as if it were assert a null assert 0 lt i assert i lt a length x a i There are several valuable differences between the explicit introduction of assertions through the use of assert pragmas and their implicit introduction through other ESC Java pragmas and through built in checking rules e Warnings arising from assert pragmas all produce the sa
163. ways supposed to be non null To do this we annotate the declaration of a with a non_null pragma class Bag non_null int a This causes ESC Java to assume that the a field of any Bag object is itself non null and thus can safely be dereferenced Conversely it causes ESC Java to issue a warning for any assignment to the a field of a Bag If it cannot confirm that the expression being assigned will have a non null value at run time Furthermore ESC Java will check that every Bag constructor initializes the a field of the constructed object to a non null value 0 4 Scene 4 We correct a bug in Bag extractMin We now consider the third warning Bag java 15 Warning Array index possibly too large IndexTooBig if a i lt m A Examining the program we now find a genuine bug The for loop starting on line 15 in the original program examines array elements a 1 through a n but array indexing in Java is zero based We correct the line to read for int a2 07 a lt my att 4 0 5 Scene 5 We take no action for a redundant warning The fourth warning Bag java 21 Warning Possible null dereference Null a mindex a n requires no action as the non_null pragma we added in section 0 3 already prevents a from being null In other words the second and fourth warnings complain about the same problem Remark ESC Java often avoids issuing such redundant warnings Note for example that it doesn t compl
164. xical pragmas at any point where Java allows a comment we henceforth take the liberty to eschew this degree of pedantry The current ESC Java includes only one kind of lexical pragma nowarn pragma section 2 1 0 Declaration pragmas such as for example the invariant pragma in section 0 8 in our introductory example are analogous to Java declarations and may occur only where declarations of class members or interface members may occur The current ESC Java includes the following kinds of declaration pragmas invariant pragma section 2 4 1 axiom pragma 2 4 2 ghost pragma 2 6 0 Statement pragmas are analogous to Java statements They may occur only where Java statements nay occur The current ESC Java includes the following statement pragmas assert pragma 211 1 1 O assume pragma 2 1 2 unreachable pragma 2 1 3 9 loop_invariant pragma 2 4 3 set pragma 2 6 1 Modifier pragmas are analogous to Java modifiers such as private and final Generally modifier pragmas are allowed in the same positions as Java modifiers but they are also allowed in a few other places as described in the fine points below Some modifier pragmas for example the non_null pragma in section 0 3 in the introductory example modify variable declarations other modifier pragmas for example the requires pragmas in sections 0 2 and 0 6 in the introductory example modify declarations of routines methods or constructors Th
165. y in section 4 0 but will not discuss them further in the course of this introductory example 0 2 Scene 2 We write a requires precondition pragma for the Bag constructor ESC Java s first warning is that the attempt on line 6 to access input length might fail because input might be nu11 We now must decide what to do about this warning One approach would be to decide that the implementation of the constructor is incorrect Following this approach we would modify the constructor to test for a null argument and for example construct an empty multiset Bag int input if input null n 0 a new int 0 else n input length a new int n System arraycopy input 0 a 0 n This would indeed eliminate the first warning Instead however we will continue our example by illustrating a second approach in which we decide that the implementation of the constructor is correct but that we do not intend for the constructor ever to be called with a null argument We inform ESC Java of this decision by adding an annotation to the constructor declaration requires input null Bag int input n input length When the character is the first character after the initial or of a Java comment as in the first line of the program fragment above ESC Java expects the body of the comment to consist of a sequence of ESC Java annotations known as pragmas The requires pragma above specifies a precon
166. y of reasons including but not limited to the following e The annotations in the spec files were added mostly in reaction to specific situations encountered by members of the ESC Java team in our use of ESC Java rather than as part of any systematic effort to specify any set of routines completely or even as completely as practical given the limitations of the ESC Java annotation language e There may be version skew between the spec files you download and the JDK files in use at your site e The spec files may have intentional semantic differences from the corresponding JDK files for methodological reasons see for example the discussion of unchecked exceptions in section 4 5 81 of 86 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 82 of 86 e The spec files the JDK files or both may simply contain errors See also the disclaimers near the beginning of this manual C 0 11 Shared variables ESC Java depends on programmers to supply monitored and monitored_by pragmas telling which locks protect which shared variables In the absence of such annotations ESC Java will not produce a warning when a routine might access a variable without holding the appropriate lock Even when the user does specify which locks protect which variables there is another potential source of unsoundness ESC Java assumes that the value of a shared variable stays unchanged if a
167. ystem arraycopy input 0 a 0 n 0 1 2 requires n gt 1 2 int extractMin 3 int m Integer MAX_VALUE 4 int mindex 0 5 for int i 0 i lt n itt 6 if a i lt m 7 mindex i 8 m ali 9 20 21 n 22 a mindex a n 23 return m 24 25 We now run ESC Java again and it produces the following warning Bag java 17 Warning Array index possibly too large IndexTooBig if a i lt m A 08 02 2005 17 56 ESCJ 27 ESC Java User s Manual http gatekeeper research compaq com pub DEC SRC technical notes 12 of 86 0 8 Scene 8 We supply an invariant pragma relating n to a lenght It may appear that ESC Java is still complaining about the bug we thought we d fixed in section 0 4 but further study reveals a different problem ESC Java has no reason to expect that n which we intend to be the length of the meaningful prefix of a will in fact be at most a length We can express this intention with an invariant pragma 1 class Bag 2 non_null int a 3 int n 4 invariant 0 lt n amp n lt a lenght Roughly speaking ESC Java treats an invariant as an implicit postcondition of every constructor and as both a precondition and postcondition of every method The semantics of invariant pragmas and all other ESC Java pragmas are described in greater detail in section 2 below The full rules about expressions that can occur in pragmas

(ESCJ 27:\240 ESC/Java User`s Manual)

Contents

Download Pdf Manuals

Related Search

Related Contents