Previous article

Next article


Reasoning with specifications containing method calls and model fields

David R. Cok, B65 MC01816, Eastman Kodak Company, Research & Development Laboratories, Rochester, NY 14650-1816, USA

space ARTICLE

PDF Icon
PDF Version

Abstract

Allowing abstraction in program specifications increases modularity and comprehensibility and is as important in specifications as it is in the program itself; two such abstraction mechanisms are method invocations and model fields. However, method invocations do not map neatly into the first-order logics that are often used for assuring the correctness of specifications. One problem is translating specifications in a way that acknowledges the potential for exceptional behavior. Furthermore, translating model fields into verification conditions exposes the non-trivial interactions between frame conditions and the model representations. The ESC/Java2 tool has been able to achieve a practical translation of method invocations and model fields within the
design constraints of its parent tool, ESC/Java. Furthermore, the techniques used are applicable to other specification constructs such as generalized quantifiers.


1 INTRODUCTION

Research and practical capability in program verification is advancing significantly with the help of clearer semantics, evolution of languages and tools, and experience with industrial-scale software systems. One research thread in program verification combines (a) specifications indicating the intent of a program with (b) tools that check those specifications either dynamically at run-time or statically without needing to execute the program. Using method calls in specifications provides a level of abstraction and conciseness that promotes reading, writing and understanding specifications and will likely assist in their automated verification as well. However, method calls in specifications have not been widely supported and have unclear semantics in the light of potential exceptional behavior. ESC/Java [9, 10] is a successful, publicly available, static checker, but it does not allow such abstraction. This paper discusses the implementation of an extension to ESC/Java, called ESC/Java2 [7, 8], that allows the use of method calls in specifications, with a discussion of the difficulties caused by the possibility of exceptions or non-terminating behavior. With that accomplished, other programming language constructs can also be handled by the underlying prover. The approach described here is applicable to any source code translator interfacing with a prover that operates in a generic first-order logic.

Model fields [6, 17], though not present in Java itself, also provide a useful abstraction. They can be used to model the behavior of interfaces and abstract classes that do not have an implementation and they can be used to separate the public and private aspects of a class’s specification. However, model fields exhibit properties both of fields and of methods; the interactions of these properties lead to complications and potential logical inconsistencies.

The solutions described in this paper were implemented and tested using the Java Modeling Language[1], the ESC/Java2 tool, and its back-end theorem prover, Simplify[25, 28]. The Java Modeling Language, described in section 2, is a specific and fairly rich language for expressing specifications about Java programs; for example, it supports both method calls in annotations and model fields. ESC/Java2, introduced in section 3, is a tool that checks these specifications against the program’s implementation. Section 4 describes Simplify, the theorem prover used by ESC/Java2 to check the various logical conditions corresponding to the specifications. Section 5 describes a solution for translating method calls and issues arising from exceptional termination, with an example in the Appendix. The issues and implementation of model fields are described in section 6. Section 7 discusses applications to other specification language features and some outstanding issues. The paper ends with descriptions of some future work, related work and conclusions, and acknowledgements in sections 8-10.

2 THE JAVA MODELING LANGUAGE

The Java Modeling Language (JML) has by now been described in several publications [1, 16, 17] and that full description will not be repeated here. The discussion in this paper can be illustrated using simple preconditions and postconditions.

  • A behavior keyword introduces a specification case, which is a set of annotations controlled by a conjunction of one or more preconditions.
  • A requires keyword followed by a predicate declares a precondition for a method.
  • A ensures keyword followed by a predicate declares a postcondition for a method that holds when the method terminates normally.
  • A signals keyword declares a postcondition that holds if the method exits with the given exception.
  • A diverges keyword declares a condition that must be true of the program state at the time the method is called (the pre-state) if the method never terminates.
  • A assignable keyword declares a frame condition, namely those fields that may be assigned to (or modified) by a method.
  • The pure modifier indicates a method that has no side-effects on the program state.
  • The \result identifier denotes the return value of a method.
  • The \old identifier denotes an expression evaluated in the pre-state of a method.
  • The model modifier indicates a method or field that is defined in annotations only.
  • A represents clause indicates a constraint for the value of a model field.
  • The in and maps clauses define additional contents of a datagroup corresponding to a model field.
  • An assert statement indicates an annotation predicate that is to be verified at a given point in the program text.

Specifications are included in the text of a Java program by placing them in specially formatted comments, as shown in the figures. The syntax of the specification predicates follows Java closely. It excludes any operations that have side effects, such as the increment operator ++. Other operations, such as arithmetic and comparison operators, have the same syntax and semantics as in Java. In particular, specification predicates may include method calls, if those methods are designated pure; tools supporting JML can then check that the implementations of pure methods have no side-effects. Fig. 1 shows a class with specifications containing method invocations. In it the public specifications of public methods use pure public methods and not private implementation details. The combination of JML’s visibility modifiers, pure methods, datagroups, and model methods and fields allows a separation of public information from private implementation detail.

3 ESC/JAVA2

The ESC/Java2 tool [7, 8], an extension of ESC/Java [9, 10], implements the translation of Java programs and JML specifications into a target logic. ESC/Java was a pioneering tool in the application of static program analysis and verification technology to annotated Java programs. The tool and its built-in decision procedure operate automatically with reasonable performance. The program annotations needed are easily read, written and understood by those familiar with Java and are partially consistent with the syntax and semantics of the separate Java Modeling Language (JML) project [1, 19]. Consequently, the original ESC/Java was a research success and was also successfully used by other groups for a variety of case studies [11, 12].

The ESC/Java2 project extends ESC/Java and its long-term utility by addressing a number of issues.

  • ESC/Java2 fully parses current JML and Java 1.4, so it is compatible with the variety of tools that now work with JML specifications.
  • ESC/Java2 checks more of JML than did ESC/Java. For example, frame conditions were not checked in ESC/Java, but errors in frame conditions could cause the prover to reach incorrect conclusions. ESC/Java also lacked the ability to use methods or model fields in annotations, limiting the annotations to statements only about low-level representations.
  • ESC/Java2 provides ongoing distribution and maintenance. As companies were bought and research groups disbanded, there was no continuing development or support of ESC/Java; the tool was untouched for over two years and its source code was not available.

