fmrisc.ProgramExplorer.Semantics

Class ParamSymbol

java.lang.Object

fmrisc.ProgramExplorer.Semantics.SymbolBase

fmrisc.ProgramExplorer.Semantics.GlobalSymbolBase

fmrisc.ProgramExplorer.Semantics.ParamSymbol

All Implemented Interfaces:

GlobalSymbol, Symbol

Direct Known Subclasses:

ConstructorSymbol, MethodSymbol

public abstract class ParamSymbol
extends GlobalSymbolBase
implements GlobalSymbol

A symbol denoting a parameterized entity.

Method Summary

Modifier and Type	Method and Description
TypeExpression[]	getArgumentTypes() Get the argument types of the entity
StatJudgement	getBodyJudgement() Get body statement judgement.
java.util.Set<ParamSymbol>	getCall() Get the set of methods called by this method.
ClassSymbol	getClassSymbol() Get the class to which the entity belongs.
abstract ParamDeclaration	getDeclaration() Get declaration associated to symbol (may be null).
TaskFolder	getLoops() Get the loops.
TaskFolder	getObligations() Get the other proof obligations.
TaskFolder	getOptional() Get the optional conditions.
ParameterSymbol[]	getParameterArray() Get array of parameters of this object.
SymbolTable<ParameterSymbol>	getParams() Get the method's parameter set.
TaskFolder	getPreconditions() Get the preconditions.
java.util.Map<Statement,Formula>	getPreMap() Get mapping of body statements to prestate knowledge.
java.util.Set<ParamSymbol>	getRecursion() Get the set of methods (directly or indirectly) recursively called by this method.
Satisfies	getSatisfies() Get judgement processor for this method.
MethodSpec	getSpecification() Get method specification.
TaskFolder	getTCCs() Get the type checking conditions.
void	reset() Reset symbol
void	setBodyJudgement(StatJudgement bjudge) Set body statement judgement.
void	setCall(java.util.Set<ParamSymbol> call) Set the set of methods directly called by this method.
void	setPreMap(java.util.Map<Statement,Formula> preMap) Set mapping of body statements to prestate knowledge.
void	setRecursion(java.util.Set<ParamSymbol> recursion) Set the set of methods (directly or indirectly) recursively called by this method.
void	setSatisfies(Satisfies satisfies) Set judgement processor for this method.
void	setSpecification(MethodSpec spec) Set method specification.

Methods inherited from class fmrisc.ProgramExplorer.Semantics.GlobalSymbolBase

getLongName

Methods inherited from class fmrisc.ProgramExplorer.Semantics.SymbolBase

getName

Methods inherited from class java.lang.Object

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

Methods inherited from interface fmrisc.ProgramExplorer.Semantics.GlobalSymbol

getLongName

Methods inherited from interface fmrisc.ProgramExplorer.Semantics.Symbol

getName, print

Method Detail

getParams

public SymbolTable<ParameterSymbol> getParams()

Get the method's parameter set.

Returns:

the set of parameters.

getClassSymbol

public ClassSymbol getClassSymbol()

Get the class to which the entity belongs.

Returns:

the class of the symbol

getArgumentTypes

public TypeExpression[] getArgumentTypes()

Get the argument types of the entity

Returns:

the argument types.

getParameterArray

public ParameterSymbol[] getParameterArray()

Get array of parameters of this object.

Returns:

the array of parameters.

getDeclaration

public abstract ParamDeclaration getDeclaration()

Get declaration associated to symbol (may be null).

Specified by:

getDeclaration in interface Symbol

Overrides:

getDeclaration in class SymbolBase

Returns:

the declaration.

getTCCs

public TaskFolder getTCCs()

Get the type checking conditions.

Returns:

the folder holding the type checking conditions.

getLoops

public TaskFolder getLoops()

Get the loops.

Returns:

the folder holding the loop conditions.

getPreconditions

public TaskFolder getPreconditions()

Get the preconditions.

Returns:

the folder holding the preconditions.

getOptional

public TaskFolder getOptional()

Get the optional conditions.

Returns:

the folder holding the optional conditions.

getObligations

public TaskFolder getObligations()

Get the other proof obligations.

Returns:

the folder holding the other proof obligations.

reset

public void reset()

Reset symbol

setSpecification

public void setSpecification(MethodSpec spec)

Set method specification.

Parameters:

spec - the specification

getSpecification

public MethodSpec getSpecification()

Get method specification.

Returns:

the specification

setBodyJudgement

public void setBodyJudgement(StatJudgement bjudge)

Set body statement judgement.

Parameters:

bjudge - the body statement judgement.

getBodyJudgement

public StatJudgement getBodyJudgement()

Get body statement judgement.

Returns:

the body statement judgement.

setPreMap

public void setPreMap(java.util.Map<Statement,Formula> preMap)

Set mapping of body statements to prestate knowledge.

Parameters:

preMap - the mapping (may be null).

getPreMap

public java.util.Map<Statement,Formula> getPreMap()

Get mapping of body statements to prestate knowledge.

Returns:

the mapping (may be null).

setSatisfies

public void setSatisfies(Satisfies satisfies)

Set judgement processor for this method.

Parameters:

satisfies - the judgement processor.

getSatisfies

public Satisfies getSatisfies()

Get judgement processor for this method.

Returns:

the judgement processor (may be null)

setCall

public void setCall(java.util.Set<ParamSymbol> call)

Set the set of methods directly called by this method.

Parameters:

call - the call set.

getCall

public java.util.Set<ParamSymbol> getCall()

Get the set of methods called by this method.

Returns:

recursion the call set.

setRecursion

public void setRecursion(java.util.Set<ParamSymbol> recursion)

Set the set of methods (directly or indirectly) recursively called by this method.

Parameters:

recursion - the recursion set.

getRecursion

public java.util.Set<ParamSymbol> getRecursion()

Get the set of methods (directly or indirectly) recursively called by this method.

Returns:

recursion the recursion set.