fmrisc.ProgramExplorer.Syntax.Spec

Class ClassSpec

java.lang.Object

fmrisc.ProgramExplorer.Syntax.ASTBase

fmrisc.ProgramExplorer.Syntax.Program.ASTProgramBase

fmrisc.ProgramExplorer.Syntax.Program.ProgramAnnotationBase

fmrisc.ProgramExplorer.Syntax.Spec.SpecificationBase

fmrisc.ProgramExplorer.Syntax.Spec.ClassSpec

All Implemented Interfaces:

AST, ASTSource, ASTProgram, ProgramAnnotation, Specification

public final class ClassSpec
extends SpecificationBase

A class specification.

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	invariantKeyword

Method Summary

Methods

Modifier and Type	Method and Description
void	accept(ASTVisitor visitor) Accept visitor for a visit.
void	accept(ASTVisitorOld visitor) Accept visitor for a visit.
void	acceptChildren(ASTVisitor visitor) Accept visitor for a visit to the children of this node.
static ClassSpec	construct(java.lang.String text, ErrorStream error, SourcePosition pos) Construct class specification from denoted text.
Formula	getClassInvariant() Get class invariant.
void	setClassInvariant(Formula inv) Set class invariant.

Methods inherited from class fmrisc.ProgramExplorer.Syntax.Program.ProgramAnnotationBase

getPosition, getText, setPosition

Methods inherited from class fmrisc.ProgramExplorer.Syntax.ASTBase

accept, accept, print, printCore, toString, toStringCore

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface fmrisc.ProgramExplorer.Syntax.ASTSource

getPosition, setPosition

Methods inherited from interface fmrisc.ProgramExplorer.Syntax.AST

print, printCore, toString, toStringCore

Field Detail

invariantKeyword

public static final java.lang.String invariantKeyword

See Also:

Constant Field Values

Method Detail

construct

public static ClassSpec construct(java.lang.String text,
                  ErrorStream error,
                  SourcePosition pos)

Construct class specification from denoted text.

Parameters:

text - the text of the specification.

error - the stream for printing error messages

pos - the source position of the specification

Returns:

the class specification (null, if an error ocurred in parsing)

getClassInvariant

public Formula getClassInvariant()

Get class invariant.

Returns:

the class invariant (null, if none).

setClassInvariant

public void setClassInvariant(Formula inv)

Set class invariant.

Parameters:

inv - the class invariant (may be null).

accept

public void accept(ASTVisitorOld visitor)

Accept visitor for a visit.

Specified by:

accept in interface AST

Overrides:

accept in class SpecificationBase

Parameters:

visitor - the visitor who is accepted by this node.

accept

public void accept(ASTVisitor visitor)

Accept visitor for a visit.

Specified by:

accept in interface AST

Overrides:

accept in class SpecificationBase

Parameters:

visitor - the visitor who is accepted by this node.

acceptChildren

public void acceptChildren(ASTVisitor visitor)

Accept visitor for a visit to the children of this node.

Specified by:

acceptChildren in interface AST

Overrides:

acceptChildren in class ASTBase

Parameters:

visitor - the visitor who is accepted by the children of this node.