[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

2. Fundamental Concepts

This chapter discusses fundamental concepts that are used in explaining the semantics of JML.

2.1 Types can be Classes and Interfaces  
2.2 Model and Ghost  
2.3 Lightweight and Heavyweight Specifications  
2.4 Privacy Modifiers and Visibility  
2.5 Instance vs. Static  
2.6 Locations and Aliasing  
2.7 Expression Evaluation and Undefinedness  
2.8 Null is Not the Default  
2.9 Language Levels  


2.1 Types can be Classes and Interfaces

In this manual we use type to mean either a class, interface, or primitive value type in Java. (Primitive value types include boolean, int, etc.)

A reference type is a type that is not a primitive value type, that is either a class or interface. When it is not necessary to emphasize that primitive value types are not included, we often shorten "reference type" to just "type".


2.2 Model and Ghost

In JML one can declare various names with the modifier model; for example one can declare as "model" fields, methods, and even types. One can also declare some fields as ghost fields. JML also has a model import directive (see section 5. Compilation Units).

The model modifier has two meanings. The first meaning of a feature declared with model is that it is only present for specification purposes. For example a model field is an imaginary field that is only used for specifications and is not available for use in Java code outside of annotations. Similarly, a model method is a method that can be used in annotations, but cannot be used in ordinary Java code. A model import directive imports names that can be used only within JML annotations. The second meaning of model depends on the type of feature being declared.

The most common and useful model declarations are model fields. A model field should be thought of as the abstraction of one or more non-model (i.e., Java or concrete) fields [Cheon-etal05]. (By contrast, some authors refer to what JML calls model fields as "abstract fields" [Leino98].) The value of a model field is determined by the concrete fields it abstracts from; in JML this relationship is specified by a represents clause (see section 8.4 Represents Clauses). (Thus the values of the model fields in an object determines its "abstract value" [Hoare72a].) A model field also defines a data group [Leino98], which collects model and concrete fields and is used to tell JML what concrete fields may be assigned by various methods (see section 10. Data Groups).

Unlike model fields, model methods and model types are not abstractions of non-model methods or types. They are simply methods or types that we imagine that the program has, to help in a specification.

A ghost field is similar to a model field, in that it is also only present for purposes of specification and thus cannot be used outside of JML annotations. However, unlike a model field, a ghost field does not have a value determined by a represents clause; instead its value is directly determined by its initialization or by a set-statement (see section 13. Statements and Annotation Statements).

Although these model and ghost names are used only for specifications, JML uses the same namespace for such names as for normal Java names. Thus, one cannot declare a field to be both a model (or ghost) field and a normal Java field in the same class (see section 17. Separate Files for Specifications). Similarly, a method is either a model method or not. In part, this is done because JML has no syntactic distinction between Java and JML field access or method calls. This decision makes it an error for someone to use the same name as a model or ghost feature in an implementation. In such a case if the Java code is considered to be the eventual goal, then one can either change the name of the JML feature or have one declaration in which the Java feature is modified with the JML modifier spec_public. See section 2.4 Privacy Modifiers and Visibility, for more about spec_public.


2.3 Lightweight and Heavyweight Specifications

In JML one is not required to specify behavior completely. Indeed, JML has a style of method specification case, called lightweight, in which the user only says what interests them. On the other hand, in a heavyweight specification case, JML expects that the user is fully aware of the defaults involved. In a heavyweight specification case, JML expects that a user only omits parts of the specification case when the user believes that the default is appropriate.

Users distinguish these between such cases of method specifications by using different syntaxes. See section 9.2 Organization of Method Specifications, for details, but in essence in a method specification case that uses one of the behavior keywords (such as normal_behavior, exceptional_behavior, or behavior) is heavyweight, while one that does not use such a keyword is lightweight.


2.4 Privacy Modifiers and Visibility

Java code that is not within a JML annotation uses the usual access control rules for determining visibility (or accessibility) of Java [Arnold-Gosling-Holmes00] [Gosling-etal00]. That is, a name declared in package P and type P.T may be referenced from outside P only if it is declared as public, or if it is declared as protected and the reference occurs within a subclass of P.T. This name may be referenced from within P but outside of P.T only if it is declared as public, default access, or protected. Such a name may always be referenced from within P.T, even if it is declared as private. See the Java language specification [Gosling-etal00] for details on visibility rules applied to nested and inner classes.

Within annotations, JML imposes some extra rules in addition to the usual Java visibility rules [Leavens-Baker-Ruby06] [Leavens-Mueller07]. These rules depend not just on the declaration of the name but also on the visibility level of the context that is referring to the name in question. For purposes of this section, the annotation context of a reference to a name is the smallest grammatical unit with an attached (or implicit) visibility. For example, this annotation context could be a method specification case, an invariant, a history constraint, or a field declaration. The visibility level of such an annotation context can be public, protected, private, or default (package) visibility.

JML has two rules governing visibility that differ from Java. The first is that an annotation context cannot refer to names that are more hidden than the context's own visibility. That is, for a reference to a name x to be legal, the visibility of the annotation context that contains the reference to x must be at least as permissive as the declaration of x itself. The reason for this restriction is that the people who are allowed to see the annotation should be able to see each of the names used in that annotation [Meyer97], otherwise they might not understand it. For example, public clients should be able to see all the declarations of names in publicly visible annotations, hence public annotations should not contain protected, default access, or private names.

In more detail, suppose x is a name declared in package P and type P.T.

In the following example, the comments on the right show which uses of the various privacy level names are legal and illegal. Similar examples could be given for method specifications, history constraints, and so on.

 
public class PrivacyDemoLegalAndIllegal {
   public int pub;
   protected int prot;
   int def;
   private int priv;

   //@ public invariant pub > 0;      // legal
   //@ public invariant prot > 0;     // illegal!
   //@ public invariant def > 0;      // illegal!
   //@ public invariant priv < 0;     // illegal!

   //@ protected invariant prot > 1;  // legal
   //@ protected invariant def > 1;   // illegal!
   //@ protected invariant priv < 1;  // illegal!

   //@ invariant def > 1;              // legal
   //@ invariant priv < 1;             // illegal!

   //@ private invariant priv < 1;     // legal
}

Note that in a lightweight method specification, the privacy level is assumed to be the same privacy level as the method itself. That is, for example, a protected method with a lightweight method specification is considered to be a protected annotation context for purposes of checking proper visibility usage [Leavens-Baker-Ruby06] [Mueller02]. See section 2.3 Lightweight and Heavyweight Specifications, for more about the differences between lightweight and heavyweight specification cases.

(The ESC/Java2 system has the same visibility rules as described above. However, this was not true of the old version of ESC/Java [Leino-Nelson-Saxe00].)

The JML keywords spec_public and spec_protected provide a way to make a declaration that has different visibilities for Java and JML. For example, the following declaration declares an integer field that Java regards as private but JML regards as public.

 
    private /*@ spec_public @*/ int length;

Thus, for example, length in the above declaration could be used in a public method specification or invariant.

However, spec_public is more than just a way to change the visibility of a name for specification purposes. When applied to fields it can be considered to be shorthand for the declaration of a model field with a similar name. That is, the declaration of length above can be thought of as equivalent to the following declarations, together with a rewrite of the Java code that uses length to use _length instead (where we assume _length is fresh, i.e., not used elsewhere in the class).

 
  //@ public model int length;
  private int _length; //@ in length;
  //@ private represents length = _length;

The above desugaring allows one to change the underlying field without affecting the readers of the specification.

The desugaring of spec_protected is the same as for spec_public, except that one uses protected instead of public in the desugared form.

The second rule for visibility prohibits an annotation context from writing specifications in an annotation context that constrain fields that are visible to more clients than the specifications (see section 3 of [Leavens-Mueller07]). In particular, this applies to invariants and history constraints. Thus, for example, a private invariant cannot mention a public field, since clients could see the public field without seeing the invariant, and thus would not know when they might violate the private invariant by assigning to the public field. Thus, for example, the invariants in the following example are all illegal, since they constrain fields that are more visible than the invariant itself.

 
public class PrivacyDemoIllegal {
   public int pub;
   protected int prot;
   int def;
   private int priv;

   //@ protected invariant pub > 1;   // illegal!

   //@ invariant pub > 1;              // illegal!
   //@ invariant prot > 1;             // illegal!

   //@ private invariant pub > 1;      // illegal!
   //@ private invariant prot > 1;     // illegal!
   //@ private invariant def > 1;      // illegal!
}


2.5 Instance vs. Static

In Java, a feature of a class or interface may declared to be static. This means that the feature is not part of instances of that type, and it means that references to that feature (from outside the type and its subtypes) must use a qualified name of the form T.f, which refers to the static feature f in type T.

A feature, such as a field or method, of a type that is not static is an instance feature. For example, in a Java interface, all the methods declared are instance methods, although fields are static by default. In a Java class the default is that all features are instance features, unless the modifier static is used.

In JML declarations follow the normal Java rules for determining whether they are instance or static features of a type. However, within annotations it is possible to explicitly label features as instance (see section 6. Type Declarations for the syntax). The use of the instance modifier is necessary to declare model and ghost instance fields in interfaces, since otherwise the Java default modifier for fields in interfaces (static) would apply.

It is also useful, in JML, to label invariants as either static or instance invariants. See section 8.2.1 Static vs. instance invariants, for more on this topic.


2.6 Locations and Aliasing

A location is a field of an object or a local variable. A local variable is either a variable declared inside a block (such as a method body) or a formal parameter of a method.

An access path is an expression either of the form x, where x is an identifier, or p.x, where p is an access path and x is an identifier.(5) (In forming an access path, we ignore visibility.)

In a given program state, s, a location l is aliased if there are two or more access paths that, in s, both denote l. The access paths in question are said to be aliases for l. Similarly, we say that an object o is aliased in a state s if there are two access paths that, in s, both have o as their value. In Java, it is impossible to alias local variables, so the only aliasing possible involves objects and their fields.


2.7 Expression Evaluation and Undefinedness

Within JML annotations, Java expressions generally have the values that are defined in the Java Language Specification [Gosling-etal00]. This has consequences on the interpretation of assertion expressions [Chalin07] [Rioux-Chalin07]: an assertion is taken to be valid if and only if its interpretation

Note that this interpretation of assertions, said to be based on "strong validity" [Chalin07], was made the default assertion semantics for JML in 2007. Prior to that, assertions were interpreted using a classical definition of validity [Leavens-etal05] [Leavens-Baker-Ruby06] [Gries-Schneider95] [Jones95e].

The strong validity semantics for assertion evaluation means that exceptions may arise during evaluation of subexpressions within assertions. These exceptions should be avoided by the specifier and tools are encouraged to warn users when they detect that an exception may arise during assertion evaluation.

To avoid exceptions during assertion evaluation, specifiers should practice good Java coding habits, and write specifications that prevent such exceptions. To do this, one can use left-to-right ordering of evaluation of subexpressions and the short-curcuit nature of the Java operators && and ||. JML also evaluates the its two implication operators, ==> and <== in short-curcuit fashion from left to right. Within a specification case, the precondition can protect the rest of the specification from exceptions [Leavens-Wing98]. That is, one can assume that the precondition holds in the remainder of the clauses in a specification case. JML also evaluates multiple occurrences of clauses of the same kind (such as requires or ensures) within a spec case in top to bottom order, so earlier clauses can protect later ones, just as if they were combined with &&.


2.8 Null is Not the Default

One common problem that occurs in Java and JML specifications is the possibility of null dereferences. For example, if x is null then x.f and x.m() both result in a NullPointerException. Such null pointer exceptions cause undefinedness in expression evaluation, as described above (see section 2.7 Expression Evaluation and Undefinedness).

To avoid having to constantly specify that declarations (other than local variables) are non-null, JML makes them implicitly non_null by default. That is, unless a

is explicitly annotated with the modifier nullable, that declaration is assumed to be non_null.

For a field whose type is an array of reference types, such as a field of type Object[], both the field that refers to the array and the elements of the array are non_null by default. If a field whose type is an array of reference types is declared as nullable, then both the reference to the array and all of its elements may potentially be null. To specify that the field is not null but the elements may be null, use an invariant to state that the field cannot contain null, as follows.

 
private /*@ spec_public nullable @*/ Object[] a;
//@ public invariant a != null;

While these defaults differ from Java, research has found that in most cases a declaration is expected to be non-null [Chalin-Rioux05]. More importantly, since one of the most common mistakes in JML specifications (and in Java programs) is forgetting to specify that a declaration is non-null, making the default be that they cannot hold null helps eliminate a source of common errors in specifications.

See section 6.2.13 Nullity Modifiers, for more details on the nullity modifiers.


2.9 Language Levels

One of JML's goals is to provide a single language that can be used with a variety of different tools. However, JML is also an evolving language that is used as a research vehicle by many groups. The evolution of JML means that some features are not completely documented or implemented. Use of JML in research means that some tools will have features that are not supported by other tools. All of this has the potential to threaten portability and to make JML more difficult to learn and use.

The research groups working on JML are committed to making these problems as invisible to non-researchers as possible, and for this reason have defined several language levels. The goal of defining these language levels is to make it easier to learn and use JML and its various tools.

We define the following language levels.(6)

When learning JML, one should focus on levels 0 features first, as these form the heart of the language which should be understood by all JML tools. Features at level 1 are next in importance and should be supported by most tools that are interested in having a large user base. Features at higher levels are less important and may not be present in all tools. Users should feel free to ignore them unless they meet some specific need.

The language levels also provide guidance for tool designers. JML tools should parse all of the syntax in this reference manual that is not marked as experimental. This is the most important way to guarantee portability for users, and the easiest way for tools to get feedback. In addition, tools should check at least level 0, and preferably level 1 features. Features at levels 2 and 3 are candidates for the tool to just parse and ignore, if they are not features of interest for that tool. Experimental features may ignored (or added) by any tool.

Many tool developers may want to start off supporting only a subset of JML defined by level 0 and then move on to higher levels.

It is also suggested that tools give users optional feedback, perhaps in a verbose mode, as to which features are fully and partially supported. Clearly stating which JML levels are supported in a tool release is also very important.

More details are provided in the subsections below.

2.9.1 Level 0 Features  
2.9.2 Level 1 Features  
2.9.3 Level 2 Features  
2.9.4 Level 3 Features  
2.9.5 Level C Features  
2.9.6 Level X Features  


2.9.1 Level 0 Features

The features in this level form the core of JML and should be understood and checked by all JML tools. Beginning users should pay the most attention to these features. These features include all of Java and the syntax described in the rest of this section.

Synonyms for the keywords used in level 0 features are also considered to be part of level 0's lexical syntax. For example, since assignable is a keyword used in level 0, its synonyms modifiable and modifies are also included in the lexical syntax for level 0.

Many, but not all, of the JML additions to Java's modifiers (see section 6.2 Modifiers) are level 0 features. The following modifiers are included in level 0.

Type specifications (see section 8. Type Specifications) are a level 0 feature, although not all clauses and features of type specifications are level 0. The following type-level clauses are included in level 0.

Method specifications (see section 9. Method Specifications) are a level 0 feature. This includes the ability to combine specification cases using also (see section 9.6.5 Semantics of nested behavior specification cases) and specification inheritance [Dhara-Leavens96] [Leavens-Naumann06] [Leavens06b]. It also includes the use of \not_specified for all specification clauses that are at level 0. However, not all clauses and features of method specifications are level 0. The following parts of method specifications are included in level 0. Redundancy features of method specifications are only present at level 1, not at level 0. The details are described below.

Only static data groups (see section 10. Data Groups) are part of level 0.

Some of JML's extensions to Java's expression syntax (see section 12. Predicates and Specification Expressions), but not all of them, can be used at level 0. Note that calls to pure methods and constructors in spec-expressions are not part of level 0, but are only found at level 1. We describe the level 0 specification expressions below.

All of the Java statements and most of the JML extensions for adding assertions to statements and annotation statements (see section 13. Statements and Annotation Statements) are at level 0. But redundancy features of the JML extensions are only present at level 1, not at level 0. We describe the level 0 extensions to Java statements below.

The ability to use a .jml file (see section 17.1 File Name Suffixes) to give a separate specification for a compilation unit that only appears in binary form (e.g., in a .class file) is a level 0 feature.

Some syntax from the Universe type system (see section 18. Universe Type System) is included in level 0. However, readonly is considered to be in level X, as is the semantics of the Universe type system. The rep and peer modifiers are included in level 0 because, in some form, they are important to the semantics of several level 0 features [Mueller-Poetzsch-Heffter-Leavens03] [Mueller-Poetzsch-Heffter-Leavens06].


2.9.2 Level 1 Features

The features in this level will be understood and checked by many JML tools. They are quite important in practice, especially the use of methods and constructors in writing the specifications of other methods and constructors. Also useful are all of JML's redundancy features (see section 14. Redundancy), which are included here for all level 0 features and for other features at level 1.

The following additions to Java's modifiers (see section 6.2 Modifiers) are level 1 features.

The following type-level clauses (see section 8. Type Specifications) are included in level 1.

The following features of method specifications (see section 9. Method Specifications) are included in level 1.

The following extensions to Java's expression syntax (see section 12. Predicates and Specification Expressions) are included in level 1.

The following additions to Java's statement syntax (see section 13. Statements and Annotation Statements) are included in level 1.

The \bigint type (see section 19.1 \bigint) from the safe math extensions (see section 19. Safe Math Extensions) is a level 1 feature.


2.9.3 Level 2 Features

Level 2 contains features that are more specialized to particular uses of JML, but are still useful for several different tools. It also contains some features that are mainly needed to explain JML's semantics, and have not been heavily used (so far).

The nowarn-pragma (see section 4.2 Lexical Pragmas).

The following type-level clauses (see section 8. Type Specifications) are included in level 2.

The following features of method specifications (see section 9. Method Specifications) are included in level 2.

The following extensions to Java's expression syntax (see section 12. Predicates and Specification Expressions) are included in level 2.

The following additions to Java's statement syntax (see section 13. Statements and Annotation Statements) are included in level 2.

Note that all the model-prog-statements (see section 15. Model Programs) are at level 2, because the model program style of method specification is at this level.

Aside from the \bigint type (see section 19.1 \bigint), which is a level 1 feature, the rest of the safe math extensions (see section 19. Safe Math Extensions) are level 2 features. This includes the following particulars.


2.9.4 Level 3 Features

Level 3 features are more exotic and even less commonly used. The semantics of some of these features are not yet well understood, and the features are not implemented by many tools.


2.9.5 Level C Features

The features in this level are related to the specification of concurrency. This includes features inherited from ESC/Java having to do with concurrency. The features of this level are as follows.


2.9.6 Level X Features

The features in this level are experimental. Some of the ones we know about are as follows.


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by U-leavens-nd\leavens on May, 31 2013 using texi2html