[ << ] [ >> ] [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

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.

• An expression in a public annotation context (e.g., in a public method specification case) can refer to x only if x is declared as public (or spec_public).

• An expression in a protected annotation context (e.g., in a protected method specification) can refer to x only if x is declared as public or protected, and x must also be visible according to Java's rules (so if x is protected, or spec_protected, then the reference must either be from within P or, if it is from outside P, then the reference must occur in a subclass of P.T).

• An expression in a default (package) visibility annotation context (e.g., in a default visibility method specification) can refer to x only if x is declared as public, protected, or with default visibility, and x must also be visible according to Java's rules (so if x has default visibility, then the reference must be from within P).

• An expression in a private visibility annotation context (e.g., in a private method specification) can refer to x only if x is visible according to Java's rules (so if x has private visibility, then the reference must be from within 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

• does not cause an exception to be raised, and
• yields the value true.
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)

• Level 0 should be supported by all JML tools and constitutes the heart of JML. All users should be familiar with these level 0 features. They are fundamental to all uses of JML, including its use as a design by contract language, as documentation, and as formal specification for formal verification efforts. Thus the level 0 features should be the ones that tutorial materials concentrate on. Users should be able to count on these features being understood and checked by all tools.

• Level 1 should be supported by most JML tools and should be a first priority for developers after implementing the Level 0 features. There are three categories of features that level 1 adds to level 0. The first is the redundancy features of JML, which are useful in documentation, but not absolutely vital. The second is features that are sugars for features present in level 0. The third is various features for which modular static verification is still problematic, although a runtime assertion checking semantics has been implemented. This includes the use of methods and constructor calls in assertions.

• 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).

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

• Level C contains features related to specification and verification of concurrent Java programs. Some of these are from ESC/Java [Leino-Nelson-Saxe00], and others are from [Rodriguez-etal05].

• Level X contains experimental features, which may eventually be moved to other levels. Many tools will have other experimental features not documented here.

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

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.

• Object invariants, that is an invariant (see section 8.2 Invariants) that is either written in an interface using the modifier instance (see section 6.2.8 Instance) or one that is written in a class and that does not use the modifier static (see section 8.2.1 Static vs. instance invariants).

• The functional form of a represents-clause (see section 8.4 Represents Clauses). That is, a represents clause that uses = and (not \such_that).

• The initially-clause (see section 8.5 Initially Clauses).

• The type-spec \TYPE (optionally, as a type of array element). See section 7.1.2.2 Type-Specs, for more details.

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.

• Lightweight specification cases (see section 9.4 Lightweight Specification Cases), although not all clauses that are allowed in the syntax are in level 0.

• Heavyweight specification cases (see section 9.5 Heavyweight Specification Cases) that do not use the keyword code. This includes behavior-spec-case (see section 9.6 Behavior Specification Cases), normal-behavior-spec-case (see section 9.7 Normal Behavior Specification Cases), and exceptional-behavior-spec-case (see section 9.8 Exceptional Behavior Specification Cases). However, note that not all clauses that are allowed in the syntax are in level 0.

• The requires-clause (see section 9.9.2 Requires Clauses). The redundant form of this clause (requires_redundantly, pre_redundantly) is a level 1 feature.

• The ensures-clause (see section 9.9.3 Ensures Clauses). The redundant form of this clause (ensures_redundantly, post_redundantly) is a level 1 feature.

• The signals-clause (see section 9.9.4 Signals Clauses). The redundant form of this clause (signals_redundantly, exsures_redundantly) is a level 1 feature.

• The signals_only-clause (see section 9.9.5 Signals-Only Clauses). The redundant form of this clause (signals_only_redundantly) is a level 1 feature.

• The assignable-clause (see section 9.9.9 Assignable Clauses). The redundant form of this clause (assignable_redundantly, modifiable_redundantly, modifies_redundantly) is a level 1 feature.

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.

• Using the modifier ghost in local-declarations (see section 13.1.1 Modifiers for Local Declarations).

• The possibly-annotated-loop statement (see section 13.2 Loop Statements), with a loop-invariant (see section 13.2.1 Loop Invariants). The redundant forms of loop-invariants, namely those that use the keywords maintaining_redundantly and loop_invariant_redundantly are level 1 features. Furthermore, the variant-function is a level 1 feature.

• The assert-statement (see section 13.3 Assert Statements). Note that the assert-redundantly-statement, which uses the keyword assert_redundantly, is in level 1.

• The non-redundant form of the assume-statement (see section 13.4.1 Assume Statements). Use of the keyword assume_redundantly is a level 1 feature.

• The set-statement (see section 13.4.2 Set Statements).

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].

• The \rep and rep ownership-modifiers (see section 18.2 Rep and Peer).

• The \peer and peer ownership-modifiers (see section 18.2 Rep and Peer).

### 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.

• Method or constructor declarations that use the modifier model (see section 7.1.1.2 Model Methods and Constructors). However, note that using model on a field declarations is a level 0 feature and that using model on a type declaration is a level 3 feature.

• import-declarations that use the modifier model (see section 5.2 Import Declarations).

• The modifier pure (see section 6.2.5 Pure).

• The modifier uninitialized (see section 6.2.11 Uninitialized).

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 use of redundant forms of loop-invariants (see section 13.2.1 Loop Invariants) namely those that use the keywords maintaining_redundantly and loop_invariant_redundantly. Non-redundant loop-invariants are in level 0.

• The possibly-annotated-loop statement (see section 13.2 Loop Statements), with a variant-function (see section 13.2.2 Loop Variant Functions).

• The assert-redundantly-statement (see section 13.3 Assert Statements); that is, assert statements that use the keyword assert_redundantly. The non-redundant assert-statements are a level 0 feature.

• The redundant form of the assume-statement (see section 13.4.1 Assume Statements); that is, assume statements that use the keyword assume_redundantly. The non-redundant assume-statements are a level 0 feature.

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 relational form of a represents-clause (see section 8.4 Represents Clauses). That is, a represents clause that uses \such_that. Note that the functional form of such represents clauses is a level 0 feature.

• The writable-if-clause clause (see section 8.8 Writable If Clauses).

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.

• The \real type (see section 19.2 \real).

• The modifiers code_bigint_math, code_java_math, code_safe_math, spec_bigint_math, spec_java_math, and spec_safe_math (see section 6.2.12 Math Modifiers).

### 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.

• The \readonly and readonly ownership-modifiers from the Universe type system (see section 18. Universe Type System). Note that the \peer and \rep modifiers are level 0 features.

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

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