Figure 1: An example class with specifications containing method invocations.

The engineering goals of ESC/Java were to be automatic and useful in finding bugs and violations of program specifications. It was not designed to find all specification errors or to fully represent Java semantics. ESC/Java2 has continued that spirit, though some unsound aspects have been corrected.

It is important to note that ESC/Java does not incorporate an explicit notion of program state in the logical structure that represents the program. Instead, a singleassignment calculus represents new values of program variables by new identifiers in the logic. This simplifies the logic and makes it much easier to reason about variables that remain unchanged; however, it also adds difficulty to the translation of loops and of method calls used in annotations.

4 SIMPLIFY

ESC/Java2 and ESC/Java translate program source code into guarded commands, then into a single-assignment representation, and finally into verification conditions. These conditions are passed to an accompanying theorem prover that may judge them to be valid or invalid and may produce counterexamples to demonstrate invalidity. The tool used is Simplify [25, 28], which accepts verification conditions expressed in a first-order logic (including universal and existential quantification) with equality and untyped total functions, extended with a simple theory of arithmetic.

Simplify implements interacting and cooperating decision procedures for some subdomains of first-order logic, along with heuristics to handle quantification, in order to assess the satisfiability of a set of input formulas. In the context of a programming language, the prover has knowledge of numerical and boolean values and operators on those values. A base set of axioms describes the behavior of arrays, types, and the subtype relationship. Object identity corresponds to a simple equality relationship among untyped, uninterpreted constants. Object fields are modeled as arrays: a field named f is considered an array, and a field reference o.f is translated as the array reference f[o]. The various operators and built-in functions of Java are modeled as function terms.

5 TRANSLATING USES OF METHOD CALLS IN ANNOTATIONS

Method calls within annotations

The problem at hand is to translate specification expressions containing method calls into the target logic described above. Information about the behavior of a method resides in the specifications of the method being called. Thus, we need to translate the specifications of the called method in a manner similar to that used to translate the calling expression.

In some cases there exists an expression whose value is the result of the method call. For instance, if a method’s specifications have a postcondition of the form

then one could extract such an expression, at least under the preconditions for which the postcondition holds. That expression could then be substituted for the method call itself, after appropriate substitution of actual for formal arguments. This procedure does not work in general however. There may not be such an expression available. There may be more than one such expression available, requiring a prescient choice of the best one to substitute for the method call. In addition, the expression being substituted may contain other method calls that will themselves require substitution; the substitution procedure may not terminate if there is any recursive use of method calls in the annotations. Even without recursion, the depth of rewriting can create very large verification conditions (easily consuming 256MB on the ordinary but realistic sets of specifications contained in the JML library, in experiments with ESC/Java2).

Inlining the implementation of the called method is another approach. This can result in large, unwieldy verification conditions and does not work in the presence of either recursion or overriding methods. It also can lose natural relationships between identical subexpressions and complicates the logical predicates of a specification with the imperative constructs of a method body. Also, we would like to be able to reason about uses of methods without needing their implementations.

The approach most appropriate to modular reasoning and to the implementation inherited from ESC/Java is to define a new uninterpreted function in the logic corresponding to each pure method used in a specification. A naive translation of methods to function terms would translate a method call of sort() into a function term with no arguments, namely, (sort). This procedure encounters the following complications.

  • As will be obvious to any Java programmer, the argument list of the method must include the receiver object (this), if the method is not static.1 Thus a method call sort() in Java is translated into a term of the logic as (sort this). This allows a natural distinction between the method calls sort() and a.sort(). These are translated into the terms (sort this) and (sort a'), where a' is the translation of the programming language expression a. Reasoning about aliasing is naturally handled as well: if it is established, for example, that (EQ this a'), then (EQ (sort this) (sort a')) will immediately follow.
  • Secondly, the method implementation may use fields of the receiving object that are not listed in the argument list. The values of instance fields may be considered to be implicitly included by way of the this argument, but their values then depend on the current program state.
  • Most importantly, the semantics of equality among function terms is not appropriate to the reference semantics of an object-oriented language such as Java. Two function terms in the logic are equal if they have the same function symbol, the same number of arguments, and the arguments are pairwise equal. This definition of equality is fine for the immutable values of Java’s primitive types, but not for reference values. Reference values referring to the same object in different program states will test equal even though their internal states may be different, since the logic used does not contain a global memory model.

The translation procedure adopted here adds a state argument to the function representing a method; the value used for that function argument is a unique constant indicating the program state in which the method is being evaluated. It would be equivalent to use a different name for the new function (rather than the same name with a different state constant as argument) in each new context in which it was being invoked. Remember that a method used in an annotation must be pure; that is, it must not change the program state, at least in ways that are observed by the program.2 Consequently the pre- and post-conditions of the pure method may be evaluated in a common state. The state constant is uninterpreted; that is, it is not used in any context other than to distinguish different program states. With this procedure we can maintain the single-assignment mechanism adopted by ESC/Java, without introducing a full memory model into the logic, but still utilize a first-order logic for proof obligations. Having a representation of explicit state would enable a more concise translation, since then the assumptions about the behavior of methods could be universally quantified by a state variable. However, that would make for a more complex logic and in any case would be a different design than that adopted by ESC/Java and extended by ESC/Java2.

As uninterpreted values, the state constants serve simply to distinguish the values produced by different instances of method calls in annotations. In each case the single-assignment translation step ensures that each field and variable used in the pre- and postconditions of the method is translated with its current value in that state. Fields that are not mentioned in a frame condition (assignable or modifies clause) are presumed to be unchanged from state to state.

