ESC/Java Quick Reference
Contents
1. can be applied only to fields The modified field is a shared variable monitored by the locks 4of7 in SL which is a nonempty comma separated list of specification expressions ESC Java checks that the field is never read except by a thread holding at least one non null lock in s1 and that the field is never written except by a thread holding all non null locks in si of which there must be at least one monitored modifier synchronization This pragma may modify only an instance variable declaration and is the same as monitored_by this 3 The ESC Java specification expressions A specification type is either a Java type or one of the special types TYPE or LockSet or an array of special types for example TYPE The specification type LockSet cannot be mentioned explicitly in annotations Specification expressions must be free of subexpressions that may potentially have side effects so they may not contain any assignment etc pre post increment decrement or array or object creation new or method invocation even for methods that have no side effects The additional constructs that are allowed in specification expressions beyond those allowed in Java expressions are e type T TYPE denotes the specification type T e typeof E TYPE denotes the dynamic type of the value of specification expression where E is of a reference type elemtype E TYPE d2. SRC Technical Note 2000 004 October 12 2000 ESC Java Quick Reference Silvija Seres June 1999 Revised by K Rustan M Leino and James B Saxe October 2000 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 Any other trademarks or registered trademarks mentioned herein are the property
3. a will check that holds at the start of each iteration of the loop spec_public modifier variable referencing This pragma may modify only non public field declarations and it will cause the fields in the declaration to be as accessible in pragmas as they would have been if the declaration had been public readable_if E modifier variable referencing This pragma may modify only the declaration of a field or a local variable denotes a boolean specification expression that has to be true at any read access of the fields or variable uninitialized modifier variable referencing This pragma may modify only a local variable declaration that has an initializer ESC Java will check that no execution path accesses the variable without first performing an assignment other than the initializer to the variable ghost M S v declaration ghost variables s is a Specification type v is an identifier and m is a sequence of modifiers including public this pragma is like an ordinary Java variable declaration m s v except that it makes the declaration visible only to ESCV Java and not to the compiler such variables are called ghost variables set D E statement ghost variables D refers to a ghost field of some object or class and Eis a specification expression containing no quantifiers or labels this pragma has the analagous meaning to the Java assignment statement D E monitored by SL modifier synchronization This pragma
4. access A I when A length lt I Invariant warns that some object invariant may not hold when control reaches a routine call or that 6 of 7 some object invariant may not hold on exit from the current body LoopInv warns that some loop invariant may not hold when it is supposed to OwnerNul1 warns that a constructor may violate the implicit postcondition this owner null NegSize warns of a possible attempt to allocate an array of negative length NonNull warns of a possible attempt to assign the value null to a variable whose declaration is modified by a non_nu11 pragma or to call a routine with an actual parameter value of null when the declaration of the corresponding formal parameter is modified by or inherits a non_null pragma NonNullInit 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_nu11 pragma Null warns of a possible attempt to dereference null for example by field access o an array access O i amethod call o m asynchronized statement synchronized O ora throw statement throw O where o evaluates to null Post 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 Pre warns that control may reach a routine call when so
5. ce array type e fresh E boolean used in postconditions denotes that is non null and was not allocated in the pre state of the routine call where is a specification expression of a reference type e result is a specification expression whose type is the return type of the non void method in whose normal postcondition or modification target it appears denoting the value returned by the method old E is a specification expression of the same type as the specification expression E and is used in a postcondition to denote the same thing as except that 1 any occurrence in of a target field 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 E owner Object is a specification expression of type object denoting the owner of object E The standard specification library shipped with ESC Java declares owner as a ghost field of java lang Object The pragma invariant f owner this in the declaration of a type T is the conventional way to specify that the objects of type T do not share their fields All constructors have the implicit postcondition this owner null 4 The ESC Java modification targets or specification designators a simple name denoting a non final field afield acc
6. enotes the specification type T if denotes an array type T unspecified otherwise e S lt T boolean denotes that s is a subtype of T where s and T are specification expressions of type TYPE e lockset LockSet denotes the set of locks held by the current thread e S L boolean denotes that L is a member of s where s is a specification expression of type LockSet and L isa specification expression of a reference type E lt F boolean denotes that object precedes object F in the locking order E lt F boolean denotes that object precedes object F in the locking order or E F e max S Object denotes the maximum element of s in the locking order where s is a specification expression of type LockSet E gt F boolean denotes the condition that implies F where and F are specification expression of type boolean e forall T V E boolean denotes that is true for all substitutions of values of type T for the bound variables v where T is a specification type v is a nonempty comma separated list of identifiers and is a specification expression of type boolean e exists T V E boolean denotes that is true for some substitution of values of type T for the bound variables v where T and v are as above e nonnullelements A boolean 5of7 denotes that a and all its elements are non null where a is a specification expression of a referen
7. erations null pointer dereferencing deadlocks and race conditions of threads Given a Java program it automatically infers and checks a set of verification conditions that correspond to the described classes of errors It also allows the programmer to record design decisions and to influence the choice of verification conditions by annotating the program with a set of pragmas These can be used to specify the pre and postconditions of routines properties of abstract data types invariants of loops and much more The errors that ESC Java looks for are chosen on a pragmatic basis they are the errors that according to the engineering experience occur often and are relatively cheap to find but the ESC Java system is flexible and can be extended to allow for checking of other types of errors Currently ESC Java checks almost the entire Java 1 2 language including all of Java 1 0 In terms of program verification ESC Java is unsound because it can miss real programming errors from the targeted class and it is incomplete because it can give some spurious warnings Some degree of inaccuracy is inevitable in a tool such as ESC Java due to theoretical limits of decidability Additionally the design of ESC Java intentionally sacrifices some accuracy in trade for efficiency of the tool The user has some control over ESC Java s unsoundness and incompleteness thanks to pragmas These pragmas not only enable modular program checking but are also a co
8. ess o where o is a specification expression of a reference type T and denotes one of the fields possibly a ghost field of T e an array access of the form a I where a is a specification expression of an array type and I is a specification expression of an integral type other than Long or e an array range of the form a where a is a specification expression of an array type 5 The ESC Java warning types 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 ArrayStore warns that the control may reach an assignment A I E when the value of is not assignment compatible with the actual element type of A e Assert warns that control may reach a pragma assert E when the value of is false Cast warns that control may reach a cast T E when the value of cannot be cast to the type E Deadlock warns that control may reach a synchronized statement that would acquire a lock in violation of the locking order or that the a synchronized method may start by acquiring a lock in violation of the locking order Exception Warns that a routine may terminate abruptly by throwing an exception that is not an instance of any type listed explicitly in the routine s throws clause IndexNegative warns that control may reach an array access A 1 when the value of the index 1 is negative IndexTooBig warns that control may reach an array
9. ethod declaration otherwise it has the same meaning as modifies s non_nu11 modifier data invariant Modifies the declaration of a variable of a reference type where the variable may be a static field instance variable local variable or parameter ESC Java will check at each assignment to the variable that the value assigned is not null and assume at each use that the value is not null invariant E declaration data invariant E denotes a boolean specification expression that is an object invariant of the class within whose declaration the pragma occurs If does not mention this the invariant is called a static invariant and is assumed on entry to implementations checked at call sites assumed upon call returns and checked on exit from implementations If mentions this the invariant is called an instance invariant An instance invariant is assumed to hold for all objects of the class on entry to an implementation and is checked to hold for all objects of the class on exit from an implementation At a call site an instance invariant is checked only for those objects passed in the parameters of the call and in static fields A call is assumed not to falsify the instance invariant for any object axiom E declaration data invariant ESC Java assumes that is true at the start of every routine body loop_invariant E statement data invariant This pragma may appear only just before a Java for while or do statement ESC Jav
10. henever the routine terminates normally e exsures T t E modifier non overriding routine T is a subtype of java 1lang Throwable t is an optional identifier and denotes a boolean specification expression that is an exceptional postcondition of the routine the pragma modifies ESC Java will assume that holds whenever the a call to the routine completes abruptly by throwing an exception t whose type is a subtype of T and will issue a warning if it cannot prove from the routine implementation that holds whenever the routine terminates completes abruptly by throwing an exception t whose type is a subtype of T also_ensures E modifier overriding routine This pragma may modify only a method declaration that overrides another method declaration otherwise 3 0f7 it has the same meaning aS ensures E also_exsures T t E modifier overriding routine This pragma may modify only method declaration that overrides another method declaration otherwise it has the same meaning as exsures T t E also_requires E modifier overriding routine This pragma may modify only a method declaration that occurs in a class declaration overrides a method of a superinterface and does not override a method of a superclass otherwise it has the same meaning as requires E also_modifies S modifier overriding routine This pragma may modify only a method declaration that overrides another m
11. l assume that is true whenever control reaches the pragma and ignores the remainder of all execution paths in which is false e assert E statement general E denotes a boolean specification expression ESC Java will issue a warning if it cannot establish that is true whenever control reaches the pragma unreachable statement general semantically equivalent to assert false e requires E modifier non overriding routine E denotes a boolean specification expression that is a precondition of the routine the pragma modifies ESC Java will assume that holds initially when checking the implementation of the routine and will issue a warning if it cannot establish that holds at a call site modifies S modifier non overriding routine s denotes a nonempty comma separated list of modification targets ESC Java will assume that calls to the routine modify only the modification targets in s and freshly allocated state components but will not check the routine implementation correspondingly that is ESC Java does not warn about implementations that modify more targets than s allows e ensures E modifier non overriding routine E denotes a boolean specification expression that is a normal i e non exceptional postcondition of the routine the pragma modifies ESC Java will assume that holds just after each call site the routine and will issue a warning if it cannot prove from the routine implementation that holds w
12. me precondition of the routine does not hold Race warns of a possible attempt to access a monitored field while not holding the requisite lock s Reachable warns that control may reach an unreachable pragma Uninit 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 Unreadable warns that control may reach a read access of a field or variable x when the expression in a readable_if pragma modifying x s declaration is false ZeroDiv warns of a possible attempt to apply the integer division or remainder operator with zero as the divisor Tof7
13. nvenient formalism for recording programmers design decisions and program specifications The remainder of this page gives a rough description of the kinds of pragmas available in the current ESC Java the specification expressions that can occur in those pragmas and the kinds of warnings ESC Java reports 1 There are four syntactic categories of ESC Java pragmas 2 0f7 A pragma annotation is enlosed in a Java comment whose first character is an e For example non_null is an ESC Java pragma e lexical pragmas may occur in the same places as Java comments e statement pragmas may occur in the same places as Java statements e declaration pragmas may occur in the same places as Java declarations of class and interface members e modifier pragmas may occur in certain places within Java declarations of variables or routines All pragmas enclosed in a single Java comment must be of the same syntactic category 2 The list of ESC Java pragmas with their syntactic semantic contexts For pragmas terminated by semicolon the semicolon is optional if there are no further pragmas enclosed in the same comment nowarn L lexical general L denotes a possibly empty comma separated list of warning types ESC Java will suppress any warning messages of the types in L or of all types if L is empty at the line where the pragma appears e assume E statement general E denotes a boolean specification expression ESC Java wil
14. of their respective holders lof7 Abstract This document is intended to be a non detailed trimmed down version of the ESC Java User s Manual for people who would like to get an overview of the annotation language supported by the Compaq Extended Static Checker for Java ESC Java without getting immersed in all its technical intricacies For more detailed information please refer to the ESC Java User s Manual For information about the invocation of the ESC Java checker please see the escjava 1 man page included with the ESC JJava download available from http research compag com SRC esc 0 What does ESC Java do anyway Type annotation and static type checking of programs have proved to be one of biggest engineering successes of computer science Typing provides a coarse semantics for programs since it pays no attention to the semantics of any language constructs that are not related to types Nevertheless the automatic type checking of programs weeds out already at compile time many of the most common programming errors thus making them less costly for the developers Also typing forces a certain discipline upon the programmer which results in better programs The Compaq Extended Static Checker for Java ESC Java pushes the idea behind type checkers a few steps further The class of errors that it looks for is much larger and more varied it addresses among others the potential run time errors that arise from illegal array op
Download Pdf Manuals
Related Search