17. MultiJava Extensions to JML

This section describes extensions to JML to support the MultiJava [Clifton-etal00] language. All of these extensions are optional and are only used when an option (or special tool) is used to parse this syntax.

The sections below explain the extensions that MultiJava makes to JML.

17.1 Augmenting Method Declarations
17.2 MultiMethods

17.1 Augmenting Method Declarations

MultiJava has a feature, called "open classes" [Clifton-etal00] or "augmenting methods" that allows methods to be added to an existing class. It has the following syntax, which, in JML, permits method specifications.

multijava-top-level-declaration ::= multijava-top-level-method multijava-top-level-method ::= [ method-specification ] modifiers [ method ] [ type-spec ] extending-method-head method-body extending-method-head ::= name . ident formals [dims ] [ throws-clause ]

This syntax adds a method to the class named by the name in the extending-method-head.

The method must satisfy the given method-specification, if there is one.

17.2 MultiMethods

The other feature in MultiJava is multiple dispatch, which is used to define multimethods. Multiple dispatch is defined using the following syntax.

multijava-param-declaration ::= [ param-modifier ] ... type-spec specializer ident [ dims ] specializer ::= @ type-spec | @@ value-specializer value-specializer ::= expression

See the MultiJava paper [Clifton-etal00] for how the use of a specializer affects the meaning of method calls.