JML specifications are often partial. That is, the behavior of the method is not specified for all combinations of input. They may also be partial in the sense that there is no value of the type of the result for the given arguments (such as for division by 0). This is the case for conditions in which the method does not terminate or terminates with an exception.

On the other hand, functions in Simplify’s logic are total. The logical term introduced as the translation of a pure method will simply be undefined for those function arguments for which the JML specification does not normally terminate or the result is not specified. This is consistent with how partiality is handled elsewhere in JML [18]. However, this partiality of specification affects how the method should be translated and the deductions that can be inferred from its logical representation; this problem is discussed in the following section.

Handling abnormal termination

In JML, a method’s ensures postcondition states that (under the given precondition) if a method terminates normally, then the given predicate holds; the signals postcondition states that if the method terminates with the given exception, then its predicate holds. In JML’s semantics, if a method terminates with an exception or does not terminate at all, the result value is undefined. Thus, in order to reason about the use of a method call in an annotation, we must know when a method does terminate normally. That is, the assumption we need to generate for a method has the form

Figure 2: A class with a specification that includes normal, abnormal and nontermination conditions.

in which normalReturn(args) is true precisely when the method always returns normally for the given arguments. For those argument combinations for which the method might possibly not return normally, the result must be undefined.

Consider the code fragment of Fig. 2. Since the diverges predicate is false, we know that the method valueOfI will always terminate. Similarly, the signals clause states that if !(o == null) then the method will not terminate exceptionally. 3 Hence if !(o == null) the method will terminate normally; consequently the behavior of the method is defined by the assumption

In general, with predicates for the signals and diverges clauses, the generated assumption has the form

However, what if the user omits the signals clause, as in Fig. 3? The default for an absent signals clause is true, meaning that there is no restriction if the method terminates exceptionally. The corresponding assumption is

This assumption is trivially true and says nothing that defines the behavior of the valueOfI method.

Figure 3: An inadequately specified method. Method valueOfI may throw an IllegalArgumentException exception for any value of the argument.

It is not uncommon for a method’s specifications to omit the specification of exceptional behavior, as in Fig. 3. The specification writer is simply stating that as long as the method (or those it calls) does not throw exceptions, the result will satisfy the given postcondition. However, if a method that is used in an annotation does not provide signals and diverges clauses, the effect will be more significant. In that case, any combination of method arguments might result in non-normal termination. Thus the returned value of the method is undefined for any argument combination, and consequently no conclusion about the behavior of the method will be able to be drawn. Fortunately the result of omitting the signals clause will be that the postcondition of the init method (in the example here) will not be able to be established, rather than, say, silently stating that the method meets its specifications. However the naive specification writer might be puzzled at this behavior without some warning that the generated assumptions are trivially satisfied. In effect, for a method that is used in an annotation, a specification that omits a statement of exceptional and divergent behavior is too weak to be useful.

One might take the approach that a method used in an annotation is expected to terminate normally, at least for the preconditions under which it is called (referred to as implicit specification of exceptions). However, this is equivalent to assuming JML’s normal_behavior or signals (Exception) false; when a signals clause is missing. In contrast, the usual JML semantics is that a missing signals clause is equivalent to signals (Exception) true;.

An alternate approach4 is that a method declared pure, which must be the case for methods used in annotations, must always terminate normally, for any precondition, in addition to having no side effects. This avoids the problem with exceptional termination by definition, but significantly limits the Java methods that might otherwise be considered pure.

Another approach (called explicit specification of exceptions) would require that any method used in an annotation have a specification for its exceptional and divergent behavior, as is shown in Fig. 2. The result of the method in question will be undefined if the method does not terminate normally. Thus the specification must at least be detailed enough to preclude exceptional or divergent behavior under the circumstances in which the method is called. One can do this by stating the conditions under which no Exception will occur. If there is a predicate only for one particular exception type, there is still the possibility that for any argument some other exception might be thrown. A simple specification idiom might be that methods used in annotations only have normally terminating behavior (for the preconditions in which they are used in a specification); using JML’s normal_behavior specifications would accomplish this. This approach has the advantage of a clear semantics that is consistent with the current definition of JML; it has the disadvantage that specifications for methods used in annotations must be more detailed than they might otherwise be written.

The requirement of extra detail is mitigated by the following recent evolution of JML’s semantics. The default diverges clause is diverges false;. That is, an omitted diverges clause is interpreted as requiring termination. The defined default for an omitted signals clause is signals (Exception) true;, which allows an Exception to be thrown. On the other hand, ESC/Java5 uses the throws clause of the method declaration to define its default. ESC/Java and ESC/Java2 will only allow those exceptions to be thrown that are explicitly listed in the throws clause, not even permitting additional unchecked exceptions such as a RuntimeException. Thus if a method declaration has an empty throws clause, then (for ESCJava(2)) the default signals clause is signals (Exception) false; this is consistent with the desired behavior above, namely, a tight restriction on non-normal termination of the method. Recent discussions6 have proposed that JML adopt this same default behavior. In that case the explicit specification of exceptions will also be the natural default.

The translation procedure

The translation, then, consists of the following steps:
  • Select a unique function identifier for each method declaration in the program. A family of overriding method declarations have the same identifier. One could use distinct identifiers for different overriding methods and switch among them based on the dynamic type of the receiver argument. It appears, however, that using the same identifier for all members of an overriding family of methods and then adding tests on the dynamic type into each specification’s preconditions is a simpler design.
  • Define a unique state constant (distinct from all other constants) for each unique program state within a calling method’s implementation. A new state is created after every operation with a side-effect. In practice, state constants are only needed for those points in a program where an annotation containing a method call occurs.
  • Where a method call is used in an annotation expression, translate that method invocation into the logic as a function term. Use the unique identifier for the method as the function name. Include as arguments the translations of (a) the state constant for this program state, (b) the receiver object (if the method is not static), and (c) each of the actual arguments of the method call.
  • The specifications of the called method must be turned into assumptions about the behavior of the method. In the case of a family of overriding and overridden methods, the specifications must have an additional antecedent of the form (this instanceof T) for the type T in which the specification appears.
    • They are first desugared by combining preconditions and postconditions into stand-alone implications of the form ([27] describes the details):

