C.5  Method Specifications

Synopsis

Description This specification describes the observable behavior of a given method (class method, object method, or constructor) by the following clauses:

helper

This optional clause may be given for a constructor or an object method. It indicates that the method is a helper method that must not assume the as its precondition and need not ensure the class invariant as its postcondition.

assignable vars

This optional clause lists the variables vars that are visible in the scope of the declaration of the method (object and class variables of the current class, class variables of other classes, respectively variables that represent components of such variables, but not local variables of the method) and whose values may be changed by the execution of the method.

If the clause is omitted, the method must not modify any variable that is visible in the scope of the method declaration.

If the variable this is added to the clause, it indicates that all object variables of the current class may be modified.

A parameter of the current method may be only listed in the clause, if it denotes an array or an object; the clause then indicates that the contents of the array/object may be changed by the call of the method.

signals exceptions

This optional clause lists the types of the exceptions that may be thrown by the execution of the method (excluding “runtime exceptions” such as “division by zero” that may be thrown by the execution of primitive operations).

If the clause is omitted, the method must not throw any exception.

requires formula

This optional clause states that it is only legal to call the method in a state (the method’s “prestate”) that satisfies the given formula.

If the clause is omitted, the formula is considered as “true”, i.e. it is legal to call the method in any state.

diverges formula

This optional clause states that the method will terminate (by returning normally or by throwing an exception) when called in any legal state that satisfies also the negation of formula (i.e. the method is allowed to run forever when called in any legal state that satisfies formula).

If the clause is omitted, the formula is considered as “false”, i.e. the method must terminate when called in any legal prestate.

ensures formula

This optional clause states that, for every legal prestate of the method, every state in which the method terminates is only legal if it is related to the method’s prestate by formula.

If the clause is omitted, the formula is considered as “true”, i.e. the method may terminate with any poststate.

decreases term, …

This optional clause states that, for every call of the method in a legal state, the value of the a given term sequence decreases according to a well founded ordering. If the sequence consists of a single term, the term denotes a non-negative integer number which is decreased in every (directly or indirectly) recursive call of the method (such that chain of recursive method calls must eventually end). If the sequence has more than one elements, then the values of some term₁,…,term_i may remain the same while term_i+1 is decreased as described above (decreasing lexicographical ordering). If the clause is omitted, no default is assumed.

Pragmatics This specification is in essence modeled after the “light-weight” specification format of JML, the Java Modeling Language [4]; however, a fixed order is required and specific default values for missing clauses are given. Furthermore, the specification follows (not precedes) the method’s declaration header to emphasize that the specification appears in the scope of the parameters of the method.

If the clause decreases term is missing in a (directly or indirectly recursive) method, the termination of the method can be probably not proved.

If in an assignable clause specific components of an object (e.g. specific fields of the current object) are listed, the “frame condition” itself just verifies that only the object (e.g. this) is modified; however, the “postcondition” is appropriately extended to ensure that only the specified components of the object are modified.

In an assignable clause, parameters may be listed that denote objects or arrays. The RISC ProgramExplorer handles such parameters not as input parameters but as transient parameters that may have a new value after the call of the method (methods are allowed to update the components of such parameters, not to assign new values to them). Therefore e.g. also a method that sorts a given array in place may be appropriately analyzed and verified.