Home

Escjava2-Implementat..

1. ssse eiiis 68 6 4 4 non null on formal parameters and results of routines 68 6 4 5 monitored by ssssuusessselees nas 68 6 4 6 readable_if 0 ccc ene tenet tne ennes 68 GAT anally told Style sanidad e icon Ie opiate dtd 68 6 4 8 semicolon termination 00 eee e cece ee eee ee 68 6 4 9 Routine bodies in spec files lisse eese lessen 68 6 5 Non JML features in ESC Java2 ooooooooomommom o 69 6 5 1 annotation comments beginning with Q or 69 6 5 2 order of clauseS 0 0 00 c cece cece eene 69 6 5 3 splitting of annotations 0 00 cece ce eee eee 69 6 5 4 help r annotations 2 02 4 c Rr Rep eee RRI BE eee RR 69 6 5 5 typeof applied to primitive typesS o ooooooooo 69 6 5 6 unreachable sises cons eR ERR SR pep 69 6 5 not modified sss si serbe cedet et ER doa nd e ea 69 6 5 8 specifications of default constructor luus 69 6 5 9 loop_predicate 0 0 cece cece eee eee 69 6 5 10 skolem constant 00 enian a eee nen 69 6 5 11 still deferred 0ooooooooorrcorrrr ellen 69 6 5 12 writable deferred 0 0 eee eee eee eee 70 0 5 139 3Vritable if uc Thea db ed eae oa A 70 6 5 14 readable orita ls rettet aee oet s o 70 6 5 15 monitored_by 0 0 ameda eee eee eens 70 0 9 10 SUE D Sa A ech lacs Sikes nated Sener ea eae oe oe eee 70 ODIT ummritialized uscire se ad 70 6 5 18 placement of annotation
2. 000 ee cece ee esee 3 16 6 not_specified 0 cece eee eee eee ee eens 9 16 7 private datas t 2d etu creer ida cin 0 10 8 NOHE ua cete see en eere nc vol n oe C Rata Bua 3 16 9 Other Java operators and expression syntax 3 17 store ref expressions 00 0 cece eee eee 3 17 1 ident super this ident this sisas alt ident super thi8 Baron nue ex 3 17 3 ident super this expr eee 3 17 4 ident super this expr expr2 22s 3 17 5 ident super thie Pico dd Ner NEC o n is AR AAA RAGE OM ADOLAM a sesso uae end peed ed edad Ded Pu ren bdo UNS Neverythine sii ae e E ed oce pog CUR Roe paie tas 3 18 Statements within model programs eslueeesss 3 19 Other 18SUe8 24e ea redeo da is aio Pa ads 3 19 1 universe type system esseseeeeeee een 3 19 2 infinite precision arithmetic s liiis esee 3 19 3 nowarn annotation rror irsini iri is rea EErEE 3 19 4 Java and JML assert statements s esses sess 3 19 5 Methods and constructors without bodies in Java files 3 19 6 Methods and constructors in annotation expressions 3 19 7 Original ESC Java also specifications 3 19 8 anonymous classes sisse 3 19 9 block level class declarations esee eese 3 19 10 field method and constructor keywords ii 3 19 11 Equivalence of NTYPE and java lang Class 48 3 19 12 exceptions in anno
3. Status Fully implemented Differences from JML or Java None 3 10 6 synchronized Java methods only Description This modifier indicates that processing must wait until a monitor lock is available and must obtain that lock before the execution of the method is begun the lock is released when the method execution is completed Each object has implicitly a monitor lock associated with the object Before executing an instance method it is the lock associated with receiver object that is obtained before executing a static method it is the lock associated with the class object T class for type T that is obtained Are the preconditions postconditions evaluated before or after obtaining and releasing the locks Status Implemented Differences from JML or Java None Chapter 3 Status of JML features 32 3 10 7 native Java methods only e Description A native method is one whose implementation is provided outside of the Java language Consequently such a method will not have an implementation e Status Fully implemented The static checker will indicate that the method passes its checks since there is no body to check e Differences from JML or Java None 3 10 8 strictfp Java methods only e Description This modifier indicates that all of the floating point operations within the method must hold to strict semantics e Status Parsed and ignored by ESC Java2 No static checking of floating point seman t
4. ensures Q1 public void m public class D extends Super also requires P3 requires PP3 ensures Q3 public void m ESC Java would combine the interface and subclass specifications as follows requires P1 requires P3 requires PP3 0 ensures Q1 ensures Q3 This does not satisfy behavior inheritance The desugaring provided by ESC Java2 is correct 0 requires P1 P3 amp amp PP3 ensures P1 gt Q1 0 ensures P3 amp amp PP3 gt Q3 Here is a larger example public class Super requires P1 Q ensures Q1 also requires P2 ensures Q2 public void m public class D extends Super 1 also requires P3 requires PP3 ensures Q3 also requires P4 ensures Q4 public void m The specifications in Super desugar in ESC Java2 to Chapter 3 Status of JML features 51 0 requires P1 P2 0 ensures P1 gt Q1 0 ensures P2 gt Q2 The specifications in D desugar to 0 requires P3 amp amp PP3 P4 ensures P3 amp amp PP3 gt Q3 0 ensures P4 gt Q4 but they are then combined with the super class specifications to produce the composite specification requires P1 P2 P3 amp amp PP3 P4 0 ensures P1 gt Q1 0 ensures P2 gt Q2 0 ensures P3 amp amp PP3 gt Q3 0 ensures P4 gt 4 With this approach
5. A field declaration including ghost and model field declarations may have both Java and JML modifiers In addition to the access modifiers see Section 3 4 Access modifiers page 13 the following modifiers are relevant to field declarations Chapter 3 Status of JML features 33 3 12 1 non_null JML e Description This modifier on a field declaration indicates that the field in question never has a null value after the object is constructed It is equivalent to a class invariant of the form invariant field null with the same access modifiers as the field itself Note that the field is not null after construction The field may indeed be null after class innitialization and during the execution of constructors or helper methods called by constructors e Status Fully implemented and supported by the static checker e Differences from JML or Java None 3 12 2 monitored JML e Description This modifier indicates that the field modified is guarded by the monitor associated with this if the field is not static and by the monintor associated with the class object if the field is static On any write to the field all monitors guarding the field must be held by the thread executing the write on any read of the field at least one of the monitors guarding the field must be held by the thread executing the read Modifying a field x in class C with monitored is equivalent to the declaration monitored by x C class if x i
6. Describe the function of the this suffix Status Implemented within modifies clauses 3 17 2 ident super this This designates all static and instance fields of any privacy level including those inherited from superclasses and interfaces of the given object Status Not implemented 3 17 3 ident super this expr This designates an element of the given array object Describe the function of the this and super prefix Status Implemented within modifies clauses 3 17 4 ident super this expr expr2 This designates a range of elements of the given array object Status Not implemented 3 17 5 ident super this This designates all the elements of the given array object Status Not implemented Chapter 3 Status of JML features 44 3 17 6 classname This designates all static fields of any privacy level including those in superclasses and interfaces and including ghost and model fields of the given class Status Not implemented 3 17 7 nothing This designates an empty set of store refs It may be used with the modifies accessible and callable clauses If nothing appears in a sequence of other store refs it is ignored since a sequence of store refs is essentially a union Status Fully implemented 3 17 8 everything This designates a universal set the set of references to all object and class fields for every object and class allocated in the current state
7. None Chapter 3 Status of JML features 26 3 9 3 requires requires redundantly pre pre redundantly e Description A requires clause specifies a condition that must hold in the pre state of the method in the context where it is called in the program The remaining clauses of the specification case must hold whenever the requires clause or the conjunction of multiple requires clauses holds The expression in the clause may also be not_ specified which is equivalent to omitting the clause The expression must have boolean type and is evaluated in the pre state e Status The requires clause is implemented and is utilized by ESC Java2 in generating verification conditions e Differences from JML or Java None Decide discuss use of this instance variables in constructor preconditions Note any change from ESC Javal 3 9 4 ensures ensures redundantly post post redundantly e Description An ensures clause states a condition that must hold in the post state of a method or constructor whenever the associated preconditions hold in the pre state and the method or constructor exits normally The expression in the clause may also be Nnot specified which is equivalent to omitting the clause The expression must have boolean type and is evaluated in the post state e Status Implemented and used by the static checker e Differences from JML or Java None 3 9 5 signals signals redundantly exsures exsures redundantl
8. Status of JML features 27 e Status Implemented and used by the static checker ESC Java2 checks that assign ments within a routine are consistent with the routine s modifies clauses and checks that the modifies clauses of called routines are consistent with those of the caller However ESC Java2 is not yet able to properly handle the forms everything array and array ei e2 when in the modifies clause of a routine called within the body of a calling routine and remember that modifies everything is the default For example given public int i public int a modifies everything void mO modifies a void nO y 0 modifies a 2 10 void mO 4 0 modifies nothing void pO 4 i 0 nO assert i 0 a 3 0 nt assert a 3 0 a 3 0 nnO assert a 3 0 ESC Java2 should complain that the first assert statement in routine p is not estab lished because m which claims to possibly modify everything might have modified field i It will complain that the modifies clauses of the two routines are in conflict It will also complain about the assert statement if m had a modifies clause of modifies i Similarly the forms of array range designators in the modifies clauses of n and nn are not fully handled so the second and third assert statements do not provoke complaints Store ref expressions that are specific array elements or the forms expr and typename ar
9. notation public void m assert true Message d Java behavior No warnings no exception ever thrown JML behavior No warnings predicate is always true exsures java lang AssertionError e true public void m 1 assert false Message Java behavior ESC Java2 will issue an Unexpected Exception warning JML behavior ESC Java2 will issue an Assert warning There may be a bug here ESC Java complains about types in an exsures clause that are not in the throws list of the declaration but ESC Java2 does not exsures java lang AssertionError e true public void m throws AssertionError assert false Message Java behavior No warnings the exsures clause allows the exception JML behavior Assert error Chapter 3 Status of JML features 47 0 exsures java lang AssertionError e false public void m throws AssertionError assert false Message F Java behavior Postcondition warning the exsures clause disallows the exception JML behavior Assert error 3 19 5 Methods and constructors without bodies in Java files Java requires non abstract non native methods and constructors to have a defined body Some tools such as javadoc allow the bodies to be stubbed with a semicolon in place of the usual block statement ESC Java2 also allows method and constructor bodies within java files to be represented simply by a semicolon This allows classes to be documented and s
10. sesiieeeseess ee eee eee 1 1 2 Acknowledgements sessesseessseeeee ene 1 1 3 Dependencies and license restrictiOOS ooooooooo 2 1 4 Contacts and information 00 c cece cee eee 2 2 Ranning BSC Java sarao cotas 4 3 Status of JML features 5 3 1 File finding and refinement sequences 00 000 eee oc 5 3 2 Format of annotations eegee e c cece cnn a 8 3 3 Compilation unit annotations lessen 10 3 3 1 refine statements 0 0 ccc cece ene n eens 11 3 3 2 model import statements 0 0 00 e eee eee eee ee 12 do automate Imports neha vies die ea de keeles 13 3 4 Access privacy modifiers era whe ashes 13 3 6 Type modifiers 2 2 ecu Rr RR HER Ea e 14 Bl pure nM t tcctctdetdederseeseded ipee delete e px dd 14 35 2 model JML La oui oua ol et eec enyons he cas 14 200 9 weakly IML sour pA Opere ex aa 14 om MED WENT nm 15 35 5 abstract Jawa anki bce eee e RR M ia 18 5 04 SUO AA a 15 AS 18 3 6 Annotations pertinent to a class or interface 15 3 6 1 Ghost fieldS 0ooooooooorrrrronrrarrr nets 15 3 6 2 Model fels renier iir drre raa ea E E ai n iE a 16 3 0 3 Model methods 00000 idad a eee gees 16 3 6 4 Model constructors seess ra na aae e i ai 17 3 6 5 Model class and model interface declarations 17 3 6 6 Java initializer blocks oooooooooooooooo I7 S0 ANMIANZET 25222 piata 1L 3 Cete ad
11. 5 18 placement of annotations ESC Java2 maintains some of ESC Java s features with regard to alternate placement of annotations The customary location for annotations is just prior to the declaration to which they apply with the exception of the in and maps assertions for field declarations ESC Java2 allows in addition the following e Annotations may be placed just prior to a routine s body either just before the opening or the marking an absent body Example public void m pure ensures true e Annotations on field declarations may be placed between the initializer for the field and the terminating semicolon This syntax also applies to local variable declarations within routine bodies Example public Object o new Object non_null e Annotations on formal parameters may be placed between the identifier and the fol lowing comma or right parenthesis Example public void m Object o non null Object oo non null JML does not recognize this syntax with the exception of specification clauses but not modifiers such as pure or non nu11 placed just prior to the routine body Consequently using this style of annotation writing is discouraged in ESC Java2 SHould we generate a caution Chapter 6 Incompatibilities 71 6 5 19 semicolon termination JML requires annotations to be terminated with semicolons ESC Java2 will warn about missing semicolons but does not require them 6 5
12. Simplify executable appropriate to the platform on which ESC Java2 is running Current options are Simplify 1 5 4 linux Simplify 1 5 4 macosx Simplify 1 5 4 solaris and Simplify 1 5 4 exe for Windows Only the first two have had any testing CLASSPATH BOOTCLASSPATH ESC_SPECS sets the default value for specs ESCJ_VERBOSE normally not set When set to some value then more verbose output is obtained This is simply output describing the environment variables used in invoking the tool Chapter 4 ESC Java2 features 62 e ESCJ_STDARGS the command line options to be used in addition to any additional ones on the command line for escjava2 Default nowarn Deadlock e ESC_REMOTE_DEBUG normally not set When set to some value then the value of JAVA_ VM_DEBUG_FLAGS is included in the options supplied to the virtual machine intended to be used to invoke the virtual machine in a debugging mode e JAVA the name of the executable of the Java virtual machine default java e JAVA_VM_FLAGS the set of options to be supplied to the Java virtual machine the default is an empty string e JAVA VM DEBUG FLAGS a set of flags to be used when ESC_REMOTE_DEBUG is set intended to be used to invoke the virtual machine in a debugging mode default is a set of options appropriate for debugging on my machine The following variables affect the running of the Simplify prover e ESCJ SIMPLIFY ARGS the command line arguments to u
13. a construct on that line the annotation will suppress the warning either if it is on the line where the offending action took place or if it is on the line of the associated declaration If there is no list of warning types then all warnings associated with this line are suppressed The warnings of a given type can also be suppressed using command line options The nowarn annotations have no effect on errors or cautions since these are produced by parsing or semantic errors in the source code itself e Status Implemented e Differences from JML or Java JML supports the parsing of these annotations but since JML does no static checking it ignores them ESC Java did not require a ter minating semicolon but JML does ESC Java2 accepts nowarn annotations with or Chapter 4 ESC Java2 features 58 without a terminating semicolon it issues a caution if the semicolon is missing JML should allow a nowarn without a list to be terminated by an end of line 4 2 2 nowarn warning types The static checker used in ESC Java2 and in ESC Java produces warnings as opposed to errors or cautions when it detects source code that might violate the specifications These warnings are categorized into types and can be suppressed or enabled by warning type name using either the nowarn annotation or the command line options nowarn which suppresses individual warning types or warn which enables individual warning types or nocheck which turns of
14. a subclass to modify a formal pa rameter as non_null in an overriding declaration The declarations of the top most declaration were used for all overriding declarations 3 13 2 final Java Description This Java modifier indicates that a formal parameter may not be the target of an assignment in the body of the routine Status Fully implemented This feature does not affect the static checking it simply produces a typechecking error if a final parameter is the target of an assignment Differences from JML or Java None 3 14 Annotation statements within the body of a method or constructor These annotation statements may be intermixed with the statements within the body of a method or constructor They may also be used within model programs 3 14 1 assume assume_redundantly Description This annotation statement inherited from the original ESC Java states a predicate which is then assumed by the static checker It is typically used to state a predicate at some point in the body of a routine that the static checker is unable to establish Checking of the remainder of the body can then proceed with this assump tion Status Implemented Differences from JML or Java None 3 14 2 assert assert redundantly Description This statement will generate a static checker warning if a program execu tion can be found in which the associated predicate is false Note that this is different than the Java assert statement both in synt
15. be static e Status Parsed and typechecked The static checker issues a warning if the constraint is not true as part of the postconditions of any method but does not check constraints in association with constructors e Differences from JML or Java ESC Java2 does not check the restriction on static constraints 3 7 3 represents represents_redundantly e Description A represents clause designates how a model field is related to the con crete fields or other model fields of the implementation The represents clause must be declared static when and only when the model field for which it is providing a repre sentation is declared static if the clause is static then all field and routine references must be static e Status Parsed typechecked and used by the static checker e Differences from JML or Java None ESC Java2 does not check the restrictions on static 3 7 4 axiom e Description An axiom is used to specify a mathematical property independent of the implementation of classes or objects Axioms are always considered to be static Describe circumstances in which an axiom is added to the proof context Are access modifiers allowed e Status Implemented e Differences from JML or Java None Chapter 3 Status of JML features 20 3 7 5 initially initially_redundantly e Description This clause specifies a condition that must hold in the post state of any non helper constructor including the de
16. comments enclosed between and either or Q These are used for primarily experimental constructs that are known to ESC Java2 but are not part of JML Note that JML recognizes additional annotations in these forms e single line comments beginning with 0 e multi line comments enclosed between and either or or Q These latter forms are part of JML but not ESC Java2 to allow for syntax defined by JML but ignored by ESC Java2 It is hoped that the result of the current work Chapter 3 Status of JML features 9 on ESC Java2 will diminish the need for the JML only comments They may remain useful as a way to retain JML annotations that are not processed though they could be by ESC Java2 Status All of these annotation markers are implemented Differences None There is also an interaction between javadoc comments and embedded annotations of which the annotation writer should be aware Consider the text Javadoc material lt esc gt annotations lt esc gt More javadoc material public void m It is somewhat ambiguous as to whether a to associate Javadoc material with the embedded annotations and More javadoc material with the method declaration or b to associate all of the javadoc material with the method declaration The javadoc tool will do the latter and consequently the jmldoc tool does also or will this is an outstanding bug But the writer and the flow of t
17. considered as uninitialized That is a warning will be issued if its value is used before having been assigned a new value Status Implemented as in ESC Java Differences from JML or Java This modifier is not part of JML 3 15 3 final Java Description This Java modifier has the usual meaning that the variable may not be altered or even reassigned its same value after it has been declared and initialized Status Implemented Differences from JML or Java ESC Java2 does not detect invalid assignments to final variables that are not initialized in the declaration 3 16 JML functions extensions to expressions JML defines a number of new operators functions and other constructions for use within expressions that are part of annotations Chapter 3 Status of JML features 38 3 16 1 New operators in JML JML adds to Java the operators described below The gt and lt operators have the same precedence and they bind less tightly than the Java logical or expression That is the expression Cp q gt r s is equivalent to p q gt r s The lt gt and lt gt operators have the same precedence and bind less tightly than gt and lt That is the expression p gt q lt gt r lt s is equivalent to p gt q lt gt r lt s The equivalence and inequivalence operators bind more tightly than the conditional operator The subtype operator lt has lower precedenc
18. form For this purpose ESC Java2 largely follows the desugaring as outlined in FIXME provide ref but it does not need to desugar all clauses of a given type down to one instance of that clause type That paper provides more details on the desugaring process the equivalent but slightly simpler version used in ESC Java2 is outlined here Note that the desugaring process must take care not to lose the location information that is helpful to the user when warning messages are issued The desugaring process first eliminates nesting by replicating and distributing the forall old and requires clauses across the nested groups of clauses Any old 2 Its treatment of assignable clauses is incorrect Chapter 3 Status of JML features 23 clauses are desugared by replacing any references to them by the expression with which they are initialized evaluated in the pre state any forall clause is desugared by wrapping any clause within its scope in a forall quantified expression Also each lightweight specification case normal_behavior and exceptional_behavior keyword is desugared into a behavior specification Specifications from corresponding methods in the refinement sequence are combined connected by also That produces a series of specification cases connected by also each consisting of one group of clauses that is one specification case ESC Java2 s static checker will accept a single specification case For each specification case
19. function returns a long value giving a maximum number of virtual machine cycles needed to execute the method or constructor call which is the argument The argument is not executed and so need not be a pure expression Status Parsed No type checking is performed on the argument nor is any static checking performed Why not allow any expression as the argument space This function returns a long value giving the number of bytes of heap space allocated to the object referred to by its argument The argument must have reference type Status Parsed No type checking is performed on the argument nor is any static checking performed working_space This function returns a long value giving the number of bytes of heap space needed to execute the method or constructor call that is the argument The argument is not executed and so need not be a pure expression Status Parsed No type checking is performed on the argument nor is any static checking performed Why not allow an arbitrary expression nonnullelements This function returns a boolean and takes an argument of a reference array type The result is true if the argument is not null and no element of Chapter 3 Status of JML features 40 the array is null Status Implemented e typeof This function returns a value of type TYPE and takes one argument of any type The result is the dynamic type of the argument The result of typeof applied to a null expression
20. in a Java program as specially for matted comments In particular JML annotations recognized by ESC Java2 are either e single line comments beginning with or e multi line comments enclosed between and either or or e annotations embedded in a javadoc comment between any of the four pairs of markers esc and lt esc gt lt ESC gt and lt ESC gt jm1 and lt jml gt or lt JML gt and lt JML gt The original ESC Java only recognized the first pair These annota tion pairs may not be nested but there may be multiple annotations in sequence ESC Java2 and JML do not restrict where in the javadoc comment an annotation may occur However javadoc requires the annotation to be a part of the textual description and to precede any tag descriptions that are part of the comment The jmldoc tool allows multiple annotations to be intermixed with the tag descriptions Neither ESC Java2 nor the JML tools require the annotation to be enclosed be tween lt pre gt and lt pre gt tags however if you expect reasonable formatting in a javadoc produced HTML page you will likely wish to do so The jmldoc tool does not require lt pre gt and lt pre gt tags to produce good formatting Both the JML tools and ESC Java2 allow multiple symbols in the opening and closing comment markers e g is equivalent to ESC Java2 recognizes these additional comment forms e single line comments beginning with e multi line
21. in a derived type JML constructs may not be modified with spec_public or spec_protected Note that spec_public but not spec_protected was present in ESC Java Status Parsing of access modifiers is fully implemented The access modifiers do not affect static checking Checking that access is used consistently is not implemented Need to verify checks for spec_public and spec_protected and access checks in general Behavior sections do not retain or use their access modifiers ALso ghost and model fields routines 3 5 Type modifiers A class may be modified with the Java modifiers public final abstract and strictfp and the JML modifiers pure model spec_public and spec_protected An interface may be modified with the Java modifiers public strictfp and the JML modifiers pure model spec_public and spec_protected Nested classes and interfaces may have the additional modifiers static protected and private The access modifiers are described in Section 3 4 Access modifiers page 13 In addition the superclass and super interfaces may be modified with the keyword weakly 3 5 1 pure JML e Description The pure modifier when applied to a class or interface indicates that every method and constructor of the class or interface is pure Thus no method may assign to variables other than those declared within the body of the routine Constructors may only assign to the instance fields of the object being constructed and its sup
22. in the first place It also is built upon the work in designing JML and providing tools for JML led by Gary Leavens at Iowa State University with contributions from several other individuals and groups as described on the JML web page 1 3 Dependencies and license restrictions The ESC Java2 tool relies on the following software packages that are separately available and may have their own license restrictions e The original source for ESC Java Simplify and related tools available at http www research compaq com downloads htm1 e Part of the Mocha tool from UCBerkeley optional available at http www cad eecs berkeley edu mocha download j mocha e The CM3 compiler for Modula 3 which is needed to build the Simplify tool available from http www elegosoft com or fink sourceforge net e The testing framework JUnit version 3 8 1 available at http www junit org e Specifications of the Java system classes The most useful set of these specifications are those available with the releases of JML e ESC Java2 does not depend on the JML tool set but it is useful to use the two in combination ESC Java2 is obviously dependent on the grammar and semantics of JML JML is available at http www jmlspecs org 1 4 Contacts and information Further information about JML and ESC Java2 can be obtained from these sources e The KUN ESC Java2 website http www niii kun nl sos research escjava e The JML web site http w
23. io model import myclasses File Chapter 3 Status of JML features 13 public class C extends File the use of File as the superclass is interpreted as java io File by the Java compiler but as myclasses File by JML tools and ESC Java2 Similarly in import java io model import myclasses class myclasses File exists public class C extends File the use of File is interpreted as java io File by a Java compiler but will be deemed ambiguous between java io File and myclasses File by the JML and ESC Java2 tools These are as yet unresolved bugs e Comment This form is also illegal model import typename Either use a Java import statement without a model keyword or enclose the entire model import statement in an annotation comment 3 3 3 automatic imports e Description In Java programs the package java lang is automatically imported into each compilation unit Similarly in JML the package org jmlspecs lang is automatically imported as a model import into each compilation unit e Status Fully implemented in ESC Java2 e Differences None 3 4 Access privacy modifiers Java allows the programmer to modify fields methods constructors class and interface declarations with one of the privacy or access modifiers public protected private or to omit these implying default or package access These modifiers affect the visibility of the associated declaration in other classes ESC Java2
24. issues compile time errors for some misuses of access but the access of any given syntactic entity does not affect the static checking that is performed JML also imposes some rules about access modifiers Some JML constructs are al lowed to be modified by an access modifier the class level clauses described in Section 3 6 Type Annotations page 15 such as invariant and the behavior and example keywords behavior normal_behavior exceptional_behavior example normal_example and exceptional_example In addition the method level clauses e g requires see Sec tion 3 9 Routine Annotation clauses page 25 are assigned the privacy level of the behavior case of which they are a part if in a heavyweight specification case or the privacy level of the method they modify if in a lightweight specification case A specification clause may not use program entities with tighter access restrictions than it itself has For example a requires clause in a protected normal_behavior specification case may not use private fields Java program constructs that may be modified with an access modifier may also be modified with one or the other of spec_public and spec_protected program construct modified with spec_public is considered to have public access for any specification and may Chapter 3 Status of JML features 14 be used in any specification clause a program construct modified with spec_protected may be used in any specification clause
25. may also be annotated with these specifications 3 8 1 Lightweight and heavyweight specifications e Description Lightweight specification cases are simply a series of specification clauses and correspond to the specification style of ESC Java Heavyweight specification cases are introduced with a behavior normal_behavior or exceptional_behavior key word Heavyweight specifications may have optional privacy modifiers see Section 3 4 Access modifiers page 13 and have different defaults than do lightweight specifica tions Within a heavyweight specification if a particular clause type is omitted the default for that clause is as follows ensures true signals java lang Exception true diverges false assignable everything accessible everything callable everything when true duration not_specified infinite working space not_specified infinite The defaults defined by JML for lightweight specifications are Nnot specified in each case This is interpreted within ESC Java2 as follows ensures true signals java lang Exception true diverges true assignable everything accessible everything callable everything when true duration not_specified working_space not_specified The default for the requires clause is determined as follows e If there are some other clauses explicitly given but no requires clause the default is requires true e If there is no specifica
26. may not be relevant to the discussion here 6 5 1 annotation comments beginning with or ESC Java2 allows annotation comments to begin with either or to allow for experimental or old ESC Java constructs that are not part of JML 6 5 2 order of clauses comment needed 6 5 3 splitting of annotations comment needed 6 5 4 helper annotations JML and ESC Java2 differ in which sorts of routines are allowed to be helper routines 6 5 5 typeof applied to primitive types Is this in JML 6 5 6 unreachable There is no unreachable annotation in JML 6 5 7 not_modified ESC Java2 allows arbitrary pure expressions as arguments to not_modified JML only allows store references 6 5 8 specifications of default constructor needs description 6 5 9 loop_predicate discussion needed 6 5 10 skolem_constant discussion needed O 5 11 still deferred discussion needed Chapter 6 Incompatibilities 70 6 5 12 writable_deferred discussion needed 6 5 13 writable_if discussion needed 6 5 14 readable_if discussion needed 6 5 15 monitored_by ESC Java2 still supports the monitored by field annotation as in ESC Java although this form has been deprecated in JML 6 5 16 dttfsa discussion needed 6 5 17 uninitialized ESC Java2 and ESC Java include the uninitialized annotation This is not present in JML 6
27. not used within any static checking e Differences from JML or Java None Chapter 3 Status of JML features 25 3 8 6 for_example specification e Description The for_example keyword introduces specification cases that are use ful and instructional examples for the reader of the specifications Hence they must be logical consequences of the other specifications Each case may be lightweight or be introduced by one of the keywords example normal_example and exceptional_ example these keywords may have associated access modifiers see Section 3 4 Access modifiers page 13 e Status The specifications in a for example section are parsed and typechecked including the example normal example and exceptional example keywords How ever they are not used within any static checking nor is it verified that they follow from the other specifications e Differences from JML or Java None 3 9 Annotation clauses for a method or constructor In this section we describe the clause types that may be part of specifications including implies that and for example sections Note that some clauses have alternate keywords reflecting different personal preferences or different usages among ESC Java2 and other JML tools l hese alternates are complete synonyms 3 9 1 forall e Description The forall declaration declares a universally quantified variable the scope of the declaration is all subsequent clauses for the same routine up t
28. of the specification of Super m line E is an error and C and D are not e Case 3 Super class has no non_null but subclass does class Super public void nonnull non null Object o public void m Object o 1 nonnull o Line A FAILS o null Line B OK class Derived extends Super public void m non_null Object o nonnull o Line C FAILS annotation ignored o null Line D OK annotation ignored Chapter 3 Status of JML features 56 public void mm Object o m o Line E OK new S m o Line F OK In this case it is the derived class that has the non null specification but not the super class This is a problematic case since the body of the overriding method may be called through the overridden signature in which case the actual argument may not be constrained to be non_null Hence the non_null annotation on the overriding formal paramater can be misleading Therefore in ESC Java2 a non_null annotation is ignored if there is any overridden method that has that formal parameter declared without a non_null argument A caution message is provided to warn the user of this behavior Thus ESC Java2 will allow lines B and F since the super class does not limit the values of the parameter similarly line A provokes an error Although the parameter of Derived m is declared non null the non null annotation is ignored Consequently there is no limitation on t
29. option if that is not provided the sourcepath is identical to the classpath The tool also needs a set of specifications of Java system classes and of other library classes you may be using The directory path to these specifications can be included in the sourcepath but it is convenient to specify them to the tool using the specs option which takes a standard directory path as its single argument The command line arguments consist of options and their arguments described in Sec tion 4 3 Command line options page 59 and input entries Input entries may be files directories package names or class names These input entries designate the classes on which ESC Java2 operates Files and directories specified on the command line are found with respect to the current working directory if the paths to the files are relative paths Specifying a directory is Chapter 3 Status of JML features 6 shorthand for listing all of the files in the directory with suffixes known to JML namely refines java refines spec refines jml java spec and jml Input entries may also be fully qualified package or class names In this case the package or class is found by searching the directories of the sourcepath which suffixes are used stop after the first directory found Each file on the command line or file implied by a directory package or class is parsed to determine the package to which it belongs and the name of the type
30. return type the same Java modifiers and the same names for its formal parameters An implementation may be present only in the java file The restriction on the formal parameter names is to simplify reading and to avoid having the implementation have to rename variables in specifications e These JML modifiers must be consistent across all method and constructor redec larations model These JML modifiers may be added by a refinement but may not be removed spec_public spec_protected helper non_null pure e The Java modifier final as applied to a formal parameter must be consistent Chapter 3 Status of JML features 12 across all redeclarations of a method or constructor The JML modifier non_null may be added but not removed e If a refinement file redeclares a method or constructor from a previous refinement or if the method is overriding a method in a super class or interface including the case where a type redeclares a method with specifications even though there is no Java declaration the specification for that redeclared or overriding method must begin with also and must not begin with also when those conditions are not satisfied e A type redeclaration must have the same set of Java modifiers In addition the JML modifier model must be consistent the JML modifiers pure spec public and spec protected may be added by a refinement but not removed e Status The refine statement is implemented in ESC J
31. routine body may fail to establish some normal postcondition on ter minating normally or some exceptional postcondition when terminating by throwing an exception of a relevant type e Pre warns that control may reach a routine call when some precondition of the routine does not hold e Race warns of a possible attempt to access a monitored field while not holding the requisite lock s e RaceAllNull warns of a possible attempt to access a monitored field at a time when all of the objects designated as monitors for the field are null e Reachable warns that control may reach an unreachable pragma e 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 e 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 readable_if has changed e ZeroDiv warns of a possible attempt to apply the integer division or remainder operator with zero as the divisor 4 3 Command line options ESC Java2 has implemented a number of command line options that are not present in ESC Java as well as documenting some of those in ESC Java ESC Java2 also kept many experimental and undocumented options from ESC Java The following is a partial list of command line options available in ESC Java2 so
32. sequence other than that they must be in the same package but not necessarily in the same directory In particular aside from the suffix for the MRCU and java and class files there is no restriction on the suffixes that the files may have nor on the order of suffixes in the refinement sequence There is also no restriction on the prefixes of the file names other than that the MRCU the java file and the class file must have the typename as the prefix However it is good style if all of the files in the refinement sequence have the same prefix If a file has a filename prefix that does not match the type declared within it it is in danger of being misinterpreted as belonging to a different type Consequently a caution is issued to the user if this situation is discovered e Once an MRCU is found the remainder of the refinement sequence is determined by the refine statements But which file is found as the MRCU may depend on the contents and order of the directories in the sourcepath This order dependence is by design as it is thought that the user may use this feature to choose different starting points along the refinement sequence for processing It may also lead to inadvertent errors e It is an error if a sequence of refine statements defines a circular sequence of refinement files e The java source file and the class file for the given fully qualified type are found as defined by Java independently of determining the refinement
33. sequence using the sourcepath and the classpath respectively Note that if the java file declares more Chapter 3 Status of JML features 7 than one type then there may be more than one class file relevant to the refinement sequence e Note that if the java file declares more than one type then the files of the corresponding refinement sequence must contain the specifications for all of the declared types e The specifications for the classes declared in the files of a refinement sequence are the combination of the specifications in all the files of the refinement sequence The Java signature of the classes is obtained from the relevant java or class files The source code implementation of the classes is determined from the java file If no java file exists or it does not contain an implementation of a method then the check of that method will be a trivial pass checks of the usage of the method within other routine bodies will still be performed e It may be that a refinement sequence exists and does not contain the file specified on the command line ESC Java2 issues a caution to the user in this case However if no refinement sequence is found no caution is issued even if the command line file is not on the sourcepath it is simply used as the specification of the declared classes e It may be that the refinement sequence exists and a corresponding java file exists in the sourcepath but the refinement sequence does not con
34. that it declares ESC Java2 and JML tools then use the following procedure to find the refinement sequence for the given fully qualified type When the specifications of types referenced in files being processed by ESC Java2 are needed they are found using the same procedure e Search each directory of the sourcepath in turn looking for the first sourcepath di rectory containing a directory hierarchy for the given package containing a file whose name has the type name as its prefix and one of the following suffixes refines java refines spec refines jml java spec jml If the directory contains more than one such file the one with a suffix closest to the beginning of the list of suffixes is used This file is called the Most refined compilation unit MRCU e If the MRCU contains a refine statement then the file named in it is sought in the sourcepath in the same package but not necessarily the same directory as the MRCU It is an error if a file named in a refine statement cannot be found in the sourcepath Files found in this way are parsed in turn and the files named in each refine statement are sought This procedure is repeated recursively until a file is found that has no refine statement The sequence of files so found is called the refinement sequence The refinement sequence may contain the java file for the type JML allows class files e The rules above do not restrict the filenames of the files of the refinement
35. the expression which is its argument must be evaluated in the pre state It is used in ensures and signals clauses to distinguish pre and post state values It may also be used within annotations in the body of a routine e g assert assume set statements Status Implemented JML does not allow old in set statements or local ghost variable initialization Xnot_modified This function of an arbitrary number of arguments returns a boolean value indicating whether all of the arguments are unchanged between pre state and the current state It may be used in an ensures or signals clause and in annotations in the body of a routine It is equivalent to boolean AND of x old x for each argument Status Implemented not part of the original ESC Java Differences ESC Java2 allows arbitrary pure expressions as the arguments of not_ modified JML only allows store locations Check that ESC Java2 and JML actually allow this in routine bodies fresh This function takes a single argument of any reference type and returns a boolean The operator may be used in an expression that is evaluated in the post state The result is true if its argument is non null and was not allocated in the pre state Status Implemented CHecks needed that this is allowed in set and initialization statements and works correctly both in ESC Java and JML reach description status differences needed here deprecated duration This
36. the unsoundness of requires noted in section C 0 4 of the ESC Java User s Manual is corrected However the behavior of some specifications will change since specifications of an overriding method are no longer simply textually conjoined with the specifications of an overridden method For example in ESC Java the specification of m in this code public class Super 0 requires i gt 0 public int m int i public class D ensures result gt 0 public int m int i was interpreted as 0 requires i gt 0 ensures result gt 0 whereas in ESC Java2 it is requires i gt 0 true 0 ensures i gt 0 gt true 0 ensures true gt result gt 0 which is equivalent to requires true ensures result gt 0 3 19 13 2 Defaults and inheritance The defaults for missing clauses were described in Section 3 8 1 specifications page 21 The effect of the default for requires is demonstrated in these examples Given class Super requires P Chapter 3 Status of JML features 52 ensures Q public void m class Derived extends Super 1 no spec given default is requires false public void m the two classes behave as if they had these specifications class Super 0 requires P ensures P gt Q public void m class Derived extends Super 1 also 0 requires P ensures P gt Q public void m Given class Sup
37. used in static checking Comment The keyword max is used both as a quantifier and as a function The parser is able to distinguish the two usages 3 16 5 Set comprehension JML has a syntax for expressions whose value is a set An example is new JMLObjectSet Integer i o has i amp amp i intValue gt 0 No side effects are permitted in the predicate Status ESC Java2 parses and typechecks set comprehension expressions with the following omissions e Set comprehension in class level specifications is not handled e Expressions containing set comprehension are not used in static checking e No restrictions on the type of the set are imposed e The JML restrictions on the form of the predicate are not checked e ESC Java2 should check and forbid Java or JML modifiers in the bound variable dec laration 3 16 6 not_specified This may be used within the guidelines of the JML grammar as the predicate or store ref expression in an annotation clause JML allows tools to provide their own behavior for not_specified Escjava2 treats such clauses as if they were not present making them equivalent to the default for that clause type Status Fully implemented 3 16 7 private_data description status differences needed here 3 16 8 Mother description status differences needed here Chapter 3 Status of JML features 43 3 16 9 Other Java operators and expression syntax Java operators and expres
38. used in subsequent annotation statements within the body such as assert assume or set statements Such declarations may also be declared final or non_null and may have initializers Status Implemented Differences from JML or Java None 3 15 Modifiers that may be applied to local declarations Declarations within the body of a method constructor or initialization code introduce local variables used only during the execution of that body of code Privacy modifiers static and instance are not applicable to these declarations JML defines local ghost declarations as well but not local model declarations The following modifiers are allowed 3 15 1 non_null JML Description A local declaration of a variable of reference type within the body of a method or constructor including local ghost declarations may be modified with the JML annotation non_null This requires that the initial value and any subsequently assigned value for that variable must not be null must have an initializer Status Fully implemented in ESC Java and ESC Java2 Failure to initialize is not detected Or failure to initialize with null value Also ghost declarations Differences from JML or Java None 3 15 2 uninitialized JML Description This JML modifier may be applied to a local variable declaration within the body of a block of code It indicates that although the variable has been initialized with an initial value it should be
39. warning messages ESC Java2 continues ESC Java s use of four levels of error messages e fatal errors are problems usually invalid syntax that prevent ESC Java from proceed ing further in parsing and checking files e errors indicate illegally formed input files though processing may continue to find other errors or even to attempt static checking of the files errors or checks subsequent to the first problem may be erroneous as a result of earlier problems e cautions indicate situations that are not illegal but may be misleading to the user a common example is features that are parsed but not checked also some illegal JML constructs are reported using cautions if ESC Java2 can unambiguously correct them e warnings indicate situations in which the static checking phase could not determine that annotation specifications were satisfied such as an inability to determine that an object reference is non Null when it is dereferenced The reporting of cautions and warnings can be controlled by command line options noCautions nowarn warn nocheck 4 2 Nowarn annotations and warnings 4 2 1 nowarn annotations e Description A nowarn annotation has the form nowarn comma separated list of warning types or simply 0 nowarn The annotation is associated with the line in the source file on which it is located rather than with a grammatical construct It is used to suppress warnings from the static checker associated with
40. 20 need for the field method constructor keywords ESC Java2 parses non null in method declarations 6 5 21 omission of method bodies ESC Java2 does not require bodies of methods and constructors to be present even in java files The JML checker does require such bodies in java files although not in specification files with other suffixes 6 5 22 Errors and cautions Some JML errors are reported as cautions by ESC Java2 This enables as much checking to be performed as possible in cases in which the correction to the error seems obvious 6 5 23 membership in lockset The features associated with locks and the sets of locks associated with an object were part of the original ESC Java and only recently added to JML JML needs documentation of these features Mockset max and membership in a lockset JML does not yet include the membership in a lockset operation 6 6 JML features needing clarification Need discussion of these 6 6 1 model programs 6 6 2 callable accessible 6 6 3 when measured_by 6 6 4 initializer static_initializer 6 6 5 desugaring of forall 6 6 6 weakly 6 6 7 hence_by 6 6 8 use of result in duration and working_space clauses 6 6 9 instance fields and this in constructor preconditions 6 6 10 rules about splitting annotations across comments 6 6 11 typeof applied to primitive types Chapter 6 Incompatibilities 72 6 7 Desired extensions This is a list of some discussed but not res
41. 3 6 2 Model fields e Description Model fields are declarations within an annotation prefixed by the modifier model They do not represent actual specification fields as do ghost values Rather their values are implied by the concrete representation of the class either by an explicit expression in a represents clause or implicitly by a boolean condition in a such_ that form of the represents clause They are used to supply values that model the behavior of the class A model field may have these modifiers access modifiers see Section 3 4 Access modifiers page 13 static what about final and the JML modifiers non_ null monitored and instance see Section 3 12 Field Annotation modifiers page 32 Model fields may not have initializers An initializer expression would make nice syntactic sugar for the combination of a model declaration and a represents clause e Status Model fields are parsed and used in typechecking Inconsistencies between multiple represents clauses are usually not found e Differences from JML or Java None 3 6 3 Model methods e Description Model methods are method declarations within an annotation and mod ified with the modifier model They declare methods that may be used in model pro grams and if pure in specifications Model methods may have these Java modifiers public protected private static abstract final synchronized strictfp they may have these JML modifier
42. 4 imodifiables vinos nace pio 26 modifiable_redundantly 0 000000 26 3nodfeesu u s 2 4 iii 26 64 modifies_redundantly 26 most refined compilation unit 6 MRGU s cioe ir rra 6 N MAUVE ss pane qure shined o nique IE ERE SR 31 P Private Cm 13 Proteina 13 p blic pcia io id 13 quantified expressi0OS 0 o o oooooooooooo 41 R refinement sequence oocooocccooocccooo o 5 6 set comprehension ariei eere es 42 SIGNALS sens isse pe ee ae TU D pP Eq Id 26 signals_redundantly 4 26 DIMpPlify cic ioc t betaine bias eee eee Motes be 2 O dere een iUe eem 5 61 spec protected i is lsco ra RR a TIS 13 Speccpublie 2 von tech o be ERR ee es 13 ciini 31 Strichips idi rata abad 32 SUFIDB S oe de edema nae EE ERR Re EPI US 63 SUIS cid ERpIeIPeRekh iex 4a er RISE 5 synchronized add whee ben bets 31 V VENOM ias ibid onbres i edu 61
43. Differences from JML or Java None 3 9 9 duration e Description This specification asserts that the execution of the routine with the given preconditions will not exceed the stated number of virtual machine cycles The expression in the clause may also be not_specified which is equivalent to omitting the clause The expression must have long type and is evaluated in the post state What happens if result is undefined because of an exceptional return e Status Parsed and typechecked but not used in any static checking e Differences from JML or Java None 3 9 10 working_space e Description This specification asserts that the execution of the routine will not utilize more than the stated number of bytes of heap space The expression in the clause may Chapter 3 Status of JML features 29 also be not_specified which is equivalent to omitting the clause The expression must have long type and is evaluated in the post state What happens if result is undefined because of an exceptional return Status Parsed and typechecked but not used in any static checking Differences from JML or Java None 3 9 11 accessible Description description description needed The list of locations in the clause may also contain the special keywords nothing everything Any expressions e g array indices are evaluated in the pre state COmment on not specified Status status status unknown Differ
44. ESC Java2 Implementation Notes VERY MUCH A PRELIMINARY INCOMPLETE DRAFT David R Cok cok frontiernet net November 2004 Abstract ESC Java2 is a tool for statically checking program specifications It expands significantly upon ESC Java on which it is built It now is consistent with the definition of JML and of Java 1 4 It adds additional static checking to that in ESC Java most signif icantly it adds support for checking frame conditions and annotations containing method calls This document describes the status of the implementation of ESC Java2 along with some notes regarding the details of that implementation Keywords Behavioral interface specification Java JML Escjava ESC Java ESC Java2 model based specification assertion precondition postcondition frame 2003 CR Categories D 2 1 Software Engineering Requirements Specifications lan guages tools theory JML ESC Java ESC Java2 D 2 4 Software Engineering Soft ware Program Verification assertion checkers class invariants formal methods pro gramming by contract F 3 1 Logics and Meanings of Programs Specifying and Verifying and Reasoning about Programs assertions invariants logics of programs pre and post conditions specification techniques Copyright 2003 2004 David R Cok CVS Version Revision CVS Date Date Table of Contents Ll JIntroducilof cicsR i 3 Re 288 5056825255 1 1 1 Motivation and Background
45. Terminating semicolons JML requires annotations to be terminated by semicolons The original ESC Java did not The absence of semicolons is illegal JML but is some times tolerated by ESC Java2 ESC Java2 will warn if a semicolon is missing Such warnings can be suppressed with the noSemicolonWarnings command line option 3 3 Compilation unit annotations Compilation unit annotations are placed prior to the declaration of any type within the compilation unit Chapter 3 Status of JML features 11 3 3 1 refine statements e Description A JML refine statement indicates that the containing compilation unit adds additional specifications to those contained in the referenced file If present it must be located after any Java package statement and before any Java or model import statements There may be only one refine statement in a compilation unit It has the form 0 refine filename The refine statements define a refinement sequence as described in Sec tion 3 1 File finding page 5 Here we focus on the combining of the compilation units in a refinement sequence to produce a single set of specifications for a type Each compilation unit has its own set of declarations and specifications all of which must be consistent They are subject to the following rules violations of which provoke error messages e All files of the refinement sequence must belong to the same package though not necessarily the same directory the type names
46. a 17 3 6 8 static_initializer 0 00 0 cnet eee 18 3 6 9 Java method constructor and field declarations 18 3 6 10 Nested Java type declarations ooooooooooooo 18 3 7 Annotation clauses for a class or interface oo oooooooo o 18 3 7 1 invariant invariant redundantly 0 19 3 7 2 constraint constraint redundantly 19 3 7 3 represents represents redundantly 19 Qui ASOT ode hoe RE pe On teo d e RO COS UR ee 19 3 7 5 initially initially_redundantly 2 000 20 3 7 6 readable and writable o oo ooooooooono oo o 20 3 8 Annotations for a method or constructor 2 055 21 3 8 1 Lightweight and heavyweight specifications 2T B82 alBSO i OOO Rer bebe EROR PE ER pea d EP RUE 23 3 8 9 Model program 4 34 dia eI Ree CRI RA 24 B84 code contraet oseas cesse ete ep cic dod onte Ro e 24 3 8 5 implies that c ined ee bane Lr RR RR Rad 24 3 8 0 for example specification lissse esie eese 24 3 9 Annotation clauses for a method or constructor 25 SOM Toral aues ud al ac acted dele UR SR RR 25 39 2 Oldie nba be Ide Ea c eee qua oae 25 3 9 3 requires requires redundantly pre pre redundantly 26 3 9 4 ensures ensures redundantly post post redundantly 26 3 9 5 signals signals redundantly exsures exsures redundantly ssssseeeeeeee ees 26 3 9 0 modi
47. a composite precondition predicate is formed by taking the conjunction of the predicates in each of the requires clauses in that specification case and making that conjunction the argument of an old function pre predicate Nold p1 amp amp p2 Each clause within the specification case is altered by constraining its action using that conjunction Calling that combined predicate pre predicate we transform each clause as follows e ensures pred becomes ensures pre predicate gt pred e diverges pred becomes diverges pre predicate gt pred e modifies clauses Multiple modifies clauses within one specification case are com bined into one clause along with the composite precondition for that specification case modifies clauses from different specification cases are not combined e signals type id pred becomes signals type id pre predicate gt pred e when complete this e accessible complete this e callable complete this e duration complete this e working space complete this The requires clauses are desugared by replacing all of the requires clauses in all of the specification cases with a single requires clause whose predicate is the disjunction of the conjuctions formed for each specification case without the enclosing old When the static checker creates a VC to be used as a precondition for calling a method it forms a disjunction of the requi
48. a had an implicit default for a missing modifies clause namely that nothing was modified modifies nothing in JML JML defines the default instead to be modifies everything ESC Java2 has implemented this as the default The implicit use of modifies nothing had the danger of missing or hiding many errors in usage since un expected changes to variables caused by calling a routine are a not unusual source of bugs However some outstanding issues are discussed in the following section There are three special cases of defaults for the modifies clause e Methods annotated as pure including methods in pure classes have a default modifies clause of modifies nothing e Constructors annotated as pure including constructors in pure classes have a defaults modifies clause of modifies this It may have non default modifies clauses but these may not allow more fields to be modified than are contained in this e A default constructor that is not declared has a default modifies clause that allows the same fields to be modified as does its super class constructor 5 10 modifies everything The use of nothing everything and not_specified in a modifies clause are now implemented not_specified is equivalent to everything and everything is the default However there are two issues outstanding e With this default any method that has no annotations is assumed to have the behavior modifies everything There is very little reas
49. ang Object is ensures result typeof this java lang Class getClass which can only be written if the value on the left hand side of the ensures predicate which has type java lang Class can be compared to the value on the right hand side which has type TYPE 3 19 12 exceptions in annotation expressions Discuss the behavior of logical and short circuit operators in the presence of undefined expressions or expressions that throw exceptions 3 19 13 Specifications and inheritance Talk about behavioral inheritance 3 19 13 1 Desugaring in the presence of inheritance ESC Java has some limitations and some unsoundness in handling the inheritance of spec ifications If a superclass stated a precondition with a requires clause then a subclass could not state an additional precondition If a superinterface stated a precondition an im plementing class was permitted to state a precondition using the also_requires keyword but the discussion in the ESC Java User s Manual acknowledged this to be an unsound construct ESC Java2 has corrected this problem by using the syntax and desugaring approach outlined by JML JML allows subclasses to have additional requires clauses and does not utilize the also_requires syntax Consider the following example the handling of super interfaces is the same as the handling of super classes Chapter 3 Status of JML features 50 public interface Super requires P1
50. are implemented in ESC Java2 with the following exceptions e ESC Java2 does not yet use the search order for the MRCU as described Rather it finds the file with the most active suffix anywhere in the sourcepath regardless of its position in the sourcepath e When finding a package named as an input entry ESC Java2 combines all of the packages by that name in any directory of the sourcepath rather than just using the first one e Check the caution for CL file not in the RS OK Chapter 3 Status of JML features 8 e Check the caution for the Java file not in the RS OK e Check the caution if a misnamed file is found in the RS OK e Check that there is an error if a refine file cannot be found OK e Check that the sourcepath is actually defined and used OK e Can ESC Java2 handle refining a class e Should we have an option to find MRCUs with any suffix e Should we have an option to find the whole chain whatever the order of the sour cepath and suffixes e Should we have an option to change expand the list of MRCU suffixes e Should we have an option to define implicit refine statements in order for example to connect specification files to implementation files when the implementation files suddenly become available and we don t want to edit all of the files 3 2 Format of annotations e Comment format JML annotations are included
51. ava2 Check that all the rules above regarding consistency of modifiers are enforced They are not all yet e Comment on combining refinements There are at least 3 ways to carry out the combining of refinements a by syntactically combining the relevant text b by typechecking each compilation unit independently and then combining the sig natures c by typechecking each compilation unit in turn in the context of the compilation units it is refining Discuss implications and differences ESC Java2 uses a 3 3 2 model import statements e Description A model import statement has the form model java import statement Note that simply writing java import statement is not legal JML A model import statement may occur wherever a Java import statement may be placed A model import statement introduces types that are used only by annotations Annotations may also use types introduced by Java import statements e Status Model import statements are fully implemented e Differences from JML or Java This feature is implemented in ESC Java2 as it is in JML However both have the following problem The model import statements are parsed by JML tools and by ESC Java2 as if they were Java import statements Thus they may introduce or resolve an ambiguity in class name resolution of names used in the Java source code in a compilation unit or cause misinterpretation of a type name For example in import java
52. ax and in semantics The command line options jmlAssertions will cause Java assertions to behave like JML assertions see Section 3 19 4 Java and JML assert statements page 45 Status Fully implemented Differences from JML or Java None Chapter 3 Status of JML features 36 3 14 3 set e Description The JML set statement is used as a statement within the body of a routine to assign a value to a ghost field or variable ESC Java allowed only fields to be set ESC Java2 allows in addition the declaration of local ghost variables and the assign ment of values to them using set statements Only assignments with are allowed and the right hand sides of the assignment statements must be pure expressions e Status Implemented e Differences from JML or Java None What about using set statements containing statements other than assignments such as x chekc on the purity requirement in JML 3 14 4 unreachable e Description This is a statement that asserts that the command flow of the program will never reach this point If the static checker suspects that there is a program execution that can do so it will issue a warning It is equivalent to an annotation stating assert false There is no conditional unreachable statement but the equivalent can be created using an assert statement e Status Implemented e Differences from JML or Java There is no unreachable annotation in JML 3 14 5 hence_by hence_by_redundantl
53. ce code according to the definition of Java for the given version The only implemented effect of this option is the interpretation of assert as a keyword if the version is 1 4 and as a normal identifier if the version is not 1 4 The default is version 1 3 In the absence of other options enabling Java 1 4 will cause Java assertions to be treated as exceptions the javaAssertions mode See Section 3 19 4 Java and JML assert statements page 45 sourcepath directory path specifies the directories in which source and specification files for types are sought the default is to use the classpath specs directory path specifies a directory path of specification files ESC Java2 will not work well without a set of specifications The jar file constituting a release contains a current version of the JML specifications if ESC Java2 is run from that jar file those specification will be the default value of this option v verbose output describing the steps of processing ESC Java2 has added more output to that produced by ESC Java warn warning type turns on the reporting of warnings of the given type FIXME check for others to be documented group the above by typel 4 4 Environment variables affecting ESC Java2 There are several environment variables which alter the behavior of ESC Java2 or Simplify which is called by ESC Java2 These are described in this section ESCTOOLS RELEASE ESCTOOLS_ROOT SIMPLIFY the name of the
54. clauses 000 e essei 65 5 10 modifies everything 0 cece eee cee eens 65 5 11 Checking of modifies 0 0 0 ee cece eee eens 65 A NUVBGOL a ceret pets lind aden gaa ebd eti lea Re dus 65 5 13 Use of pure routines in annotations o o ooooooooo 66 5 14 Checking of model fields 0 0 0 0 elei 66 Bild ynot modified si etudes reet or Rd edible 66 Incompatibiliti 8 cerro doses XR TEES 67 6 1 Major features of Java not implemented in ESC Java2 67 0 L 1 Java Lio ai edit ad deel eed aed Mea dae See 67 6 1 2 anonymous and block level classes 67 6 1 3 Serialization e ti ee eR Rh RR RAUS EUR CE Rd CR Bates 67 6 1 4 most multi threading considerations 67 60 1 5 Java QeNETICS ico corro ead DROP IER bed dade 67 6 2 Major features of JML not implemented in ESC Java2 67 6 2 1 code contract clauses 0 00 c eee cece eee eee eee 67 6 2 2 some aspects of store ref expressions 000 67 6 2 3 implies that and for example behavior 67 6 2 4 splitting of annotations across comments 67 iv 6 3 Limitations of static checking 0 0 00 else 67 6 4 Incompatibilities with ESC Java o oooooocmoommmo 68 6 4 1 Error messages and warnings lisse essere 68 042 alBOicoltonxeererserihe emer i o i EA Y O4 ipei deed ees 68 6 4 3 inheritance of specifications
55. corresponding meanings in JML the less than and less than or equal operators are used to compare locks Any object that is listed as a monitor in a monitors for clause or is identified implicitly or explicitly in a Java synchronization statement is a lock in addition to its declared use as an object In order to reason about deadlocks the user must define a partial order on locks and have the code acquire the locks only in increasing order The partial order may be defined using axiom clauses the operators are used to compare locks by this partial order They take two locks as arguments and return true if the left hand object is less than or less than or equal to respectively the right hand object according to the partial order axioms and returns false otherwise The comparison is independent of whether the locks have actually been acquired the lockset expression supplies that information The ESC Java User s Manual provides additional information and examples about Deadlock and Race detection Status Implemented Chapter 3 Status of JML features 39 3 16 2 New JML expressions functions and values result This keyword denotes the result of a method that returns a value It may be used in an ensures clause but not a signals clause What about duration working _space clauses Status Implemented old This pseudo function takes one argument of any type and returns the value of its argument It is used to indicate that
56. ctools2 jar file that comes with the release This launches a GUI tool that runs ESC Java2 The jar file has the JML specs built in and uses them by default You will have to tell the GUI tool the location of the appropriate Simplify executable for your platform what value of CLASSPATH to use and what the input files and other options should be Versions of Simplify for several platforms are supplied with the release 2 Execute the esctools2 jar file using the command java jar esctools2 jar This allows you to launch the GUI tool from the command line and to add other command line options as initial settings of the GUI tool In particular you can specify the location of the Simplify executable with the option simplify PathToSimplify in which you supply an absolute path to the correct Simplify executable A directory path for alternate Java specifications can be supplied as the argument to the specs option The classpath is specified with the classpath option 3 Execute a non GUI version of ESC Java2 using the script supplied with the release escj The script can guess the location of the release and of the Simplify executable You can help it by defining the environment variable ESCTOOLS_ROOT as the absolute path to the location of the directory containing the release and by defining the variable SIMPLIFY as the name of not the path to the Simplify executable If your working directory is something other than the directory containing the
57. d They are described in this chapter 5 1 Handling of specification inheritance The semantics of the inheritance of specifications has changed from ESC Java to ESC Java2 ESC Java2 now matches the semantics of JML The implementation required changes in the way that translation of specifications into guarded commands is performed The change in semantics is described with examples in Section 3 19 13 Specifications and inheritance page 49 5 2 non_null The semantics of non_null applied to formal parameters in the presence of inheritance has changed from ESC Java to ESC Java2 If an overriding declaration declares a formal parameter non_null then all overridden declarations must have that formal parameter declared non_null This is described in more detail in Section 3 19 13 3 Inheritance and non null page 53 5 3 Translation of the Java 1 4 assert statement The handling of the Java 1 4 assert statement is discussed in Section 3 19 4 Java and JML assert statements page 45 The assert statement is translated into equivalent Java or JML constructs and the static checker is used without modification 5 4 Semantics of String Although java lang String is a reference type in Java it has a number of built in properties that were not modeled in Esc Java but have been added in Esc Java2 These properties are the following e The built in and String concatentation operators e Explicit String literals are interned e The intern me
58. d is declared pure then all overriding methods are also pure whether or not they have an explicit declaration to that effect Note that a pure constructor may not modify static fields e Status Fully supported e Differences from JML or Java None 3 10 2 non_null JML methods only e Description Modifying a routine with the non nu11 modifier is valid only for methods that return objects as return values and not for constructors The modifier specifies that the return value is never null It is equivalent to a specification of ensures result null added to each specification case of the method s specification in all of the files of the refinement sequence but not of a superclass s specification of that method Note that superclass and subclass declarations of a method each independently may have or not have non nu11 declarations A method s implementation must satisfy the superclass specification and independently satisfy the subclass specification There is a more thorough discussion in Section 3 19 13 3 Inheritance and non_null page 53 e Status Parsed typechecked and supported by the static checker e Differences from JML or Java None Chapter 3 Status of JML features 31 3 10 3 helper JML Description This modifier indicates that the method or constructor in question is used as an internal helper routine and that the method or constructor is therefore not expected to satisfy any of the class level i
59. dden by ESC Java2 3 13 Annotation modifiers for formal parameters These modifiers may precede the type name of a formal parameter within the declaration of the method or constructor 3 13 1 non_null JML e Description Modifying a formal parameter with a non null modifier is equivalent to adding a precondition stating that the parameter is not equal to null and requiring that any assignment to that variable assign a non null value It is only legal for reference types not for primitive types The non_null condition is in addition to the composite Chapter 3 Status of JML features 35 specification formed from the complete refinement sequence Hence it is equivalent to adding a precondition requiring the parameter be non null to the desugared specifi cation of the routine as well as the conditions on subsequent assignments within the body of the routine Note that parameters of superclass and subclass declarations of a method each indepen dently may have or not have non nu11 declarations A method s implementation must satisfy the superclass specification and independently satisfy the subclass specification A more thorough discussion is given in Section 3 19 13 3 Inheritance and non null page 53 Status The modifier is parsed checked and supported by the static checker Differences from JML or Java None known FIXME does JML detect problems with overriding methods Comment The original ESC Java did not permit
60. defined as the type of type values The following table shows the relationships between Java and JML syntax and quantities In the following T is a type name such as int or java lang String t is an expression of TYPE type and e is an expression of any type JML Java Type names denoting the type of type NTYPE java lang Class values Chapter 3 Status of JML features 49 Expression that is a type literal corre type T T class sponding to a given type name Expression whose value is the type value Class forName s corresponding to the name in a String Expression whose value is the type value typeof e e getClass corresponding to the dynamic type of an expression subtype relationship between two type t1 lt t2 t2 isAssignableFrom t1 values Expression has type or is subtype of type typeof t lt t instanceof T name type T A type value corresponding to the ele elemtype t t getComponentType ment type of an array type In JML and ESC Java2 TYPE and java lang Class have been made equivalent thus the corresponding quantities in each row may be used interchangeably in annotations The one exception in ESC Java2 is that methods of Class or Object may not be invoked on a value of type TYPE The location where the equivalence is particularly needed is in writing the specifications for a method such as java lang Object getClass which is inherited by every reference type in Java The natural specification in java l
61. e Systems Research Center at DEC later Compaq now HP http www research compaq com ESC Java parses JML like annotations in a Java program and warns in a modular way about annotations that may not be justified by the Java source of the given classes and the specifications of other classes The program works accurately enough and fast enough that it has been found to be a useful tool Its usefulness is diminished by limitations in the kind of annotations that it can parse and check and also in that its annotation language is similar to but is neither a subset nor a superset of JML The goal of the ESC Java2 work is to extend the use of ESC Java by a updating the parser of ESC Java so that it is consistent with the current definition of JML and Java b packaging the updated tool so that it is more easily available to a larger set of users consistent with the source code license provisions of the ESC Java source code c and extending the range of JML annotations that can be checked by the tool where possible and where consistent with the engineering goals of ESC Java This document records the status of this implementation It is not intended to be a tutorial or a reference guide for either JML or ESC Java or ESC Java2 Rather it records the status of the features of JML the status of their implementation in ESC Java2 the degree to which the annotation is logically checked and any differences between ESC Java2 and JML e More detai
62. e handled properly A second aspect of modifies clauses not being fully handled is the following Within a class that has a field named i 0 modifies this public void m n Chapter 3 Status of JML features 28 0 modifies i public void n provokes no complaints since i is recognized as part of this However in 0 modifies i public void m 1 nO 0 modifies this public void n ESC Java2 will issue a warning since it does not check that all possible fields of the class any of which might be modified by n are listed in the modifies clause of m The similar situation holds for static members 3 9 7 diverges diverges_redundantly e Description This clause states a predicate that must hold in the pre state if the method never terminates given that the associated precondition holds in the pre state The expression in the clause may also be not_specified which is equivalent to omitting the clause The expression must have boolean type and is evaluated in the pre state e Status Parsed and typechecked but not used in any static checking e Differences from JML or Java None 3 9 8 when e Description description description needed The expression in the clause may also be not_specified which is equivalent to omitting the clause The expression must have boolean type and is evaluated in the pre state e Status Parsed and typechecked but not used in any static checking e
63. e than the shift operator lt lt the same precedence as the comparison operators lt gt lt and gt and has higher precendence than the equality and inequality operators e lt gt This operator equivalence takes two boolean arguments it returns a boolean value of true if the two arguments are both true or both false and false otherwise Status Implemented e lt gt This operator inequivalence takes two boolean arguments it returns a boolean value of false if the two arguments are both true or both false and true otherwise A lt gt B is equivalent to A lt gt B Status Implemented e gt This operator implies takes two boolean arguments and returns a boolean value of true if the first is false or the second is true and returns false if the first is true and the second is false Status Implemented e lt This operator reverse implication or explies takes two boolean arguments and returns a boolean value of true if the second is false or the first is true and returns false if the second is true and the first is false A gt B is equivalent to B lt A Status Implemented e lt This operator takes two arguments of type TYPE or equivalently of type java lang Class it returns true if the left hand argument is the same type as or a subtype of the right hand argument Status Implemented e lt lt In addition to their usual meaning in Java and
64. ed but ignored by ESC Java2 This feature was not present in ESC Java 3 5 4 final Java e Description A final class may not have subclasses e Status This modifier is parsed and checked It does not need any static checking e Differences from JML or Java None 3 5 5 abstract Java e Description A class must be declared abstract if it has abstract methods An abstract class may not be instantiated only non abstract subclasses of an abstract class may be instantiated All interfaces are by definition abstract using the abstract modifier on an interface has been deprecated e Status This modifier is parsed and checked It does not need any static checking e Differences from JML or Java None 3 5 6 strictfp Java e Description The strictfp modifier determines the semantics of floating point opera tions within the class so modified e Status This modifier is parsed and typechecked The static checker does not make use of this information Is it inherited or does it just apply to the implementations given in that class If so what about interfaces maybe applies just to initializers in interfaces e Differences from JML or Java None 3 5 7 static Java e Description static is a Java modifier that may be applied to classes and interfaces that are members of enclosing classes e Status Implemented e Differences from JML or Java None 3 6 Annotations pertinent to a class or interface These a
65. ed in JML in favor of monitors for It may at some time be deprecated in ESC Java2 as well Check this 6 4 6 readable if Discussion needed 6 4 7 initially old style ESC Javal had a field declaration annotation that was a modifier of the field declaration itself JML has replaced that with a class level declaration similar to the invariant clause that states an assertion that must be true of objects immediately after construction The old form is deprecated in JML but supported still in ESC Java2 6 4 8 semicolon termination The original ESC Java did not allow and later tolerated termination of clauses by semi colons JML requires this ESC Java2 issues a caution if a required semicolon is not present see Terminating semicolons page 10 6 4 9 Routine bodies in spec files The original ESC Java allowed routines declared in specification files to have bodies which were then checked ESC Java2 allows bodies for Java declarations only in java files Model Chapter 6 Incompatibilities 69 methods model constructors and routines in model classes may have bodies in at most one specification file Check the behavior of JML 6 5 Non JML features in ESC Java2 There are some syntactic constructs accepted by ESC Java and continue to be accepted by ESC Java2 or are additions in ESC Java2 that are not part of JML discussion needed have not checked how some of these are used in ESC Java so they
66. ee eed wae 60 preferSOurce s lia eL REP e ha oa 61 oil Pm 61 SSM MEY A ke pc Rep Rer x Ab 61 zi PP D 61 sSourcepath 2 ni di 61 A riiidbdo ke ed seriden kun Reds adele ERG E 61 p 61 A 61 n A A 8 PPO is E E T ANE isis 8 TINO a RU nea 8 77 lt O 38 iD ca at a 38 a dad ei 38 mls S RRALIChCRPR M epe g Phebe reden done dds 38 CES tp 38 cia RU CRER RM M E ECRRPQ GE 38 Lr a ta 8 e A ae mS OER eRe Laem ees 8 SUMP 8 SML AAA 8 ES id idee 38 A cm 8 JA CT 8 NDAB ANG wigs aire rgennenbisekrASnrue n eR 41 Nd ratqon o dece uu CEA Es 39 Nelemtype iii eren ueri esu qug 40 everything Loose nre e iia 44 NA Ge ug i a fictePriue 41 Moral a o denne hoe ed 41 Xfresh inoiinsieD ENIM MER idas 39 Winvaridnt fOor 6 2154 lb beber 40 Niscinitiala lt 1 ge peii i eoe acd o tias 40 NDE c E 40 NILDIDOS aeneis rra e a 40 NILOGESSES u iiis Le tail 40 NLOCkSet icicdsex 9k a 4 we PIDE Ga X iE 41 Mockset membership oooooocooooocoooo 40 M AX ci id 41 A xd eae eie dt 41 NXnonnullelements lesse 39 pot modified asada a aa 39 A a eU EP pua 44 Num OEY ch ccs mad eus ERI OY eb ee Une E 41 po n P re 39 Nod sb uuu hie at eae dece eae 64 Nprod ct oin e incl arp ed oasis 41 Nreachis ilicis iege we tne i Tip eii Canada eru 39 Aralar da io 41 NEO ia ee rer cmrSlc d Dns 39 NSpaCOw tein rnieor Pe Ote e bene POTIS 39 ASUS a hacen earn a 41 NEVBG copi aldea bi 40 ATIPE S
67. eir illegal use within the implementation of a Java routine 3 6 5 Model class and model interface declarations e Description A model type class or interface declaration is a conventional type dec laration modified by the JML keyword model and in an annotation comment The entire declaration must be within one annotation comment The model type may be used within annotation expressions and statements Model types may have the same modifiers as top level and nested java type declarations as appropriate see Appendix A e Status Implemented e Differences from JML or Java Model types are in the same name space as conventional Java types Thus in some cases the resolution of a type name in Java code could resolve to a model type name rather than to the correct Java type This is a bug in the name scoping of both JML and ESC Java2 the workaround is to rename the model type so that it does not hide a Java type name 3 6 6 Java initializer blocks e Description Java permits blocks of code within braces in the body of a class but not interface declaration In the process of loading a class each initializer of a static field and each initializer code block with a static modifier is executed in textual se quential order Similarly when an instance of a class is created each initializer of a non static field and each non static initializer block is executed in textual sequential order Each initializer block may be preceded by a specif
68. ences from JML or Java bugs 3 9 12 callable Description description description needed The list of locations in the clause may also contain the special keywords nothing everything Any expressions e g array indices are evaluated in the pre state COmment on not specified Status status status unknown Differences from JML or Java bugs 3 9 13 measured by Description description Description needed The expression in the clause may also be Nnot specified which is equivalent to omitting the clause What is the type of the expression Status Parsed and ignored Differences from JML or Java bugs 3 9 14 Redundancy Description Many clauses have a redundant form indicated by using a keyword with a redundantly suffix The intention of these clauses is to indicate specifications that are implied by other nonredundant specifications The writer may choose to include the redundant specifications in order to point out some non obvious implications of other specifications either to facilitate understanding by the reader or to assist the prover in verifying conclusions Note that the implies that and for example specifications are additional forms of redundancy Status Currently in ESC Java2 a command line option selects between using re dundant specifications those with keywords ending in _redundantly in the same way as nonredundant specifications the default or
69. entifier Expression The enclosing parentheses are required the middle item is an unquoted identifier that has no relationship to any other identifiers elsewhere in the program The result of the expression is the value of the expression that is within the expression this expression must be a boolean expression The effect of the operation is as follows If the static checker would issue a warning that some condition does not hold and the relevant expression contains a lblneg or a lblpos construct and the expression within the construct evaluates to false for Iblneg or true for lblpos then the identifier in the construct is listed as a label encountered in the counterexample context This may be useful to the user in identifying which portion of an expression is causing some condition to hold or not to hold e lockset This value has type LockSet The value is the set of objects whose locks are held by the current thread Status This feature is fully implemented by ESC Java2 as inherited from ESC Java e membership in a Mockset A lockset contains objects Membership in a lockset is tested using this syntax for some object expression o lockset o This expression Chapter 3 Status of JML features 41 returns a boolean which is true if the object is in the lockset Status This feature is fully implemented by ESC Java2 as inherited from ESC Java It is not part of JML but should be There should be a way to get the
70. er no spec given default is requires true public void m F class Derived extends Super also 0 requires P 0 ensures Q public void m the two classes behave as if they had these specifications class Super requires true public void m class Derived extends Super 1 also requires true ensures P gt Q public void m Chapter 3 Status of JML features 53 Finally given class Super no spec given default is requires true public void m class Derived extends Super 1 no spec given default is requires false public void m the two classes behave as if they had these specifications class Super 0 requires true public void m class Derived extends Super 1 also 0 requires true public void m What does jmlrac do with this issue 3 19 13 3 Inheritance and non_null The syntactic rules and semantic meaning of non_null on formal parameters in the presence of inheritance differ between ESC Java and ESC Java2 A non nu11 annotation on a formal parameter is equivalent to a a requirement that the parameter not be assigned a null value in the body of the implementation of the routine and b an additional precondition in each of the specification cases of the method s or constructor s specifications Item b means that specifications public void m non_null Object o Object oo is equiva
71. erRuby02 G T Leavens A L Baker C Ruby Preliminary Design of JML A Be havioral Interface Specification Language for Java Iowa State University Department of Computer Science TR 98 06t December 2002 Available from ftp ftp cs iastate edu pub techreports TR98 06 TR ps gz Leavens etal03 G T Leavens E Poll C Clifton Y Cheon C Ruby D R Cok J Kiniry JML Reference Manual Available from http www jmlspecs org Appendix A Concept Index Concept Index The index needs a lot of work PP 41 TL 41 Ms as ace Ses IER QOL TE I 8 bootclasspatli z micos 59 Cs ias Steps Fh aoe hats 59 classpatbh ica 59 da da dando delata 59 zo 60 disableassertions sese cess ee eee 60 HCA ERE P npe ade ERRAT AREE CERE Eg Rp 60 HOA AV Ale ii el uie duae RU ds 60 eagjml ss ais abba ad cee sie aw wg adco NEP E 60 enableassertions sees eene 60 Mm 60 uU C 60 SUD si ecc pP rud Eae EE E dub ee dos gre abe 60 zl pp 60 javaAssertions eese eed bet rr FER rt 60 jmlAssertions eere tet eR RR ere 60 A vel p aa i RI iri ap RAT 60 STOOPS EET 60 neverBinary i ere Rb A 60 neyerSOUFCe uos nb xp pice ib ob 60 NOCAULIONS e gt ioges ciu er Erde dde rede 60 nocheck ouvir dani eds 60 STIOWALED 24420 a e Rd oe aa 60 Packages tonta c wor he ur EFE RAM es 60 aparseP lS wien ieu IER a 60 prefer Binary fui civ t cess EP RISE ERES 60 4preferRecentz sce s
72. erclasses e Status Parsed and fully implemented e Differences from JML or Java None e Comment A method inherits purity from the methods it overrides that is if an overridden method is pure the overriding method will be pure whether or not it is declared pure This is not the case for classes or for interfaces A subclass may add non pure methods even if it has a pure superclass Declaring a class pure is precisely equivalent to declaring all of its methods and constructors pure Verify with JML 3 5 2 model JML e Description The model modifier indicates that the class or interface is only to be used in annotations It is not part of the Java program e Status Parsed and fully implemented e Differences from JML or Java JML does not yet properly handle model classes espe cially those at the top level Both JML and ESC Java2 parse model types as if they were Java types and so will not detected erroneous uses of model types in Java code both tools may also have some related name lookup bugs 3 5 3 weakly JML e Description This annotation is used to modify super classes and super interfaces in a class or interface declaration An example of its syntax is this Chapter 3 Status of JML features 15 public class A extends B weakly implements C weakly D weakly Need a description of the semantics e Status Parsed and ignored by ESC Java2 e Differences from JML or Java Pars
73. ertions e enableassertions as in Java causes parsing to read Java 1 4 source and to use Java assert statements e f filename the text within the named file is inserted at that location in the command line this option is typically used to insert standard sets of options or input elements into the command line e file filename the file given is one of the input elements upon which the program will act e gui this must be the first command line argument it causes the GUI version of ESC Java2 to start e help causes the program to print information about command line options and then to terminate e javaAssertions causes parsing to read Java 1 4 source and to treat Java assert statements as Java does as a throw of a java lang AssertionError exception e jmlAssertions causes parsing to read Java 1 4 source and to treat Java assert statements like JML assert statements e list filename the given file must contain a sequence of input entries one per line the option can be used to include a standard set of files directories packages or classes see also e loop n 0 5 ESC Java analyzes loops by unrolling them The argument of the option specifies the number of times the loop is unrolled The default is 1 5 The precise meaning of the argument including the inclusion of the 5 is described in the ESC Java User s Manual e neverBinary do not use any class files even if there is no java file for a type e
74. es from JML or Java ESC Java also allows a readable_if and writable_ if modifier for field declarations each taking simply a predicate and are positioned just prior to the field declaration as for example a non_null modifier would be readable_if is deprecated in JML and writable_if is not defined at all Hence these forms are discouraged in ESC Java2 as well 3 7 7 monitors_for e Description This clause associates a list of expressions with a given field name The field identified must be a field of the class containing the declaration All of the ex pressions must evaluate to objects not to primitive values If the field is static all of the objects must be static The effect is to associate the expression values as monitors for the given object e Status Implemented Should a list of ids be allowed Should syntax such as this T for classname T be allowed Is a static modifier allowed e Differences from JML or Java None Chapter 3 Status of JML features 21 3 8 Annotations for a method or constructor Specifications of the behavior of an individual method or constructor typically appear within an annotation comment just prior to the declaration of the method or construc tor The specifications consist of zero or more lightweight or heavyweight behavior sections an optional code_contract section an optional implies_that section and an optional for_example section Model methods and constructors
75. ethod and constructor to help disambiguate such situations These are used in ghost field and model field method and constructor declarations Are they applicable to non model decls in JML Are they needed with model type declarations or model programs 7 They have the effect that any identifiers appearing after these keywords in a JML annotation are not interpreted as JML keywords except for non null in formal parameters as described below For example in 0 public model non null helper method requires ensures model non null helper and method are JML keywords but requires is ex pected to be a Java type name and ensures is interpreted as an identifier the name of the method being declared The one exception to this rule is that non null is needed as a JML modifier within the formal parameter declarations A parser is capable of distinguishing these cases however Thus in public model requires ensures non null Object o non null oo the first occurrence of non null is a JML modifier but the second is expected to be a Java type name ESC Java treats non null specially in this case but the JML tools do not For JML you cannot use non null here and need to write explicit pre post conditions instead Status Fully implemented 3 19 11 Equivalence of NTYPE and java lang Class In Java the types of classes can be treated as first class values of type java lang Class In JML the type NTYPE has been
76. f all static checking The following list of the warning types is excerpted except where additions are explicitly noted and quoted from the ESC Java User s Manual The additional warning pseudo type name All may be used with the nowarn command line option to turn off all warnings warn may then be used to selectively turn on individual warning types The All type may not be used with warn e ArrayStore warns that the control may reach an assignment A I E when the value of E 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 E is false e Cast warns that control may reach a cast T E when the value of E cannot be cast to the type E e Constraint warns that a method does not establish the post condition stated in a constraint clause added in ESC Java2 e Deadlock warns that control may reach a synchronized statement that would acquire a lock in violation of the locking order or that a synchronized method may start by acquiring a lock in violation of the locking order e 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 e IndexNegative warns that control may reach an array access A I when the value of the index I is negative e IndexTooBig warns that control may reach an array access A I when A length lt I e Initially warns
77. f static checking There are lots find out by experiment Chapter 6 Incompatibilities 68 6 4 Incompatibilities with ESC Java This section describes ESC Java features that are not present or behave differently in ESC Java2 the many additions to ESC Java provided by ESC Java2 are not discussed 6 4 1 Error messages and warnings ESC Java2 has added error messages to conform with current JML semantics Some old ESC Java errors and warnings are no longer appropriate and have been removed The overall organization of error messages and warnings is unchanged see Section 4 1 Error and warning messages page 57 6 4 2 also The keywords also_requires also_ensures also_exsures and also_modifies are no longer supported Use also and note the change in semantics as described in Section 3 19 7 Original also specifications page 47 6 4 3 inheritance of specifications The combining of specifications of overridden and overriding methods to create a composite specification has been revised to match the semantics specified for JML as described in Section 3 19 13 Specifications and inheritance page 49 6 4 4 non_null on formal parameters and results of routines The rules and meaning of non null in the presence of inheritance is altered as described in Section 3 19 13 3 Inheritance and non null page 53 6 4 5 monitored by ESC Java2 agrees with ESC Java in the implementation of monitored by However this keyword is deprecat
78. fault constructor Within the body of a constructor any super class initially clauses are assumed to hold after the execution of a non helper super call including a possible implied call of the default superclass constructor A class does not inherit any superclass initially clauses initially clauses are not permitted in interfaces If the clause is declared static it may only reference static fields and routines e Status Implemented Initially clauses are typechecked as additional postconditions on every constructor of a class Failures provoke an Initially warning e Differences from JML or Java None Actually TBD JML has not clarified the semantics of initially clauses such as whether they are inherited and whether they can be present in interfaces 3 7 6 readable and writable e Description JML allows class level clauses of the form readable field if predicate and writable field if predicate These specify a predicate that must be true in the state in which a read or write access of a class field is attempted These are useful to specify the access protocol for a variable shared across threads but can also be used simply to indicate under what circumstances a field s value is defined e Status Implemented However the semantics is not well defined for the situation in which the field referred to in the clause is declared in a super class of the class declaration containing the clause e Differenc
79. fies modifiable assignable modifies redundantly modifiable redundantly assignable redundantly 26 3 9 7 diverges diverges redundantly 0 00 20 e eee eens 28 0 0 8 WHEN cios stets Ded DR dak oiled atid RR eU wate eee ee 28 2 0 9 o A deett Red ba ut RUE are scd 28 3 9 10 working space seeeeeeee mmm 28 9 9 11 accessible ds ces ek Eod Maka ER Red ene e eda 29 2 9 12 cala Ple a eee dodo A RS RU Ba E ede t eet 29 3 9 13 measured by 0 cece cece eee ren 29 3 9 14 Redundancy oiii ere ete eee ot leds 29 3 10 Annotation modifiers for a method or constructor 30 3401 PIN pe p m 30 3 10 2 non null JML methods only 22 eorr nts 30 3 10 3 helper JME o3 eod dete ceed co Eo et e Nui RO ER hd 30 S104 imal Java methods only scort de o1 3 10 5 static Java methods only ooooooooocoommmo 31 3 10 6 synchronized Java methods only 31 3 10 7 native Java methods only ooooooooooooooo 31 3 10 8 strictfp Java methods only 0ooooooooooomo o 32 3 11 Annotation assertions for a field declaration 32 A pie RON 32 3112 maps to JMD paca 32 3 12 Annotation modifiers for a field declaration 32 SISTI nomnal JML cava coro poeta pae rh os hc ln peores 33 5 12 2 m nitor d JMD atu tities wade ad 33 21223 tame Chava carrier E rRER RR Eh ERE eek abs 33 3124 Volatile Java es iva la odas
80. g a b c a sample b new String sample c b intern t a b This is NOT true t a c This IS true Interning is not yet implemented in ESC Java2 5 5 The TYPE and java lang Class types In JML and ESC Java2 uses of NTYPE values and java lang Class values are interchange able with the exception in ESC Java2 that methods of class java lang Class cannot be applied to a NTYPE value 5 6 The initially clause JML defines an initially annotation that states a predicate which must be true of an object after any constructor call This is implemented in ESC Java2 by adding these assertions as additional postconditions on each non helper constructor 5 7 The constraint clause JML defines a constraint annotation that states a predicate which must be true of an object after any method call This is implemented in ESC Java2 by adding constraints as additional postconditions on each non helper method Chapter 5 Changes to static checking in ESC Java2 65 5 8 Use of modifies clauses in checking routine bodies Fix this we now do check modifies clauses ESC Java2 mitigates problems caused by errors in modifies clauses by maintaining pre state values for any variable mentioned in an old construct in addition to those in modifies clauses As a result the static checking of the routine body proceeds correctly despite any errors in the modifies clauses 5 9 Defaults for modifies clauses ESC Jav
81. he text may well have meant the former It is better to avoid embedded annotations if this confusion may arise e parsePlus option The parsePlus command line option instructs ESC Java2 to parse all annotations recognized by JML particularly including the and annotation markers This is used mainly in testing to find and attempt to process the JML only annotations but may be useful in other circumstances See parsePlus page 60 e Initial symbols in annotations Within a multi line annotation a sequence of symbols that follow whitespace at the beginning of a line are treated as white space Within an annotation embedded in a Javadoc comment a sequence of symbols but not 0 symbols that follow whitespace at the beginning of a line are treated as white space e Splitting annotations across comments JML tools will parse and process annotations that are split across multiple comments e g a multi line annotation in which each line begins with ESC Java2 expects an annotation to be entirely contained within one single or multi line comment The latter behavior is correct JML however the JML tools will correctly process and not warn about annotations split across multiple comments To be specific e ESC Java2 requires that any clause beginning with a keyword e g invariant requires and ending with a semicolon must be contained within one annotation comment For example write 0 requires
82. he value of the formal parameter since it may have been called through the super class s signature and hence line C fails similarly there is no limitation on what may be assigned to the formal parameter variable so line D is ok Finally line E is ok since there is no additional precondition created by the ignored non null Note that behavior equivalent to the non nu11 declaration on a formal parameter can be obtained by adding appropriate explicit preconditions requiring the formal param eter to be non null in the appropriate circumstances Furthermore if it is actually desired to have the formal parameter be non null within the body code such as the following can be written Instead of public void m non null Object o 1 write public void m Object oo non null Object o oo Finally note that e the original ESC Java does not allow overriding methods to have non_null parameters whether or not the overridden method does e there are no particular issues with respect to non null on the result type overriding and overridden methods may have any combination of non null annotations or lack thereof What does jmlrac do with the inheritance of non null Chapter 4 ESC Java2 features 57 4 ESC Java2 features This chapter describes some of the user interface features and usage of ESC Java2 A description of how to run ESC Java2 is provided in Chapter 2 Running ESCJava2 page 4 4 1 Error and
83. i 0 amp amp j 0 or requires i 0 amp amp j 0 not Chapter 3 Status of JML features 10 requires i 0 amp amp j 0 e ESC Java2 requires that model methods model constructors and model programs be defined within one annotation comment For example write public model int m int i int j return i j not public 0 model int m int i int j return i j e The tool also requires that a Java modifier e g public be in the same comment as a JML annotation e g behavior or model method that it modifies For example write public behavior not public 0 behavior e Finally any in or maps clauses following a ghost or model field declaration must be within the same annotation comment as the declaration Thus write 0 model T t in a not model T t 0 in a Thus requires and ensures clauses must each be wholly within a single annotation comment individual keywords such as pure normal_behavior also or implies_ that may be in annotation comments by themselves with any relevant access modi fiers FIXME JML rules need to be clarified e Multiple annotations per comment It is legal JML to include multiple annotations per comment in fact it is common practice and good style to include many related annotations within one multi line comment ESC Java2 supports this practice though ESC Java had some difficulties e
84. i 5 doe Oh ias ld idos 41 Appendix A Concept Index NEYPEOL nerse hosa dans accessible o ooooooooooooooo also_ensures o ooooooocoorooooooo also exsures oooooooooomomooo also modifies oooooooooo o also require8 ereere tosis err eee eee annotation markers Lus ASSOLE ia dre dad assignable s secs rr ars assignable redundantly C callable 2 dtt enai ETE CAUTIONS coco hich eer iaa RET classpath eiria eE EE is clause defaultsS o ooooooo comments annotation CONSA ins D defaults arras lio se diverges ice ie br er das aa RR QE diverges redundantly GUT AION core eser TP oin E error messages eee eee ESC Java sru eet PI Rud tread GXSUT S so lscce ee bane Mea Xm RARE exsures redundantly F fatal GFfOES s seus b LIRE RS file AMES cuicos filenames ills ocuisa cr eee ans final routin pora len for_example o oooooooooooo format of annotations I implies thats catas cana informal predicate o o o o oo inheritance of specifications initially taa aegis eh eee W WAITING S a aware sd does S Where a working space lesser 78 J J va MD ete ei epui Ear EEEE a 67 Mia iria 2 O cassie mb aula deste tase es arise ye Sua cabo Reed ang 2 M Mocha ia bebdkedeanescd 2 model program statements 4
85. ication just like a method specification The preconditions and postconditions specified must hold just before and just after the execution of the initializer block Note that no invariants or other class level specifications are required to hold until all static initialization and class loading is complete for static invariants or until a constructor has completed execution for instance invariants e Status Most specifications are parsed but not all and no reasoning is implemented e Differences from JML or Java Chapter 3 Status of JML features 18 3 6 7 initializer Description The JML initializer and static_initializer keywords are used in specification files as stand ins for all of the instance and class initialization that is per formed as part of object creation or class loading Within a class declaration in a com pilation unit there may be just one each of the initializer and static_initializer keywords each preceded by specifications like those preceding a routine declaration or a Java initialization block If more than one compilation unit of a refinement se quence has these keywords then the associated specifications are combined just like routine specifications are combined The composite specifications associated with an initializer keyword give preconditions that must hold before any instance initial ization and postconditions that must hold after any instance initialization but before constructors are executed Si
86. ics is performed Note that the Java Language Specification stipulates that construc tors may be strictfp only by virtue of the entire class being declared strictfp e Differences from JML or Java None 3 11 Annotation assertions for a field declaration A field declaration including ghost and model field declarations may be followed by field assertions which are introduced by the in and maps keywords These declarations associate a field or its sub fields with specific datagroups which can then be used as items in a modifies clause Which fields may have datagroups associated with them 3 11 1 in JML e Description This assertion follows a field declaration and lists the datagroups of which the field is a part A field is automatically a part of the datagroup with the same name as itself e Status Implemented e Differences from JML or Java None 3 11 2 maps into JML e Description Comment needed e Status Parsed typechecked and static checked using a limited unrolling of any recur sive definitions e Differences from JML or Java Comment needed COmment on the unrolling of recursive mappings Potential performance improvement unroll datagroups wildcard refs only when needed Perhaps have to do this to verify superclasses Comment on non support for wild cards and array ranges in the middle of spec ref expressions 3 12 Annotation modifiers for a field declaration
87. ignoring them when the option noredundancy is chosen Chapter 3 Status of JML features 30 3 10 Annotation modifiers for a method or constructor Annotation modifiers can appear between the last specification clause or javadoc comment and the type designator or class name that is part of the method or constructor JML modifiers and Java modifiers may appear in any order Though less common and not the usual style and discouraged ESC Java2 following ESC Java allows JML modifiers to appear after the method declaration and before the opening left brace of the body or the terminating semicolon if there is no body Besides the modifiers listed here methods and constructors may also have the access modifiers described in Section 3 4 Access modifiers page 13 3 10 1 pure JML e Description The pure modifier applied to a method indicates that the method does not assign to any non local memory location during its execution it may not even modify and then restore the original value It is equivalent to having modifies nothing in the specification In the case of a constructor the only fields that may be modified are at most the fields of the object itself which are initialized as a result of the action of the constructor In this case the pure modifier is equivalent to specifications of the form modifies this However a constructor may have modifies clauses that are more restrictive than modifies this Note that if a metho
88. ions that the pre and post states must satisfy the behavior is specified by a model program which specifies the behavior using typical imperative programming constructs However a model program allows some non deterministic and non executable constructs as well Note that there are a num ber of JML constructs which are only used within model programs These are described in Section 3 18 Statements within model programs page 44 e Status Model programs are parsed and ignored They are permitted as a specification case as defined by JML Any constructs unique to model programs are simply skipped over by the parser e Differences from JML or Java None 3 8 4 code_contract Needs discussion also accessible callable captures measured_by clauses 3 8 5 implies_that e Description The implies_that keyword introduces specification cases that are logi cal consequences of the usual behavior and lightweight specifications They could be used as specifications to be checked in the same way that the other specifications are Alternatively it could be verified that they are logical consequences of the other spec ifications the results could then be used as additional useful statements of behavior these in turn could help with proofs involving use of the method or constructor with which the implies_that specification is associated e Status The specifications in an implies that section are parsed and typechecked but
89. is is not applicable to a ghost or model declaration e Status Parsed but ignored by the static checker Any implications of this modifier would be part of the specifications of serialization for the object e Differences from JML or Java None 3 12 6 static Java e Description static is a Java modifier which may be used on JML ghost and model field declarations as well that indicates that the declaration in question is a member of the class and not of each instance of the class e Status Fully implemented e Differences from JML or Java None 3 12 7 instance JML e Description instance is a JML modifier that indicates the opposite of static that is that the field in question is a member of each instance of the object not just of the class Within a class declaration field declarations are non static by default and instance is not needed However within an interface Java field declarations are static and final by default Ghost and model field declarations are static by default but not final The instance modifier may be applied to ghost or model field declarations in an interface making those fields non static JML allows the modifier instance only on ghost and model field declarations in either classes or interfaces As in Java ghost and model declarations in a public interface are implicitly public e Status Implemented e Differences from JML or Java CHeck that illformed JML uses are checked and forbi
90. is not equal to nor a subtype of the type of any reference or primitive type Status Implemented Differences JML allows arguments of primitive types ESC Java2 does also but the original ESC Java did not e elemtype This function takes an argument of type TYPE and returns a value of type TYPE If the argument is an array type then the result is the dynamic most specific type of the elements of the array if the argument is not an array type the result is unspecified Status Implemented The results of applying elemtype to any non array type all test equal This should perhaps not be so Check what the behavior actually is Perhaps should define the result e type This is a syntactic construct used to denote type literals It denotes the type constant of value TYPE corresponding to the type name given as the argument Status Implemented Differences None e is_initialized This construct takes a type name as its argument It returns true just in the case that the type named has completed its static initialization Status Parsed and partly typechecked No static checking is implemented e invariant_for This function takes one object of reference type as its argument and returns a boolean The result is true just when the object satisfies its class invariants Status Parsed and partly typechecked No static checking is implemented e lblneg lblpos These syntactic constructs have the unusual form lblpos Id
91. laration Constructor declaration Model method Model constructor Java Initialization block JML initializer and static_initializer annotation Formal parameter public protected private final volatile transient static public protected private static final public protected private static public protected private abstract final static synchronized native strictfp public protected private public protected private abstract static final synchronized strictfp public protected private static 22 final 74 spec_public spec_protected non_null instance monitored non_null instance monitored non_null instance spec_public spec_protected pure non_null helper spec_public spec_protected helper pure pure non_null helper pure helper 22 22 non_null Appendix A Modifier Summary 75 Local variable and local ghost variable final ghost non_null declaration uninitialized Note that within interfaces fields are implicitly public static and final Ghost and model fields are implicitly public and static though they may be declared instance i e not static Appendix A Bibliography 76 Bibliography Flanagan etal02 C Flanagan K R M Leino M Lillibridge G Nelson J B Saxe R Stata Extended Static Checking for Java Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation June 2002 LeavensBak
92. led information on JML is available at the web site http www jmlspecs org A the details of the JML definition are published in Preliminary Design of JML LeavensBakerRuby02 and in The JML Reference Manual Leavens etal03 both available from the JML website e Information on the original ESC Java tool most of which still applies is provided in ESC Java User s Manual SRC Technical note 2000 002 Leino Nelson Saxe available at gatekeeper dec com pub DEC SRC technical notes SRC 2000 002 html 1 2 Acknowledgements To date the work on ESC Java2 has been carried out primarily by David Cok and Joe Kiniry Gary Leavens has provided guidance on the semantics and the current and fu ture state of JML K Rustan M Leino has provided advice with respect to the original ESC Java The website for the project through version 2 0a8 was hosted by the Security of Systems group at the Radboud University Nijmegen what used to be known as Katholieke Universiteit Nijmegen or the University of Nijmegen in Nijmegen Netherlands Chapter 1 Introduction 2 http www niii kun nl sos research escjava The project is now hosted by the KindSoftware Research Group in the Department of Computer Science at University College Dublin from version 2 0a8 onward http secure ucd ie The work of producing ESC Java2 stands on the very much more considerable effort of the ESC Java team in conceiving of and producing ESC Java Simplify and related tools
93. lement any of the new features in Java 1 5 6 1 2 anonymous and block level classes These are supported but the bodies of methods are not checked See Section 3 19 8 anony mous classes page 47 and Section 3 19 9 block level class declarations page 47 6 1 3 serialization discussion needed 6 1 4 most multi threading considerations discussion needed 6 1 5 Java generics Support for generic typing in Java or any other features of Java 1 5 is not implemented in ESC Java2 6 2 Major features of JML not implemented in ESC Java2 6 2 1 code_contract clauses discussion needed 6 2 2 some aspects of store ref expressions discussion needed 6 2 3 implies_that and for_example behavior These sections of a routine s specification provide specifications that are implied by the regular specifications They are parsed and typechecked but no use of them is made in static checking they are not used as an aid to reasoning nor is it checked that they follow from the other specifications 6 2 4 splitting of annotations across comments JML technically does not permit annotations to be split across comments though there is no definition of an unsplittable unit of an annotation In practice the JML tools allow some splitting and ESC Java2 allows some splitting but they are not consistent See Section 3 2 Format of annotations page 8 When in doubt use a multi line comment 6 3 Limitations o
94. lent to requires o null 41 specifications Similarly a non_null annotation on the result is equivalent to an additional post condition specifications public non null Object m is equivalent to ensures o null l Specifications Chapter 3 Status of JML features 54 This syntax is not legal JML since an ensures may not appear outside of the nested specifications but the intent is evident the ensures clause is distributed to each specification case Confusing situations can arise if formal parameters in a overridden and overiding decla ration differ in non_null annotations e Case 1 Super class has non_null subclass has a spec but no non_null class Super public void nonnull non null Object o public void m non null Object o 4 nonnull o Line A OK o null Line B FAILS 3 class Derived extends Super 1 0 also requires true public void m Object o 1 nonnull o Line C FAILS o null Line D OK public void mm Object o m o Line E OK new SO mCo Line F FAILS In this case ESC Java has Derived m inherit the non null specification from the over ridden method Hence ESC Java reports errors for lines B D E and F with A and C being OK In ESC Java2 however Derived m has its own specification and does not inherit the non null specification It must still satisfy the pa
95. lockset of a thread other than the current thread max This function takes an argument of type NLockSet It returns an object of type java lang Object The result is one of the elements of the argument the function satisfies the following for any LockSet s and Object o s o gt o lt max s Status This feature is fully implemented by ESC Java2 as inherited from ESC Java Operators for overflow checking These are under development in JML and are not yet implemented in ESC Java2 informal predicate An informal predicate consists of text enclosed within the delim iters and Informal predicates are interpreted as boolean expressions that are always true independent of what the text may say and they may only be used in contexts where a boolean expression is allowed Status This feature is fully implemented in ESC Java2 as well as ESC Java 3 16 3 New JML types JML adds some new types that may be used as type names in declarations of variables within annotations e TYPE This is a JML type name used to denote the type of type designations For example typeof and type produce results of type TYPE and the lt operator takes arguments of type TYPE Values of type TYPE can also be compared using the or operators Status This is fully implemented In JML TYPE and java lang Class are now equivalent This is not yet the case in ESC Java2 bigint This is a new type name used in JML
96. me of these have been added to those available in ESC Java or had their behavior altered Note that in ESC Java all command line options and their arguments must precede all file names ESC Java2 allows file names and other input entries to be intermixed with options e bootclasspath directory path specifies the location of system binary files this di rectory path is appended to any specification for the classpath in finding class files the default is the platform dependent classpath specified by Java preferences using the v option will show the full classpath being used e class fully qualified class name the named class will be one of the input entries upon which the program acts e classpath directory path specifies the directories in which binary class files for types are sought the default is to use the value of the CLASSPATH environment variable or to use just the current directory if neither classpath nor CLASSPATH is specified What about java property Chapter 4 ESC Java2 features 60 e da synonym for disableassertions e dir directory providing a directory as an input entry is equivalent to but much shorted and more robust than listing all JML relevant files within that directory e disableassertions as in Java causes parsing to read Java 1 4 source but ignores any Java assert statements e ea synonym for enableassertions e eajava synonym for javaAssertions e eajml synonym for jmlAss
97. milarly the specifications of a static_initializer key word hold before and after the static initialization of the class Note that these are different than the specifications for a Java initializer block which apply only to that block Status Not yet parsed or implemented in static checking Differences from JML or Java None What access modifiers are allowed and used 22211 3 6 8 static_initializer Description See the description above Status Not yet parsed or implemented in the static checker Differences from JML or Java None What access modifiers are allowed and used 27211 3 6 9 Java method constructor and field declarations Description These declarations are identical to those defined by Java An implemen tation or initialization for such a declaration may appear only in the java file not in any repeated declaration in a specification file The modifiers allowed are listed in Appendix A Status Parsed and typechecked fully Java fields may be used in annotations JML and ESC Java2 also allow pure methods and pure constructors to be used in annotations Differences from JML or Java None 3 6 10 Nested Java type declarations Description Java allows declarations of classes and interfaces within a class or interface These are called nested classes or interfaces Inner classes or interfaces are nested classes or interfaces that are not static The modifiers allowed are listed in Appendix A Status Im
98. neverSource do not use any java files even if there is no class file for a type e noCautions suppresses the reporting of any cautions e nocheck will not execute the static checking phase though does all the parsing typechecking and verification condition generation e nowarn warning type turns off the reporting of warnings of the given type use a warning type of All to turn off all warnings e package package name includes all the source files in the given package in the list of source files being processed wihch suffixes e parsePlus causes ESC Java2 to process annotations following the markers and see Section 3 2 Format of annotations page 8 e preferBinary if both java and class files exist on the source and classpath for a type then always use the class file Chapter 4 ESC Java2 features 61 preferRecent if both java and class files exist on the source and classpath for a type then always use the one with the most recent modification time preferSource if both java and class files exist on the source and classpath for a type then always use the java file quiet turns off any informational messages leaving only reports of errors warnings and cautions simplify filename used to specify the Simplify executable that should be used by ESC Java2 The executable chosen must be the appropriate one for the platform on which you are running source version interprets the sour
99. nnotations may appear anywhere a declaration within a class or interface may ap pear They define specification only ghost or model fields of the type and state specifications that apply to the whole object not just to individual methods 3 6 1 Ghost fields e Description A ghost field is a field of the object that can hold a primitive value or a reference to an object but is used only in specifications Its value is changed using Chapter 3 Status of JML features 16 the set annotation within the body of a method or constructor see Section 3 14 3 set page 36 A ghost field may have an initializer just as a Java program field may but the ghost field may be initialized in only one compilation unit of a refinement sequence A ghost field may have modifiers that a Java field declaration would have namely access modifiers see Section 3 4 Access modifiers page 13 static final but not volatile transient as well as the JML modifiers non null monitored and instance see Section 3 12 Field Annotation modifiers page 32 An interface may also declare ghost fields these fields may be referenced by annotations in the interface or its subtypes Such ghost fields are by default static but may be modified by the JML modifier instance in which case they are a field of every object that implements the interface e Status Ghost fields are completely supported e Differences from JML or Java None Check that modifiers work
100. nvariants or constraints in either its pre state or its post state The method or constructor is still expected to satisfy any specifications e g ensures clauses that are explicitly associated with this method or constructor Status Parsed typechecked and supported by the static checker Differences from JML or Java JML only allows private methods and constructors to be helpers ESC Java2 also allows any constructors final methods or methods of final classes to be helpers ESC Java2 s rule is that only routines that cannot be overridden may be helpers It seems constructors and methods labelled helper are not checked at all and are inlined when used elsewhere Rather they should be checked against their own pre and post conditions but not against invariants constraints initiallys COmment on inlining and resulting differecnes in checking 3 10 4 final Java methods only Description This Java modifier indicates that a method may not be overridden It may also be applied to model methods Status Fully implemented This feature does not affect the static checking it simply produces a typechecking error if a final method is overridden Differences from JML or Java None 3 10 5 static Java methods only Description static is a Java modifier which may be used on JML annotations as well that indicates that the declaration in question is a member only of the class and not of each instance of the class
101. o quantities declared with the static type of the anonymous type those specifications are not used in checking any uses of the routines of the anonymous class ESC Java2 does recognize that the anonymous class is a subclass and not the same class as its super class Status There is no static checking of the implementation of any of the methods of an anonymous class 3 19 9 block level class declarations Java allows classes to be declared as local classes within a block statement These constructs are parsed and type checked However Chapter 3 Status of JML features 48 e Although such a class and its routines may have annotations the body of the imple mentation of these routines are not checked against the specifications e Any specifications are used when the methods of the class are called what about model classes 3 19 10 field method and constructor keywords JML is designed to work with any Java code In particular that code may use JML keywords as variables and type names This can create a problem in parsing annotations For example if helper has been declared a class then an annotation that begins with helper model could be interpreted as the beginning of a declaration with type helper and identifier model or as the beginning of a model method declaration with JML modifier helper Though in some cases sufficient lookahead could distinguish these different uses JML has defined the keywords field m
102. o the also or marking the end of the specification case containing the forall declaration or until end of the behavior implies that or for example section No initializer is allowed The clause is desugared by wrapping each desugared clause that is in scope in an appropriate forall expression e Status Fully implemented However the semantics need clarifying and the static checker objects to quantified expressions e Differences from JML or Java None 3 9 2 old e Description The old declaration is used within a routine specification to define a value that may be used in subsequent clauses of the specification The variable declared must be initialized The initialization expression is always evaluated in the pre state regardless of how the variable is used in subsequent clauses The scope of the variable extends from its declaration including the initializer to the also or F that marks the end of the specification case sequence containing the old declaration or until the end of the behavior implies that or for example section The uses of old variables are desugared by substituting the initialization expression wrapped in an appropriate old expression at the point of use e Status Implemented Not yet supported array initializers I don t think that ESC Java2 includes the initializer in the scope Check what the java behavior is and fix the definition here e Differences from JML or Java
103. of error messages or the occurrence of an inappropriate error message is misleading to the user Examples that generate unsound or incomplete behavior beyond that already documented are also of interest The organization of ESC Java2 s error and warning messages is described in Section 4 1 Error and warning messages page 57 3 1 File finding and refinement sequences JML follows Java conventions in file naming ESC Java2 recognizes Java source and class files organized into directory hierarchies matching the package definitions including source and class files packaged in jar files The file names themselves typically consist of a type name as a prefix and either java or class as a suffix Specification files typically have the type name as a prefix and one of the specification suffixes refines java refines spec refines jml java spec jml java refined spec refined jml refined asa suffix though arbitrary suffixes are permitted The ESC Java2 program utilizes a classpath and a sourcepath which are standard se quences of directories or jar files separated by a platform dependent path separator character a colon on Linux and MacOSX a semicolon on Windows The classpath is specified by the classpath command line option or by the CLASSPATH environment variable if no command line option is given and is just the current working directory if neither is spec ified The sourcepath is specified by the sourcepath command line
104. of the declared types must be identical including case e If a java or a class file exists for a type the specifications may not add any Java that is non model non ghost declarations to the signature They may only repeat declarations The specification files may declare specifications for a method that is not implemented in the Java implementation if a the declaration overrides a method in a super class or super interface or for interfaces a method in java lang Object and b the declaration is within an interface or is an abstract declaration in a class This enables the specification writer to write specifications for a routine in a class or interface that must be obeyed by subtypes even if the class or interface itself does not provide a new implementation The requirement that the introduced declaration be abstract is not enforced Don t think it needs to be abstract e Ifa field is redeclared it must be redeclared with the same type and the same Java modifiers An initializer of a java field may be present only in the java file An initializer of a ghost field may be declared in only one file of a refinement sequence e These JML modifiers must be consistent across all redeclarations of a field model ghost instance The modifiers spec_public spec_protected non_null and monitored may be added by a refinement file but may not be removed e Ifamethod or constructor is redeclared it must be redeclared with the same
105. of the program It may be used with the modifies accessible and callable clauses Status Fully parsed refer to the clause descriptions for specific behavior 3 18 Statements within model programs A model program consists of imperative programming statements and control structures much like a typical Java program However a model program allows some non deterministic and non Java statements as well These are described in this section Need enumeration and discussion of these 3 19 Other issues descriptions needed here Use of JMLDataGroups in modifies clauses what syntactic structures use stsore refs 11 3 19 1 universe type system JML has recently introduced a universe type system for alias control This includes type modifiers readonly rep peer These have not yet been implemented in Esc Java2 either in the parser or in the semantics 3 19 2 infinite precision arithmetic JML defines primitive data types bigint and real which denote infinite precision inte gers and reals for use in specifications These type names are parsed but the underlying semantics and the Simplify prover do not handle the finite ness of numeric representations 3 19 3 nowarn annotations ESC Java2 allows an annotation to suppress warnings otherwise produced by the static checker These are discussed in Section 4 2 Nowarn annotations and warnings page 57 JML parses but ignores these annotations Chapter 3 Sta
106. olved potential extensions to current JML Changing the order of suffixes so that either jml or spec comes before java Allow modifies clauses outside of pairs the clause would be distributed across the nested specifications just like requires is Allow specifications on statements within a body of a routine Definite definition of elemtype applied to a non array Appendix A Modifier Summary Appendix A Modifier Summary 73 This table summarizes which Java and JML modifiers may be used in various grammatical contexts Grammatical construct All modifiers Class declaration Interface declaration Nested Class declaration Nested interface declaration Local Class and local model class declaration Type specification e g invariant Java modifiers public protected private abstract static final synchronized transient volatile native strictfp public final abstract strictfp public strictfp public protected private static final abstract strictfp public protected private static strictfp final abstract strictfp public protected private static JML modifiers spec_public spec_protected model ghost pure instance helper non_null pure model pure model spec_public spec_protected model pure spec_public spec_protected model pure pure model Appendix A Modifier Summary Field declaration Ghost Field declaration Model Field declaration Method dec
107. oning that can be performed as a result Thus any use of the ESC Java2 tool will require having specification files for system classes and for many of the other classes in the user s body of code e The logic to reason about routine bodies that contain calls of methods that are specified with modifies everything has not yet been defined or implemented A caution is issued in these cases But to avoid breaking tests this caution is not yet turned on This needs updating when modifies everything is implemented 5 11 Checking of modifies Needs description 5 12 typeof In ESC Java the typeof operator applied only to arguments of reference type In ESC Java2 the arguments may also be primitive types and the static checker correctly Chapter 5 Changes to static checking in ESC Java2 66 equates the value with the corresponding type literal of the form type T where T is a primitive type name This does not work completely yet 5 13 Use of pure routines in annotations This is now allowed needs description 5 14 Checking of model fields Describe the static checking of model fields 5 15 not_modified The not_modified feature of JML is implemented in ESC Java2 by replacing it with the predicate x old x for each argument x Chapter 6 Incompatibilities 67 6 Incompatibilities 6 1 Major features of Java not implemented in ESC Java2 6 1 1 Java 1 5 ESC Java2 does not imp
108. pecified before the implementation is completed JML tools except jmldoc and ESC Java require bodies to be present 3 19 6 Methods and constructors in annotation expressions JML allows the use of pure methods and constructors in annotation expressions the original ESC Java did not ESC Java2 follows JML Need a discussion of the implementation of this 3 19 7 Original ESC Java also_ specifications The original ESC Java utilized the keywords also_requires also_ensures also_ exsures and also_modifies to add annotations to subclasses These annotations were simply textually conjoined with the annotations from a super class or interface The syntax and semantics in JML are different and ESC Java2 has changed to match JML These keywords are now deprecated and are translated into the corresponding keyword without also_ However the semantics of annotations in the presence of inheritance is now somewhat different and is described by the desugaring process see Desugaring page 22 ESC Java2 issues warnings if the original keywords are used and users are encouraged to change them 3 19 8 anonymous classes Java allows anonymous classes named classes with some method overrides An anonymous class is a subclass of the named class and is nested within the class in which it is defined but is not a member of the enclosing class One can add specifications to the anonymous class body and the members within it However since there are n
109. plemented Differences from JML or Java None 3 7 Annotation clauses for a class or interface These clauses provide a specification of the behavior of the class and of objects of the class They may be specified in any order within annotation comments anywhere an element of a Chapter 3 Status of JML features 19 type declaration may appear They may individually have access modifiers see Section 3 4 Access modifiers page 13 public protected or private 3 7 1 invariant invariant_redundantly e Description An invariant clause specifies a boolean condition that must hold before and after any call of a non helper method of the containing type Invariants must hold after any non helper constructor call of the containing type In checking the implementation of a method invariants are assumed as part of the preconditions and must be established as part of the postconditions An invariant clause may be declared static in which case it may only reference static fields and routines e Status Fully implemented except that ESC Java2 does not check the restriction on static invariants e Differences from JML or Java None 3 7 2 constraint constraint_redundantly e Description A constraint clause specifies a relation that must hold between the pre and post conditions of any non helper method of the containing type If the clause is declared static then all field and routine references within the constraint predicate must
110. release you will need to provide a suitable path to the escj script when you invoke it 4 Execute a non GUI version of ESC Java2 using the command java cp esctools2 jar escjava Main In this case you need to specify the location path and name of the Simplify executable using the simplify option and the location of the reference specifications using the specs option You also need to specify the classpath using classpath and any other input files and options Chapter 3 Status of JML features 5 3 Status of JML features ESC Java2 parses correctly formatted JML files with the exceptions described in this document JML files must be correct Java source with correctly formatted annotations which appear to Java as comments Although ESC Java2 does some error reporting during parsing it does not report all parsing or type errors in either Java or JML nor does it necessarily terminate normally if the input is not legal Java JML There are a number of tools supporting JML that can be used to check the well formedness of the JML annotations in a file a Java compiler can be used to check the format of the Java source code The authors encourage any report of a legal Java JML file that ESC Java2 will not parse Furthermore despite the caveat above the authors do want ESC Java2 to be a useful tool hence they are interested in examples of legal or illegal Java JML source code that cause abnormal termination and in examples in which the absence
111. rent spec which in this case simply has a trivial postcondition So Lines B and F are errors and A is not However the combined spec for Derived m is ignoring other clause types requires o null ensures true also requires true ensures true which is equivalent to requires true Thus lines D and E are OK and C will provoke an error If the precondition of Derived m were requires false then the combined spec would be requires o null Chapter 3 Status of JML features 55 ensures true also requires false which is equivalent to requires o null Then E would fail and C and D would be OK In otherwords it would be the same as Case 2 below e Case 2 Super class has non null subclass has no spec and no non null class Super public void nonnull 0 non null Object o public void m non null Object o 4 nonnull o Line A OK o null Line B FAILS class Derived extends Super public void m Object o nonnull o Line C OK precondition limits values of o o null Line D OK no restriction on assignments in this body public void mm Object o m o Line E FAILS new SO m o Line F FAILS In this case Derived m has no specification Consequently it has a default specifica tion of requires false and effectively inherits the overridden method s specification including the non_null Lines B and F are still errors and A is not because
112. res clauses for the method and all the declarations that it overrides 3 8 2 also e Description JML allows multiple specifications for a single method declaration these are separated and connected by the also keyword Furthermore if the method has Chapter 3 Status of JML features 24 additional declarations with or without specifications in an earlier source file in the refinement sequence or an overridden method in a super class or interface then and only then the specification must begin with also to indicate that there are some previous declarations with possible specifications of which the reader should be aware e Status The use of also is completely implemented with desugaring occurring as described above e Differences from JML or Java None e Comment This syntax for combining specifications is different than and not backwards compatible with the syntax used in ESC Java That tool did not allow combining mul tiple specifications using also and did not support refinement sequences Where there was inheritance of specification clauses from a super class or interface the keywords also_requires also_ensures also_modifies and also_exsures were required These keywords are not supported in ESC Java2 and such specifications will need to be rewritten using the new also syntax 3 8 3 model_program e Description Model programs are an alternate way to provide specifications for a method Rather than stating logical condit
113. s 0 0 00 c cece eens 70 6 5 19 semicolon termination lesse cece eee eee ee T1 6 5 20 need for the field method constructor keywords 71 6 5 21 omission of method bodies 000 eeee ee eee 71 6 5 22 Errors and cautions 0 0 e cece nh 71 6 5 23 membership in lockset 0000 liess T1 6 6 JML features needing clarification oooooooocoooomooo 71 6 6 1 model programs sssssessseess nn T1 6 6 2 callable accessible ooooooooooomommmoomooo 71 6 6 3 when measured Dyas sareanicesuate eee eee cece ee aiaa 71 6 6 4 initializer static initializer liliis esie sees T1 6 6 5 desugaring of forall o o ooooooooococorocrooomo 71 6 0 6 weakly 4 air a ai ede Feb o ead sade 71 0 0 1 Hence Dy reri diysan du anaE naa a e de ea ale E EEEE 71 6 6 8 use of result in duration and working_space clauses ral 6 6 9 instance fields and this in constructor preconditions 7i 6 6 10 rules about splitting annotations across comments 71 6 6 11 Ntypeof applied to primitive tyD8S oooooooooo 71 6 7 Desired extensions 0000 cc cece cece as 72 Appendix A Bibliography Modifier Summary Concept Intil x ados oe e trie cue td de dia vi Chapter 1 Introduction 1 1 Introduction 1 1 Motivation and Background ESC Java2 extends the pioneering work on ESC Java by a group Flanagan etal02 at th
114. s pure non null helper Model methods may be declared in multiple specification files but may have an imple mentation in at most one e Status Model methods are parsed and converted to regular Java methods within ESC Java2 The use of model methods in static checking is described in e Differences from JML or Java Model methods are parsed and converted to regular Java methods within ESC Java2 Consequently ESC Java2 will not detect their illegal use within the implementation of a Java routine Some related scoping issues in the presence of inheritance Chapter 3 Status of JML features 17 3 6 4 Model constructors e Description Model constructors are constructor declarations within an annotation and modified with the modifier model They declare constructors that may be used in model programs and if pure in specifications A model constructor may have these Java modifiers public protected private it may have these JML modifiers pure helper Constructors may be strictfp only by virtue of the entire class being declared strictfp Model constructors may be declared in multiple specification files but may have an implementation in at most one e Status Model constructors are parsed and converted to regular Java constructors within ESC Java2 e Differences from JML or Java Model constructors are parsed and converted to regular Java constructors within ESC Java2 Consequently ESC Java2 will not detect th
115. s static or to monitored by x this if x is not static e Status Implemented The implementation improves on that in ESC Java by imple menting monitors for static fields and by making the error messages more informative and accurate e Differences from JML or Java None Check does JML and jmlrac support static monitors 3 12 3 final Java e Description This Java modifier indicates that the field it modifies may not be assigned to after it has been initialized either by an initializer or in a constructor Java has some complex rules about definite assignment that are relevant but not discussed here e Status It is supported by the ESC Java2 parser and type checker It does not have any effect on the static checking There are checks only that variables with initializers are not subsequently assigned to Is definite assignment checked e Differences from JML or Java None Chapter 3 Status of JML features 34 3 12 4 volatile Java e Description This Java modifier affects the optimizations that might be applied and the semantics of the order of writing the values of object fields to memory It affects multi threaded programs only It is not applicable to a ghost or model declaration e Status Parsed but ignored by the static checker e Differences from JML or Java None 3 12 5 transient Java e Description Fields designated transient are not saved as part of an object s persistent state Th
116. se in running simplify de fault noprune noplunge No longer e PROVER KILL TIME the maximum number of seconds to spend on any one proof attempt default 300 e PROVER CC LIMIT the maximum number of static checker warnings to report for any given routine default 10 e and many others undocumented but all beginning with PROVER The following variables are set automatically to match a standard release For normal operation they should not be set They would be set to another value only in debugging or other unusual circumstances However if they are set in the environment to an arbitrary value they would cause a malfunction of the tool e ESC_CLASSPATH the classpath needed to run the ESC Java2 tool i e to find its class files This is different than the classpath needed to find the source and class files being checked those classpaths are set with the classpath and sourcepath command line options e ESCJ SIMPLIFY DIR the directory in which to find the Simplify executable Predicate abstraction uses some undocumented java properties Chapter 5 Changes to static checking in ESC Java2 63 5 Changes to static checking in ESC Java2 Many of the changes from ESC Java to ESC Java2 are changes to the parser so that ESC Java2 will parse and typecheck all of current JML as well as being upgraded to handle Java 1 3 and 1 4 However there are several ways in which the static checking has been modifie
117. sertionError value C Treat them as a JML assert statement namely as equivalent to assert predicate The command line options for these three cases are A source 1 4 B javaAssertions or eajava C jmlAssertions or eajml Note that there are internally three independent conditions e The version of Java being recognized This is controlled by the source option e Whether Java assert statements are enabled given that Java 1 4 source is being processed Java has them disabled by default This is controlled by the options disableassertions enableassertions da ea The use as in Java of package Chapter 3 Status of JML features 46 names with these assertions or of enabling or disabling system assertions is not imple mented in ESC Java2 Whether to treat Java 1 4 assert statements in Java mode or JML mode given that Java assertions are enabled This is controlled by the javaAssertions and jmlAssertions options javaAssertions is the default both options also effectively do source 1 4 ea Here are some examples of use public void m assert false Message J Java behavior ESC Java2 will issue an Unexpected Exception warning JML behavior ESC Java2 will issue an Assert warning public void m assert false Message nowarn Java behavior ESC Java2 will issue an Unexpected Exception warning JML behavior ESC Java2 will not issue any warning suppressed by the nowarn an
118. sion syntax are all completely parsed and are typechecked with varying degrees of rigor Most features are interpreted and can be reasoned about by the static checker Some that are only partially handled by the static checker are these e new instance expressions These are completely handled in program code In specifica tion expressions these are interpreted according to their specifications by a procedure that inlines the specifications but only to a limited depth of rewriting Check this 22 e new array expressions These are handled adequately in both program code and in annotations except for reasoning about the values of array elements when initializers are provided e class expression e anonymous classes CLarify the above 3 17 store ref expressions This whole section needs thorough correction and review Some annotations require a list of store ref expressions which are expressions whose value is a set of references to fields of classes or objects in particular the value has type org jmlspecs models JMLObjectSet For example the modifies clause designates a set that is a JMLObjectSet of store refs that are allowed to be assigned to within a method This section describes the syntactic features that designate such sets Not sure this is right in the wake of data groups and in maps clauses 3 17 1 ident super this ident this This designates a field of an object
119. tain the java file In this case the java file is used as the source code of the implementation and to define the signature of the class but no specifications are obtained from it A caution is issued to the user in this case e It is not required that a java or a class file exist since it is desired to be able to write specifications in advance of an implementation However if either one does exist then the following rules are used a if the implementation is needed because this is a type whose implementation is being checked by ESC Java2 as well as the signature then the java file is used for both the implementation and the signature regardless of time stamp if it exists b if only a signature is needed then which file is used is determined by a command line option e g preferSource as described in Section 4 3 Command line op tions page 59 The default is to use the most recently modified of the two to define the Java signature of the class whether or not it is in the refinement sequence Specifications are not permitted to add new non model non ghost declarations of fields routines or enclosed classes or interfaces to those defined in the Java implementation e Currently class files do not contain specifications However we would like to leave open the possibility that in the future a binary version of parsed and checked specifications could be created that would improve processing time Status The above rules
120. tation expressions 49 3 19 13 Specifications and inheritance o o o ooooooo o 49 3 19 13 1 Desugaring in the presence of inheritance 49 3 19 13 2 Defaults and inheritance 0oooocooocccooo 51 3 19 13 3 Inheritance and non_null 00 53 4 ESC Java2 features oooooo ooooo 57 4 1 Error and warning messages esses ee ee eee 57 4 2 Nowarn annotations and warnings sseeeeee eres 57 4 2 1 nowarn annotations sseeeee een 57 4 2 2 nowarn warning typeS 0 0 eee eee eee eee neces 58 4 3 Command line options 000 c cece nn 59 4 4 Environment variables affecting ESC Java2 61 Changes to static checking in ESC Java2 63 5 1 Handling of specification inheritance 0 000000 eee 63 52 A Eod deber Gee a E eratac op donde ase 63 5 3 Translation of the Java 1 4 assert statement 63 5 4 Semantics of String 0c ccc cc NEE E E e 63 5 4 1 Concatentation operators lesse eee eee eee 63 5 4 2 Explicit String literals 0 0 0000 c cee eee eee eee 64 5 4 3 The intern method 00 cee eee esl 64 5 5 The TYPE and java lang Class types 0004 64 5 6 The initially clatise 0 66 2 s se hg a 64 5 7 The constraint clause 0 cece eects 64 5 8 Use of modifies clauses in checking routine bodies 65 5 9 Defaults for modifies
121. that a constructor does not establish the post condition stated in an initially clause added in ESC Java2 e Invariant 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 e LoopInv warns that some loop invariant may not hold when it is supposed to e Modifies warns that an assignment or method call violates the assignable modifies clauses of a routine added in ESC Java2 e OwnerNull warns that a constructor may violate the implicit postcondition this owner null Explain this e NegSize warns of a possible attempt to allocate an array of negative length e NonNull warns of a possible attempt to assign the value null to a variable whose declaration is modified by a non null pragma or to call a routine with an actual parameter value of null when the declaration of the corresponding formal parameter is modified by a non null pragma Chapter 4 ESC Java2 features 59 e NonNulllnit 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 e Null warns of a possible attempt to dereference null for example by field access 0 an array access O i a method call 0 m a synchronized statement synchronized 0 or a throw statement throw 0 where O evaluates to null e Post warns that a
122. thod of the String class 5 4 1 Concatentation operators Note that the operator is equivalent to an expression using the operator namely x y is equivalent to x x y The key semantic property of the String concatenation property is that it produces a fresh newly allocated object This is important because within a pure method a fresh object may be modified just as a newly constructed object may be modified Chapter 5 Changes to static checking in ESC Java2 64 5 4 2 Explicit String literals The important semantic property of String literals in Java is that two syntactically identical String literals also compare equal as objects Also the concatenation of two String literals produces a String literal at compile time Thus String a b c a sample b sample c sam ple boolean t a b This is true t a c This is also true b new String sample t a b This is NOT true The Simplify prover does not have any built in knowledge of Strings Consequently Esc Java2 makes a note of all of the String literals in a module replacing each one by a unique symbol but using the same symbol for syntactically identical literals The concate nation of String literals is performed by the parser 5 4 3 The intern method The intern operation maps Strings that compare equal using the equals method to the same Object String literals are automatically interned Thus boolean t Strin
123. tion at all and the routine is a constructor or is a method that does not override any super class or super interface methods the default is requires true l Michael M ller contributed to this formulation of the defaults for requires Chapter 3 Status of JML features 22 e If there is no specification at all including no non nu11 modifiers and the method does override some super class or super interface method the default is requires false e For the default constructor if no specifications have been given the default re quires specification is the same as the requires specification of the corresponding superclass constructor The reasons for these defaults are explained in Section 3 19 13 Specifications and in heritance page 49 The modifies clause has this exception to the above rule For the default constructor if no specifications have been given the default modifies specification is the same as the modifies specification of the corresponding superclass constructor This is not a textual replication rather the subclass constructor may modify the same set of locations under the same conditions as the superclass constructor Note that the defaults for the diverges clause are different between the lightweight and heavyweight forms The lightweight default diverges true puts the least restrictions on the implementation it states that the implementation is allowed to be non terminating but not required to be The heavy
124. to denote an integral type equivalent to the mathematical integers That is it has infinite range and no underflow or overflow as a result of a fixed bit depth Status The type name is parsed but is equivalent to long real This is a new type name used in JML to denote a type equivalent to the math ematical real numbers That is it has infinite range and precision and no underflow overflow or rounding error as do float and double Status The type name is parsed but is equivalent to double LockSet This type may not be named there is no token LockSet However the type is implicitly used as the type of the JML token lockset as the type of the argument of max and in the LockSet membership operation 3 16 4 quantified expressions forall exists num_of max min sum product As described in the JML documentation quantified expressions take the form or quantifier keyword type idlist range expr expr Chapter 3 Status of JML features 42 quantifier keyword type idlist expr or quantifier keyword type idlist expr The range expr is a boolean expression its default value is true The idlist is a comma separated list of identifiers these are the bound variables of the quantification No side effects are permitted in the predicate or expression Status e forall exists Fully implemented and used in static checking e num_of max min sum product Parsed and typechecked but not
125. tus of JML features 45 3 19 4 Java and JML assert statements JML has an assert statement of the form assert predicate The static checker will evaluate the predicate in the appropriate context If it cannot establish that the predicate is always true an ESC Java warning will be issued Java 1 4 also has an assert statement with the syntax assert predicate value If the predicate is not true then a java lang AssertionError is created with the given value as its argument and the exception is thrown In versions of Java before 1 4 assert was a legitimate identifier name in Java 1 4 it is a keyword and may not be used as an identifier To achieve backwards compatibility Java compilers have a source command line option ESC Java2 behaves in a way similar to typical Java compilers e specifying source 1 4 causes ESC Java2 to interpret assert in Java statements as a keyword e omitting the source option or specifying an argument other than 1 4 causes ESC Java2 to treat assert in Java statements as an identifier and to issue errors on encountering uses of the word as a keyword i e to interpret assert in Java 1 3 mode There are three options for how ESC Java2 should treat Java assert statements when source 1 4 is specified ESC Java2 provides command line options to achieve each of these behaviors A Parse but ignore them B Treat them as Java does namely as equivalent to if predicate throw new java lang As
126. ve 33 5 12 5 transient Java perro acre bridas 34 3 12 60 static Java Tt 34 312 7 instance JMG coria 34 3 13 Annotation modifiers for formal parameters 34 3131 oau JME Loeb bes a REA BED te 34 243 2 MENOS cUm 35 3 14 Annotation statements within the body of a method or COUSULUCUOL ornnes Hee A a Pad dd ead nen PAS 3 14 1 assume assume redundantly lesse esses eee 3 14 2 assert assert redundantly 0 0 000 eese 9 14 8 Strides e CURE epe td dere aed d do Us pee eds 3 144 dureachbable iie re recen dem el oc to Re 3 14 5 hence by hence by redundantly sues 3 14 6 loop invariant loop_invariant_redundantly maintaining maintaining redundantly 3 14 7 decreases decreasing decreases redundantly decreasing redundantly 0 00 0 cece cee eese 3 14 8 ghost declarations 000 0 cece eee tee eee 3 15 Modifiers that may be applied to local declarations 245 non null IML criteria diia tapes ex eg 5 15 2 umiritialized JML aie do as oS MEIN METTE 3 16 JML functions extensions to expressions 3 16 1 New operators in JML seeeeeeee eene 3 16 2 New JML expressions functions and values 3 16 3 New JML types euueeeeeseer n 3 16 4 quantified expressions Morall exists num_of max Xmin stim Nproduet s 1234 enda tanta rada edes 3 16 5 Set comprehension
127. weight default diverges false requires the implementation to terminate with either an exception or a normal return However this is not checked in the current implementation e Status The lightweight and heavyweight specification forms including nesting using and and combination with also are fully parsed and implemented though not all clause types as described below are fully implemented or handled by the static checker e Differences from JML or Java None except that ESC Java2 does not constrain the order of clauses as rigidly as do JML tools JML requires forall old and requires clauses to precede any other clauses with a warning level of w2 not the default JML will also warn about deviations from a recommended order of the other clause types ESC Java2 will accept clauses in any order but note that the scope of forall and old does not include clauses that precede them Esc Java2 does not currently check the access modifiers on behavior and example keywords What happens with the privacy checking e Comment The ESC Java2 and ESC Java translator which produces the verification conditions to be checked by the static checker accepts a set of specification clauses in lightweight form In order to handle the nested and heavyweight forms and the combi nation of specifications using also either within one source file or across a refinement sequence ESC Java2 desugars the more complicated syntax into a simpler
128. ww jmlspecs org e The JML project on sourceforge http sourceforge net projects jmlspecs e The JML interest mailing list on sourceforge jmlspecs interest lists sourceforge net e The JML development mailing list on sourceforge jmlspecs developers lists sourceforge net Chapter 1 Introduction 3 e The ESC Java2 mailing list on sourceforge jmlspecs escjava lists sourceforge net JML utilizes the Java subset of the multijava compiler Information about multijava can be obtained from these sources e The multijava website http www multijava org e The multijava project on sourceforge http sourceforge net projects multijava B Chapter 2 Running ESC Java2 4 2 Running ESC Java2 There are three essential items that you need in order to run ESC Java2 a build of ESC Java2 itself an executable for Simplify for your platform and a version of the JML specifications for the Java system classes These are available together as a single release from the KUN ESC Java2 website http www cs kun nl sos research nl However you may want to substitute an alternate version of the JML specifications that you generate yourself or you obtain from the JML website The specifications included with ESC Java2 are a snapshot of the JML specifications at the time of release There are a number of ways to run ESC Java2 The various command line options are described in Section 4 3 Command line options page 59 1 Double click the es
129. y e Description A signals clause states a condition that must hold in the post state of a method or constructor whenever the associated preconditions hold in the pre state and the method or constructor exits with an exception of or a subclass of the designated type The expression in the clause may also be Not specified which is equivalent to omitting the clause The expression must have boolean type and is evaluated in the post state though the keyword result is not valid in a signals clause e Status Implemented and used by the static checker e Differences from JML or Java None 3 9 6 modifies modifiable assignable modifies redundantly modifiable redundantly assignable redundantly e Description The modifies clause indicates which memory locations may be assigned within the associated routine when the routine is called in a pre state that satisfies the associated preconditions The list of locations in the modifies clause may also contain the special keywords Nnothing everything Nnot specified and the wild card forms expr typename array and array expr expr Any expressions in the clause are evaluated in the pre state Each location listed in the clause implicitly includes all the elements of its datagroup if a datagroup is associated with the location Other memory locations are added to a lo cation s datagroup using the in and maps clauses see Section 3 11 Field Annotations page 32 Chapter 3
130. y e Description Comment needed semantics unknown This keyword is followed by a predicate e Status Parsed and type checked Ignored by the static checker e Differences from JML or Java None 3 14 6 loop invariant loop invariant redundantly maintaining maintaining redundantly e Description A loop invariant pragma is followed by a predicate The pragma must appear immediately prior to a loop statement for while do or Java labeled state ment The predicate must hold at the start of each loop iteration Details are given in the ESC Java User s Manual Note that loops are checked only by unrolling them a few iterations The number of iterations can be set by the loop command line option e Status Implemented e Differences from JML or Java None 3 14 7 decreases decreasing decreases redundantly decreasing redundantly e Description This pragma specifies a quantity type int which must decrease but must always be non negative at the start of any loop iteration Note that loops are checked only by unrolling them a few iterations The number of iterations can be set by the loop command line option e Status Implemented e Differences from JML or Java None Chapter 3 Status of JML features 37 3 14 8 ghost declarations Description JML and ESC Java2 but not ESC Java allow the declaration of local ghost variables within the body of a routine just as Java allows local declarations These can then be

Escjava2-Implementat..

Contents

Download Pdf Manuals

Related Search

Related Contents