– Recalling the discussion of exceptional postconditions above, we use as the composite predicate the expression

– Any instance of \result is replaced by an instance of the function term, with formal names for its arguments.

– The expression is enclosed in a universal quantification over its formal parameters.

Thus the specification (in a class named Z)

in a state with state constant stateX creates the assumption

Since values (e.g. of fields) are not extracted out of a memory model of a program state, there is no quantification over the state constant. Instead the assumption above is repeated with a different state constant in each context where the method is called; any free variables are translated in the context of that call. Also, recall that since the method being used in the annotation must be pure, the preconditions, diverges conditions, signals conditions, and normal postconditions are all evaluated in the same state.

  • A pure Java method m may be used in a Java program and in an annotation.
    A program fragment such as
    should be provable (as long as m is presumed to terminate normally and be deterministic), even without specific specifications about m’s result. In order to connect such use of a method call in an annotation with its use in the program, an implicit postcondition could be added to the method’s specification that equates the result of the method to the term representing the method (e.g. ensures \result == m(...)). This would add a corresponding assumption to the verification conditions about the result of a method call in the program source code. This assumption must not be used when the result is a fresh, newly allocated object. The usefulness of this assumption in other cases is being evaluated.
  • If the called method has no specifications, then no other assumptions are introduced describing the behavior of the method. This will limit the conclusions that can be drawn, because the only connection between the value of a method call in one program state and the value in another program state is the definition of the value through the method’s specifications.
  • JML allows annotations to appear in the body of a method as well; assert statements are one example. These are translated in the same way as pre- and postconditions; they simply use the appropriate state constant. Since loops are partially unrolled by ESC/Java, they can be handled without additional special treatment.

If there is more than one instance of the same method call within a given program state, those calls are translated in the same way, enabling the prover to identify their return values as equal (even in the absence of specifications). If a method call in the postcondition occurs within an argument of \old, indicating that it is to be evaluted in the pre-state, then it will be translated using the state constant for the pre-state.

Appendix A contains a discussion of the details of an actual example translation.

An issue: are pure methods deterministic?

Using method invocations within annotations raises another issue: what is the relationship between the results of two different invocations (in annotations) of a pure method that occur within the same program state?7 That is, can we assume that assert m() == m(); will succeed? The value of a method such as m() is constrained by the method’s postconditions but may not be constrained to a single value. Assuming that the assertion above will be true (if the value of m() is defined) corresponds to assuming that the method execution is deterministic and not dependent on hidden volatile variables. In most specification situations it would be quite difficult to specify straightforward behavior without this assumption. ESC/Java2 currently presumes such deterministic behavior for pure methods; it is easy to model non-determinism for non-pure methods.JML does not have syntax to distinguish deterministic and non-deterministic methods.

This distinction is only relevant to those methods used in annotations, since we want assertions such as the one above to be valid in annotations. Reasoning about Java methods themselves is performed using only the method’s explicit specifications.

One situation in which m() == m(); ought to be false is when m() returns a newly allocated object. The two invocations ought to produce two distinct instances of the appropriate type. Since the program state does change because of the method call, at least in that the heap is changed, one can debate whether m() ought to be considered pure. JML currently allows this fairly common situation to be considered pure; various functions (e.g. toString()) that return String objects are good examples of methods that are pure except for allocation and would not satisfy the above equality.

Figure 4: An example of the use of model fields.

6 TRANSLATING USES OF MODEL FIELDS IN ANNOTATIONS

Syntax

The syntax related to the declaration and use of model variables is shown in Fig. 4. Within annotations, field declarations can appear as model declarations. These fields simply represent values that are constrained by expressions or predicates given in represents clauses. A represents clause may appear in either the class or interface declaring a model field or in a subclass or subinterface.

Model field names may appear in assignable clauses. In that case the name stands for a set (a datagroup) containing field designations and the contents of other datagroups. A field may be declared as a member of a datagroup using the in or maps (not shown) declarations; datagroups may be extended in subtypes. In Fig. 4, the size model field is a member of the isEmpty datagroup, as well as automatically being a member of the size datagroup.

The specification of the method AbstractList.clear() declares that the method may change isEmpty and in fact ensures that its value is true when the method terminates. Since size is a member of the isEmpty datagroup, it also might be modified in the execution of clear(). In contrast, AbstractList.shrink() may modify size but may not modify isEmpty (so the second ensures clause for AbstractList.shrink() is redundant).

Interaction of frame conditions and model field representations

The implementation of model fields, pure methods, and checking of frame conditions in JML and ESC/Java has brought to the fore current problems in JML with the interactions between frame conditions and model fields. As shown in the example, model fields may be listed in frame conditions, either explicitly or implicitly as members of a listed datagroup, just as Java fields may be. If a model field is contained in the frame condition, its value may change during the execution of the method; if it is omitted from the frame condition, its value must not change during the execution of the method.

However, depending on the representation of the model field, its value may be affected by the values of fields that are not members of its datagroup and may not even be members of the class hierarchy that contains the model field. Changes to such fields may change the abstract value of the model field; the methods causing such changes may not even be aware of the existence of the model field in question and consequently will not list it in its modifies clause.

On the other hand, if a model field is specified as modifiable by the body of a method, we need to be able to reason about its changing value at each assignment or method call within the body of the method. A method call is accompanied by its own specifications. If those state the effect of the method call on the value of the model field, appropriate reasoning can be performed; if the method call’s specifications say nothing about the value of the model field after the call, then the resulting value of the model field will understandably be arbitrary. An assignment is analogous to a method call without specifications. The effect of an assignment on a concrete field is well known: only the concrete field assigned to is modified and all others are unchanged. But without some restriction on the model fields that might be affected by assignment to a particular concrete field, the value of a model field after the assignment is undetermined.

