fmrisc.ProgramExplorer.Tasks

Class PreconditionTasks

java.lang.Object

fmrisc.ProgramExplorer.Syntax.ASTVisitorBase

fmrisc.ProgramExplorer.Tasks.PreconditionTasks

All Implemented Interfaces:

ASTVisitor

public final class PreconditionTasks
extends ASTVisitorBase

The tasks of proving that the preconditions of a method body are satisfied.

Method Summary

Modifier and Type	Method and Description
static void	generate(ParamSymbol method, java.util.Map<Statement,Formula> preMap, StateType stateType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct the precondition tasks for a given method.
void	visit(AssertionStatement stat)
void	visit(AssignmentStatement stat)
void	visit(BlockStatement stat)
void	visit(BreakStatement stat)
void	visit(CallStatement stat)
void	visit(ConditionalStatement stat)
void	visit(ContinueStatement stat)
void	visit(EmptyStatement stat)
void	visit(ForLoopStatement stat)
void	visit(ReturnStatement stat)
void	visit(ThrowStatement stat)
void	visit(TryCatchStatement stat)
void	visit(VariableStatement stat)
void	visit(WhileLoopStatement stat)

Methods inherited from class fmrisc.ProgramExplorer.Syntax.ASTVisitorBase

visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class java.lang.Object

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

Method Detail

generate

public static void generate(ParamSymbol method,
                            java.util.Map<Statement,Formula> preMap,
                            StateType stateType,
                            Name[] stateVars,
                            Name[] stateExcs,
                            java.util.Vector<TheorySymbol> theories,
                            Declaration[][] decls,
                            ErrorStream out)

Construct the precondition tasks for a given method.

Parameters:

method - the symbol of a method with a specification.

preMap - a mapping of body statements to pre-state knowledge.

stateType - the type of the current state (null, if none)

stateVars - the names of the modifiable variables (null, if none)

stateExcs - the names of the throwable exceptions (null, if none)

theories - the theories on which the following depend in dependence order.

decls - a sequence of declaration lists.

out - the stream to which to write error messages.

visit

public void visit(AssertionStatement stat)

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

visit

public void visit(AssignmentStatement stat)

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

visit

public void visit(BlockStatement stat)

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

visit

public void visit(BreakStatement stat)

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

visit

public void visit(ConditionalStatement stat)

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

visit

public void visit(ContinueStatement stat)

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

visit

public void visit(EmptyStatement stat)

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

visit

public void visit(ReturnStatement stat)

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

visit

public void visit(ThrowStatement stat)

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

visit

public void visit(TryCatchStatement stat)

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

visit

public void visit(VariableStatement stat)

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

visit

public void visit(WhileLoopStatement stat)

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

visit

public void visit(CallStatement stat)

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase

visit

public void visit(ForLoopStatement stat)

Specified by:

visit in interface ASTVisitor

Overrides:

visit in class ASTVisitorBase