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

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.

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

This document was generated by Gary Leavens on March, 16 2009 using texi2html