These issues, considering both soundness and modularity, have been discussed in more detail and addressed in previous and ongoing work, though the implementation of those results in JML and its related tools is not complete. Müller’s thesis[22] and a subsequent paper with Poetzsch-Heffter and Leavens[23] propose a universe type system and a concept of relevant locations to control visibility and use of concrete and model fields and to assign responsibility for reasoning about their modification.Implementation of the universe type system is underway in JML. It may also be possible to use JML’s syntax for defining datagroups to help specify relationships between fields and model values they affect; restrictions on the fields allowed in a represents clause may be desirable and even necessary.8 Two other relevant pieces of work have appeared since the original workshop presentation of this paper in 2004, that on Spec# [3] and further work on universe types to provide encapsulation that controls aliasing [24].

Verification conditions for model fields

JML and ESC/Java were designed to do modular specification and checking. Any representation clause for a particular model field may not be visible within the modules at hand; if it is visible, JML provides two forms: a functional representation and a predicate representation. Work on translation of model variables in JML for the LOOP tool occurred concurrently with the work in this paper and is discussed in [4]. That paper also translates model field representations as invariants but does not discuss the interaction with frame conditions outlined above.

Functional and predicate representations

JML denotes a functional representation by the syntax

There is a specific value, provided by the expression, for the model variable (in a given program state). This expression could be simply substituted for occurrences of the model field, as stated by Breunesse and Poll [4]. However, this is successful only in simple cases. If there is heavy use of model variables, the nested substitutions can be quite deep. Furthermore, JML allows multiple redundant representations, requiring a choice of which to use. Finally, direct or mutual recursion would prohibit simple substitution. It is simpler to translate such a representation in the same way as a predicate representation, generating an appropriate invariant for each represents clause.

JML also allows the values of model variables to be specified with a predicate representation:

In this case the predicate naturally implies an invariant; but it does not necessarily give an executable expression for the model variable and may not even constrain the model variable to a single value. As Breunesse and Poll point out, if there are no possible values satisfying the predicate, inconsistency in the generated assumptions can result, if appropriate care is not taken.

Non-assignable model fields

If a model variable is neither implicitly nor explicitly mentioned in a method’s assignable clauses9, then its value may not change during the course of the bodyof the method. Such a non-assignable model field is translated in the same way other fields are, as a simple variable or an array reference. No new variable names are needed as the program state changes since the value of the field is presumed not to change. If the model field has a represents clause, that representation implies an assumption about the value of the model field. We include that assumption in the pre-state assumptions. The assumption ought to be true in all states throughout the method’s execution. We currently do not check that this is true; a future enhancement should verify this presumption since otherwise inconsistent assumptions may be introduced, as discussed above.

Assignable model fields

If the model field is assignable within a method, then one must allow for different values at different states in the course of the method’s execution. In ESC/Java’s current translation scheme, this is easier to manage using a translation of the model field as a function term, with state and receiver arguments; this corresponds to the translation that would occur for a method call with no arguments, as discussed in section 5.

At each location where the model field is used, the assumptions generated from the represents clauses are also stated, so that they can be evaluated in the execution state at that point in the method’s execution. This corresponds to the introduction of the post-conditions of a method invocation that is used in an annotation.

Model fields with no representation

A model field, particularly in an abstract class or interface, may have no representation at all. It may be used in the specification of various methods, but its representation would be supplied by derived classes that implement the interface. Those representations are not necessarily visible within the classes seen by a method being checked when doing modular checking of specifications. Fig. 5 shows an example of such an interface. Another example is shown in Fig. 4, in which the model field AbstractList.size has no representation in AbstractList; it is given a representation in List in terms of the class representation supplied in that derived class. In this situation, an assignable model field is still translated as a method call, but
now there are no assumptions generated from represents clauses. Instead, only the pre- and post-conditions of methods whose specifications mention the model variable provide information about the behavior of the variable.

7 APPLICATION TO OTHER ANNOTATION CONSTRUCTS

With a mechanism for translating method calls to an underlying first-order logic implemented in ESC/Java2, some other specification constructs can be readily translated and used in static checking as well. These are described briefly in this section.

Figure 5: The specification and code for the interface NoRep, demonstrating a model field with no representation.

Constructor calls in annotations

Constructor calls in annotations can be treated as calls of static methods. That is, they do not depend on an implicit this argument. If they are constructors of a Java inner class, they will depend on an implicit argument representing an instance of the enclosing class. Since some of the arguments may be reference values, the translated function must also have a state constant as an argument. The assumptions about the constructed value are formed from the specifications of the constructor declaration.

Constructor calls are different than method calls in that they dynamically allocate new objects on the heap. Thus the result is a reference value not equal to any previous reference value. ESC/Java2 (following ESC/Java) provides axioms concerning allocation that ensure this behavior, but those are beyond the scope of this paper.

Array allocation in annotations

Translating expressions that allocate new arrays, such as new int[9], is quite straightforward. These expressions do not depend on the current state nor on any implicit receiver argument. Consequently a single function whose arguments include the dimensions of the array and the type of its elements is all that is needed. Just as for constructors, axioms regarding allocation are required, so that the value produced by a new array expression is known to be different than any previously produced reference value. Axioms about the dimensions, type, and initial values of the array are also needed. ESC/Java included such a function and axioms in its built-in axiom set, as does ESC/Java2.

Quantified expressions

Besides the usual universal and existential quantified expressions, JML also defines the generalized quantifiers \min, \max, \sum, \prod, and \num_of. For example, the value of the expression

is the smallest value of p(i) for i in the given range. The translation of each of these consists of syntactically replacing the expression with a skolemized function call (whose name is unique) and introducing appropriate assumptions about the function. Implicit receiver and state arguments are also needed, as described previously. If the quantifier is within the scope of another quantified expression, there will also need to be function arguments for any bound
variable used in the replaced expression.

