fmrisc.ProgramExplorer.Syntax.Spec

Class MethodSpec

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

All Implemented Interfaces:

AST, ASTSource, ASTProgram, ProgramAnnotation, Specification

public final class MethodSpec
extends SpecificationBase

A method specification.

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	divergesKeyword
static java.lang.String	exceptionsKeyword
static java.lang.String	postKeyword
static java.lang.String	preKeyword
static java.lang.String	terminationKeyword
static java.lang.String	variablesKeyword

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 MethodSpec	construct(java.lang.String text, ErrorStream error, SourcePosition pos) Construct method specification from denoted text.
Formula	getDivergesCondition() Get method diverges condition.
Name[]	getExceptions() Get list of exceptions that may be thrown by method.
Formula	getPostCondition() Get method postcondition.
Formula	getPreCondition() Get method precondition.
Term[]	getTerminationTerm() Get termination term vector.
Name[]	getVariables() Get method frame i.e.
boolean	isHelper() Get helper status of a method.
void	setDivergesCondition(Formula div) Set diverges condition.
void	setExceptions(java.util.Vector<Name> es) Set exceptions
void	setHelper(boolean helper) Set helper status of a method.
void	setPostCondition(Formula post) Set postcondition.
void	setPreCondition(Formula pre) Set precondition.
void	setTerminationTerm(java.util.Vector<Term> term) Set termination term.
void	setVariables(java.util.Vector<Name> vs) Set specification variables.

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

variablesKeyword

public static final java.lang.String variablesKeyword

See Also:

Constant Field Values

exceptionsKeyword

public static final java.lang.String exceptionsKeyword

See Also:

Constant Field Values

preKeyword

public static final java.lang.String preKeyword

See Also:

Constant Field Values

divergesKeyword

public static final java.lang.String divergesKeyword

See Also:

Constant Field Values

postKeyword

public static final java.lang.String postKeyword

See Also:

Constant Field Values

terminationKeyword

public static final java.lang.String terminationKeyword

See Also:

Constant Field Values

Method Detail

construct

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

getVariables

public Name[] getVariables()

Get method frame i.e. list of variables that may be modified by method.

Returns:

list of global variables modified by method (null, if none).

setVariables

public void setVariables(java.util.Vector<Name> vs)

Set specification variables.

Parameters:

vs - vector of variable names (may be null)

getExceptions

public Name[] getExceptions()

Get list of exceptions that may be thrown by method.

Returns:

list of exceptions that may be modified by method (null, if none).

setExceptions

public void setExceptions(java.util.Vector<Name> es)

Set exceptions

Parameters:

es - vector of exception names (may be null)

getPreCondition

public Formula getPreCondition()

Get method precondition.

Returns:

the method precondition (null, if none).

setPreCondition

public void setPreCondition(Formula pre)

Set precondition.

Parameters:

pre - the method precondition (may be null).

getDivergesCondition

public Formula getDivergesCondition()

Get method diverges condition.

Returns:

the method diverges condition (null, if none).

setDivergesCondition

public void setDivergesCondition(Formula div)

Set diverges condition.

Parameters:

div - the method diverges condition (may be null).

getPostCondition

public Formula getPostCondition()

Get method postcondition.

Returns:

the method postcondition (null, if none).

setPostCondition

public void setPostCondition(Formula post)

Set postcondition.

Parameters:

post - the method postcondition (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).

setHelper

public void setHelper(boolean helper)

Set helper status of a method.

Parameters:

helper - true iff the method is a helper.

isHelper

public boolean isHelper()

Get helper status of a method.

Returns:

true iff the method is a helper.

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.