fmrisc.ProgramExplorer.Syntax.Spec

Class StatementSpec

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.StatementSpec

All Implemented Interfaces:

AST, ASTSource, ASTProgram, ProgramAnnotation, Specification

public final class StatementSpec
extends SpecificationBase

A statement specification.

Field Summary

Fields

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

Method Summary

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 StatementSpec	construct(java.lang.String text, ErrorStream error, SourcePosition pos) Construct method specification from denoted text.
Formula	getAssertion() Get pre-state assertion.
void	setAssertion(Formula ass) Set pre-state assertion

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

assertionKeyword

public static final java.lang.String assertionKeyword

See Also:

Constant Field Values

Method Detail

construct

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

Construct method 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 statement specification (null, if an error ocurred in parsing)

getAssertion

public Formula getAssertion()

Get pre-state assertion.

Returns:

the assertion (null, if none).

setAssertion

public void setAssertion(Formula ass)

Set pre-state assertion

Parameters:

ass - the assertion (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.