One must also introduce assumptions concerning the value of this introduced function, corresponding to the value of the original quantified expression. For example, the assumptions associated with

are

and


with suitable universal quantification and where MIN(...) is replaced by the actual skolem function call expression.10

ESC/Java2 currently contains support for \min and \max. However, the axioms for \sum, \prod, and \num_of are most naturally expressed recursively; reasoning about them requires induction, which is not readily supported by Simplify.

Exceptional behavior

Constructor calls in annotations have the same problems with exceptional behavior as do method calls and they can be handled in the same way using the conventional specifications. However, quantified expressions and model variables both utilize expressions that may throw exceptions and neither have the syntax that method declarations have to specify the conditions under which exceptional behavior may or may not happen. How to handle exceptional behavior in these cases remains an unresearched question.

8 FUTURE WORK

Immutable values

The complication of introducing state constants as additional arguments is a result of the underlying logic using uninterpreted values for reference quantities in the programming language. Since these reference values refer to mutable objects, one must retain a state value to indicate which state of the object is meant. If all of the arguments were primitive type values such as integers and booleans, then a state value would not be needed. These values of non-reference types are immutable: if two values compare equal, they will always have the same properties in any program state.

Some reference types are also immutable. For example, objects of the class java.lang.String that compare equal (with either == or .equals()) will always have identical properties even in future program states. One requirement for the instances of a type to be immutable is that no method of the type modify the internal state of the instance; this condition is assured to hold if all methods of the type and any subtype are pure. However, it is also necessary for immutability that the internal representation not contain mutable objects and that the representation not be exposed in a way that the internal state could be modified by some external means.

Reasoning with immutable objects is potentially simpler and more efficient than with typical mutable objects. JML includes a library of classes representing mathematical concepts useful in specifying classes [18]; they are heavily used in the specification of JML code and sample classes and in JML’s specifications of Java classes. Checking these specifications might be more straightforward if it could be established that instances of these classes are immutable. For this to be possible, we need a set of sufficient conditions for immutability that can be statically checked, a proof of soundness regarding immutability, and a demonstration by a working implementation of the utility of immutable classes in program verification.

Proof management

When creating mathematical proofs, the resulting proof will usually be simpler, shorter and more understandable if one can work entirely with more abstract concepts (e.g. a Group or Sequence) and the theorems that have been established about them. Only when necessary will a mathematician resort to expanding the definitions of these abstract concepts and assembling the proof in terms of lower-level constructions. A similar situation arises in checking the verification conditions that are produced in the course of static checking of programs. One can write specifications using abstractions such as method calls and model fields. Those have definitions in terms of their implementations within classes or perhaps in terms of objects in JML’s mathematical library. All of the invariants and axioms for all of these higher and lower level constructions constitute a large set of logical conditions for a decision procedure to handle. Indeed, the introduction of abstraction mechanisms into ESC/Java2 has resulted in much larger sets of verification conditions being presented to Simplify. The problem is that Simplify simply matches terms that are equal, seeking to show unsatisfiability; it does not have heuristics to guide it to use primarily invariants concerning abstract concepts or to purposely “expand their definitions” in terms of implementation concepts. The need for such heuristics will become more important as automated checking of software programs tackles larger sets of software and seeks industrial-strength robustness in its results.

Methods and dynamic types

Method invocations in annotations are currently translated using the static type of the receiver. Sometimes more information about the receiver is known that would permit additional deductions. In Fig. 6, the assertions at lines A, B, and C can each be proved knowing only the static type of the receiver. The assertion at line D, however, requires the additional information that the dynamic type of the receiver is Sub; ESC/Java2 does not yet represent this information in the generated verification conditions.

Figure 6: An example showing the use of inherited specifications.

Specification language enhancements

As has been discussed above, this work with specification abstractions has pointed out areas in which specification languages such as JML may need enhancement.

  • JML needs a syntax and semantics to enable control and reasoning about which field assignments might modify (and which definitely do not modify) which model field values.
  • JML needs a way to distinguish deterministic from non-deterministic methods.
  • Specifications in JML need to adopt a style that precludes divergent or exceptional behavior for methods and related constructs used in annotations.

9 OTHER WORK AND CONCLUSIONS

There are by now several tools that statically check specifications against source code by logical reasoning. Java is a common but not the exclusive source language. The target logics and the accompanying provers vary widely: for example, Krakatoa [20] uses the Coq proof assistant, Jive [21] and LOOP [13, 15] use PVS [26], KeY [2] uses OCL and its own prover, and JACK [5] interfaces with Atelier B, Simplify, Coq and PVS.

It is also typical to carefully specify the mapping of the semantics of the source language into the target logic. However, definitions of the specification language are less common. The one example known to the author is the definition for the LOOP tool, which is not publicly available, of an early version of JML [15]. The LOOP tool has a comprehensive representation of Java’s memory model and the program translation and all work in PVS focuses directly on this model. The LOOP tool permits one to specify and reason about specifications that use pure methods. To do so, one either uses the specifications alone, in a manner similar to that which is described in this paper, or one uses the implementations of the methods and symbolically executes them within PVS. The latter approach is implied, for example, in [14], though it notes that the semantics of method invocations in specifications is still unclear. Similarly, Krakatoa defines all logical predicates in the context of a global heap; it also introduces a new assumption to encapsulate the behavior of pure methods. KeY allows simple query functions that do not cause exceptional behavior.

Though there are similar aspects among these approaches, the solution used by ESC/Java2 for translating method calls demonstrates a straightforward translation in the context of a general purpose first-order logic and prover. In doing so it maintains the design philosophy and usefulness of the original ESC/Java tool, while adding the capability of using method calls in annotations. The discussion above also illustrates the complexities of handling potentially non-normally terminating functions in a specification language. It appears that the tools above that handle method calls all implicitly use the implicit specification of exceptions of section 2. ESC/Java2 has been successfully using this approach in its recent alpha releases and is in the early stages of experimentation with the preferred explicit or default specifications.

