fmrisc.ProgramExplorer.Syntax.Spec

Class LoopSpec

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

All Implemented Interfaces:

AST, ASTSource, ASTProgram, ProgramAnnotation, Specification

public final class LoopSpec
extends SpecificationBase

A loop specification.

Field Summary

Fields

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

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 LoopSpec	construct(java.lang.String text, ErrorStream error, SourcePosition pos) Construct loop specification from denoted text.
Formula	getLoopInvariant() Get loop invariant.
Term[]	getTerminationTerm() Get termination term vector.
void	setLoopInvariant(Formula inv) Set loop invariant.
void	setTerminationTerm(java.util.Vector<Term> term) Set termination term vector.

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

terminationKeyword

public static final java.lang.String terminationKeyword

See Also:

Constant Field Values

Method Detail

construct

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

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

getLoopInvariant

public Formula getLoopInvariant()

Get loop invariant.

Returns:

the loop invariant (null, if none).

setLoopInvariant

public void setLoopInvariant(Formula inv)

Set loop invariant.

Parameters:

inv - the loop invariant (may be null).

getTerminationTerm

public Term[] getTerminationTerm()

Get termination term vector.

Returns:

the loop termination term vector (null, if none).

setTerminationTerm

public void setTerminationTerm(java.util.Vector<Term> term)

Set termination term vector.

Parameters:

term - the loop termination term vector (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.