Download Escjava2-Implementat..

Chapter 3: Status of JML features
15
public class A extends B /*@ weakly */
implements C /*@ weakly */, D /*@ weakly */ { ... }
[[[ Need a description of the semantics ]]]
• Status: Parsed and ignored by ESC/Java2.
• Differences from JML or Java: Parsed but ignored by ESC/Java2. This feature was
not present in ESC/Java.
3.5.4 final (Java)
• Description: A final class may not have subclasses.
• Status: This modifier is parsed and checked. It does not need any static checking.
• Differences from JML or Java: None.
3.5.5 abstract (Java)
• Description: A class must be declared abstract if it has abstract methods. An abstract
class may not be instantiated; only non-abstract subclasses of an abstract class may be
instantiated. All interfaces are by definition abstract; using the abstract modifier on
an interface has been deprecated.
• Status: This modifier is parsed and checked. It does not need any static checking.
• Differences from JML or Java: None.
3.5.6 strictfp (Java)
• Description: The strictfp modifier determines the semantics of floating point operations within the class so modified.
• Status: This modifier is parsed and typechecked. The static checker does not make
use of this information. [[[ Is it inherited, or does it just apply to the implementations
given in that class? If so, what about interfaces (maybe applies just to initializers in
interfaces)?]]]
• Differences from JML or Java: None.
3.5.7 static (Java)
• Description: static is a Java modifier that may be applied to classes and interfaces
that are members of enclosing classes.
• Status: Implemented.
• Differences from JML or Java: None.
3.6 Annotations pertinent to a class or interface
These annotations may appear anywhere a declaration within a class or interface may appear. They define specification-only ghost or model fields of the type and state specifications
that apply to the whole object (not just to individual methods).
3.6.1 Ghost fields
• Description: A ghost field is a field of the object that can hold a primitive value or
a reference to an object, but is used only in specifications. Its value is changed using