A similar approach to that used for method calls can also be used for model fields, with an optimization available for model fields that are not modifiable within the method that uses them. However, there is an outstanding issue related to reasoning about model fields: how to know in a modular fashion which model fields, if any, might have their values changed by a given assignment statement.

10 ACKNOWLEDGMENTS

Thanks to Joseph Kiniry for comments on an early version of the paper and for some material on LOOP. Kiniry also is a partner in the support, maintenance and development of ESC/Java2. Thanks also to Gary Leavens for comments that improved the discussion overall, to Peter Müller for pointers and comments on previous work, as well as to the reviewers of both the precursor workshop (Formal Techniques for Java-like Programs, 2004) paper and this journal version. I am particularly grateful to those reviewers that took the time to provide detailed comments and suggestions.


Footnotes

1 Not quite as obviously, functions representing constructors of non-static inner classes must also include a reference to an object of the enclosing class as an argument.

2 Which changes are considered observable and how to control what is observed are matters of current research. JML currently does allow allocations of new objects to be performed by pure methods; the state issues regarding those allocations are already handled within the logic of ESC/Java by a separate ’allocation’ state variable.

3 JML only specifies exceptional behavior for those cases in which an object of type (or subtype of) java.lang.Exception is thrown. In particular, there are no assertions about behavior if a java.lang.Error is thrown. Other non-Exception Throwable objects are also ignored.

4 under discussion on the jmlspecs-interest mailing list at http://sourceforge.net/mail/?group_id=65346.

5 as I was reminded by a referee

6 since the original workshop presentation, on the jmlspecs-interest mailing list

7 Thanks to Peter Müller and Erik Poll for emphasizing the importance of determinism in using methods in specifications; additional discussion of this point and of possible JML syntax is present in the Jml-interest mailing group archives.

8 Private communications with Gary Leavens and Clyde Ruby related to Ruby’s in-progress thesis.

9 including not specified by a JML datagroup

10 The value of the quantified expression when the range predicate is empty is not handled here. JML currently defines this as the largest value of the type of the quantified expression for \min, and the smallest such value for \max. It might also be considered as undefined.

 

REFERENCES

[1] Many references to papers on JML can be found on the JML project website, http://www.cs.iastate.edu/~leavens/JML/papers.shtml.

[2] W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, R. Hähnle, W. Menzel, W. Mostowski, A. Roth, S. Schlager, and P. H. Schmitt. The KeY tool: Integrating object oriented design and formal verification. Software and System Modeling, Online First, 2004. http://www.sosym.org.

[3] M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. Presented at CASSIS 2004. To be published., May 2004.

[4] C.-B. Breunesse and E. Poll. Verifying JML specifications with model fields. In Formal Techniques for Java-like Programs. Proceedings of the ECOOP’2003 Workshop, pages 51–60, 2003. Technical Report 408, ETH Zurich.

[5] L. Burdy and A. Requet. JACK: Java applet correctness kit. In Proceedings, 4th Gemplus Developer Conference, Singapore, Nov. 2002.

[6] Y. Cheon, G. T. Leavens, M. Sitaraman, and S. Edwards. Model variables: Cleanly supporting abstraction in design by contract. Technical Report 03-10a, Department of Computer Science, Iowa State University, Sept. 2003. Available from http://archives.cs.iastate.edu/.

[7] D. R. Cok and J. Kiniry. ESC/Java2: Uniting ESC/Java and JML. Technical report, University of Nijmegen, 2004. NIII Technical Report NIII-R0413.

[8] D. R. Cok and J. Kiniry. ESC/Java2 : Uniting ESC/Java and JML. progress and issues in building and using ESC/Java2 and a report on a case study involving the use of ESC/Java2 to verify portions of an internet voting tally system. Lecture Notes in Computer Science, 3362:108–128, Jan. 2005.

[9] C. Flanagan, K. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, R. Stata, et al. The Extended Static Checker for Java, 1999. See http://research.compaq.com/SRC/esc/.

[10] C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI’02), volume 37, 5 of SIGPLAN, pages 234–245, New York, June 2002. ACM Press.

[11] E.-M. Hubbers. Integrating Tools for Automatic Program Verification. In M. Broy and A. Zamulin, editors, Proceedings of the Andrei Ershov Fifth International Conference Perspectives of System Informatics, volume 2890 of Lecture Notes in Computer Science, pages 214–221. Springer–Verlag, 2003. http://www.iis.nsk.su/psi03.

[12] E.-M. Hubbers, M. Oostdijk, and E. Poll. Implementing a Formally Verifiable Security Protocol in Java Card. In D. Hutter, G. Müller, W. Stephan, and M. Ullmann, editors, Proceedings of the First International Conference on Security in Pervasive Computing, volume 2802 of Lecture Notes in Computer Science, pages 213–226. Springer–Verlag, 2004. March 12–14, 2003, http://www.dfki.de/SPC2003/.

[13] B. Jacobs. Weakest precondition reasoning for Java programs with JML annotations. Journal of Logic and Algebraic Programming, 58:61–88, 2004.

[14] B. Jacobs, J. Kiniry, and M. Warnier. Java Program Verification Challenges. In F. S. de Boer, M. M. Bonsangue, S. Graf, and W.-P. de Roever, editors, Formal Methods for Components and Objects, volume 2852 of Lecture Notes in Computer Science, pages 202–219. Springer, Berlin, 2003.

[15] B. Jacobs and E. Poll. A logic for the Java Modeling Language JML. In H. Hussmann, editor, Fundamental Approaches to Software Engineering (FASE), volume 2029 of Lecture Notes in Computer Science, pages 284–299. Springer, 2001.

[16] G. T. Leavens, A. L. Baker, and C. Ruby. JML: A notation for detailed design. In H. Kilov, B. Rumpe, and I. Simmonds, editors, Behavioral Specifications of Businesses and Systems, pages 175–188. Kluwer Academic Publishers, Boston, 1999.

[17] G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06t, Iowa State University, Department of Computer Science, Dec. 2002. See http://www.jmlspecs.org.

[18] G. T. Leavens, Y. Cheon, C. Clifton, C. Ruby, and D. R. Cok. How the design of JML accommodates both runtime assertion checking and formal verification. In F. S. de Boer, M. M. Bonsangue, S. Graf, and W.-P. de Roever, editors, Formal Methods for Components and Objects: First International Symposium, FMCO 2002, Leiden, The Netherlands, November 2002, Revised Lectures, volume 2852 of Lecture Notes in Computer Science. Springer–Verlag, Berlin, 2003.

[19] G. T. Leavens, K. R. M. Leino, E. Poll, C. Ruby, and B. Jacobs. JML: notations and tools supporting detailed design in Java. In OOPSLA 2000 Companion, Minneapolis, Minnesota, pages 105–106. ACM, Oct. 2000.

[20] C. Marché, C. Paulin, and X. Urbain. The Krakatoa tool for JML/Java program certification. Available at http://krakatoa.lri.fr, 2003.

[21] J. Meyer, P. Müller, and A. Poetzsch-Heffter. The jive system—implementation description. Available at http://softech.informatik.uni-kl.de/old/en/publications/jive.html, 2000.

[22] P. Müller. Modular Specification and Verification of Object-Oriented Programs, volume 2262 of Lecture Notes in Computer Science. Springer-Verlag, 2002.

[23] P. Müller, A. Poetzsch-Heffter, and G. T. Leavens. Modular specification of frame properties in JML. Concurrency and Computation: Practice and Experience, 15:117–154, 2003.

[24] P. Müller, A. Poetzsch-Heffter, and G. T. Leavens. Modular invariants for layered object structures. Technical Report 424, ETH Zurich, Mar. 2005.

[25] C. G. Nelson. Techniques for Program Verification. PhD thesis, Stanford University, Stanford, CA 94035, 1980. Available from University Microfilms.

[26] S. Owre, S. Rajan, J. Rushby, N. Shankar, and M. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T. Henzinger, editors, Computer Aided Verification, number 1102 in Lecture Notes in Computer Science, pages 411–414. Springer, 1996.

[27] A. D. Raghavan and G. T. Leavens. Desugaring JML method specifications. Technical Report 00-03d, Iowa State University, Department of Computer Science, July 2003.

[28] Unpublished reports about Simplify are available online at http://research.compaq.com/SRC/esc/Simplify.html.

A AN EXAMPLE

This section shows an example translation of some simple code contrived to show concisely the translation of method invocations in annotations. The verification conditions shown in Fig. 8 are a subset of the formulae generated by the translation of the method m in the code of Fig. 7. The verification conditions have been rewritten from the internal language used by Simplify to an equivalent, but more readable, form using the syntax of conventional first-order logic. The various numerical suffixes are appended by the translation mechanism to create related but distinct names (the names typically contain an associated line number in the program text).

  • The ASSUME statement in line (2) of Fig. 8 states the assumption that the precondition in line A of Fig. 7 holds. Note the function form used to represent the call of Trans.p: it has the unique name Trans.p and it contains a state constant, this parameter, and the actual arguments of the call.
  • The assumption about the value of this call of Trans.p is provided in the ASSUME statement in line (1). It is quantified over the object and the two
    formal arguments of the method call. It makes the assumption that either b is true or the returned result is equivalent to whether the z field of the object c has the value 1 ; it also assumes that the type of the result is boolean. The same state constant is used in lines (1) and (2).

Figure 7: A somewhat contrived example to illustrate the translations of method calls.

  • The ASSERT at line (4) is the translation of the assert statement at line B.
  • The ASSUME at line (3) is the assumption associated with line (4) for the call of Trans.p in the assert statement at line B. There has been no change of state as yet, so the same state constant is used. In fact, this ASSUME is redundant with that in line (1) and could be omitted by an appropriate optimization.
  • The translation of line Q generates lines 5-7. Line (5) shows the assumption that equates the value of the function term Trans.p to a temporary variable
    (RES.18 ); this variable is the result of the method call within the program; in line (6) the method specifications are applied to that variable to state that the ensures predicate holds if the method returns normally; line (7) defines the new, post-assignment, value for the variable b (fields are expressed as arrays in Simplify’s logic). The Java assignment statement also causes a state change.
  • Lines (8) and (9) are the translation of the assert statement of line C. Note that both translations use the same, new state value as well as the new value of b.
  • Lines (10) and (11) are the translation of the assert statement of line E. There has been another state change and a new variable representing c (namely RES.20).
  • Finally, lines (12) and (13) represent the postcondition. Per JML’s semantics, it uses the value of b in the post-state, but the value of the formal argument c from the pre-state. In line (13), the precondition is evaluated with the pre-state state constant (state.pre) and the post-condition with the post-state state constant (state.20 ); state.pre and state are later equated (not shown).



Figure 8: A subset of the formulae generated from the translation of the code in Fig. 7. The nomenclature brokenObj is inherited from ESC/Java to help identify the object for which an assertion does not hold in a counterexample.

About the author



space Dr. David Cok received his Ph.D. in Physics from Harvard University and is currently Chief Technologist for the Photographic Center at the Kodak Research Lab. His research interests include image processing, image understanding, machine learning and optimization, as well as static tools for applying formal methods in industrial software development environments. He can be reached at david.cok@kodak.com.

Cite this article as follows: David R. Cok: ”Reasoning with specifications containing method calls and model fields”, in Journal of Object Technology, vol. 4, no. 8, Special Issue: ECOOP 2004 Workshop FTfJP, October 2005, pp. 77-103, http://www.jot.fm/issues/issues2005_10/article4


Previous article

Next article