Uses of Interface
fmrisc.ProgramExplorer.Syntax.Program.Statement

Packages that use Statement

Package	Description
fmrisc.ProgramExplorer.InOut
fmrisc.ProgramExplorer.Judgements
fmrisc.ProgramExplorer.Parser
fmrisc.ProgramExplorer.Semantics
fmrisc.ProgramExplorer.SWT
fmrisc.ProgramExplorer.Syntax.Program
fmrisc.ProgramExplorer.Tasks

Uses of Statement in fmrisc.ProgramExplorer.InOut

Methods in fmrisc.ProgramExplorer.InOut with parameters of type Statement

Modifier and Type	Method and Description
static VirtualDirectory	Presenter.present(ParamSymbol symbol, Statement statement, Formula formula, boolean pre, java.util.Map<Statement,Formula> preMap, java.util.Map<Statement,Formula> postMap, int fontSize, int width, int port) Present method in a certain font size.
java.lang.String	Presenter.writeStatement(Statement stat) Write file for statement and statement formula.

Method parameters in fmrisc.ProgramExplorer.InOut with type arguments of type Statement

Modifier and Type	Method and Description
static VirtualDirectory	Presenter.present(ParamSymbol symbol, Statement statement, Formula formula, boolean pre, java.util.Map<Statement,Formula> preMap, java.util.Map<Statement,Formula> postMap, int fontSize, int width, int port) Present method in a certain font size.
static VirtualDirectory	Presenter.present(ParamSymbol symbol, Statement statement, Formula formula, boolean pre, java.util.Map<Statement,Formula> preMap, java.util.Map<Statement,Formula> postMap, int fontSize, int width, int port) Present method in a certain font size.

Constructors in fmrisc.ProgramExplorer.InOut with parameters of type Statement

Constructor and Description
ASTPrinterHTML(org.w3c.dom.Element parent, Presenter presenter, boolean radioButtons, Statement selected) Create printer which appends text to parent node and may create links to newly generated files in virtual directory.

Uses of Statement in fmrisc.ProgramExplorer.Judgements

Methods in fmrisc.ProgramExplorer.Judgements with parameters of type Statement

Modifier and Type	Method and Description
StatJudgement	Satisfies.derive(Statement C) Apply the judgement "se, Is, Vs |- C: F" to compute the specification F of command C and to generate proving tasks as a side effect (see Section 4.12 of "A Program Calculus", se, Is, Vs are not needed because identifiers have already been resolved to symbols).
Formula	Pre.derive(Statement C, Formula Q) Apply the judgement "se, Is, VS |- pre(C, Q) = P" to compute the precondition P of command C with respect to postcondition Q and to generate proving tasks as a side effect (see Section 4.11 of "A Program Calculus", se, Is, Vs are not needed because identifiers have already been resolved to symbols).
Formula	Post.derive(Statement C, Formula P) Apply the judgement "se, Is, VS |- post(C, P) = Q" to compute the postcondition Q of command C with respect to precondition P and to generate proving tasks as a side effect (see Section 4.12 of "A Program Calculus", se, Is, Vs are not needed because identifiers have already been resolved to symbols).
Formula	Terminates.derive(Statement C, ValueSymbol[] J, Formula F) Apply the judgement se, Is, Vs |- C |v J F to prove that command C terminates when executed in a state in which F[J] holds where J is a vector of free variables in F that denotes the measure of the recursive methods in Is that may be called in C (J may be null which indicates that the current method is not recursive).
static void	Propagator.execute(Statement C, Statement statement, Formula formula, boolean pre, java.util.Map<Statement,Formula> preMap, java.util.Map<Statement,Formula> postMap, Satisfies satisfies) Propagate condition through statement.

Method parameters in fmrisc.ProgramExplorer.Judgements with type arguments of type Statement

Modifier and Type	Method and Description
static void	Propagator.execute(Statement C, Statement statement, Formula formula, boolean pre, java.util.Map<Statement,Formula> preMap, java.util.Map<Statement,Formula> postMap, Satisfies satisfies) Propagate condition through statement.
static void	Propagator.execute(Statement C, Statement statement, Formula formula, boolean pre, java.util.Map<Statement,Formula> preMap, java.util.Map<Statement,Formula> postMap, Satisfies satisfies) Propagate condition through statement.

Uses of Statement in fmrisc.ProgramExplorer.Parser

Methods in fmrisc.ProgramExplorer.Parser that return Statement

Modifier and Type	Method and Description
Statement	MiniJavaParser.assertion()
Statement	MiniJavaParser.assigncore()
Statement	MiniJavaParser.assignment()
Statement	MiniJavaParser.block()
Statement	MiniJavaParser.breakstat()
Statement	MiniJavaParser.conditional()
Statement	MiniJavaParser.continuestat()
Statement	MiniJavaParser.emptystat()
Statement	MiniJavaParser.localvar()
Statement	MiniJavaParser.localvarcore()
Statement	MiniJavaParser.methodcall()
Statement	MiniJavaParser.returnstat()
Statement	MiniJavaParser.statement()
Statement	MiniJavaParser.throwstat()
Statement	MiniJavaParser.trycatch()

Methods in fmrisc.ProgramExplorer.Parser with parameters of type Statement

Modifier and Type	Method and Description
void	MiniJavaParser.annotateStatement(Statement tree, org.antlr.runtime.Token token, SourcePosition pos)

Uses of Statement in fmrisc.ProgramExplorer.Semantics

Methods in fmrisc.ProgramExplorer.Semantics that return types with arguments of type Statement

Modifier and Type	Method and Description
java.util.Map<Statement,Formula>	ParamSymbol.getPreMap() Get mapping of body statements to prestate knowledge.

Method parameters in fmrisc.ProgramExplorer.Semantics with type arguments of type Statement

Modifier and Type	Method and Description
void	ParamSymbol.setPreMap(java.util.Map<Statement,Formula> preMap) Set mapping of body statements to prestate knowledge.

Uses of Statement in fmrisc.ProgramExplorer.SWT

Methods in fmrisc.ProgramExplorer.SWT with parameters of type Statement

Modifier and Type	Method and Description
void	TopWindow.propagateCondition(ParamSymbol method, Statement statement, Formula formula, boolean pre) Propagate condition through method body.

Uses of Statement in fmrisc.ProgramExplorer.Syntax.Program

Subinterfaces of Statement in fmrisc.ProgramExplorer.Syntax.Program

Modifier and Type	Interface and Description
interface	LoopStatement The interface for loop statements

Classes in fmrisc.ProgramExplorer.Syntax.Program that implement Statement

Modifier and Type	Class and Description
class	AssertionStatement An assertion statement.
class	AssignCallStatement A method call statement with a result value assigned to a variable.
class	AssignmentStatement An assignment statement.
class	AssignNewStatement A constructor call statement with the result value assigned to a variable.
class	BlockStatement A block statement i.e.
class	BreakStatement A break statement.
class	CallStatement An method call statement.
class	ConditionalStatement A conditional statement with one or two branches.
class	ContinueStatement A continue statement.
class	DeclCallStatement A method call statement with a result value initializing a local variable.
class	DeclNewStatement A constructor call statement with a result value initializing a local variable.
class	EmptyStatement An empty statement (skip).
class	ForLoopStatement A for loop.
class	LoopStatementBase The base class for loop statements.
class	ReturnStatement A return statement with an optional return value.
class	StatementBase The base class for statements.
class	ThrowStatement A throw (exception statement)
class	TryCatchStatement A protected code block.
class	VariableStatement A local variable declaration
class	VoidCallStatement A method call statement without a result value.
class	WhileLoopStatement A while loop.

Fields in fmrisc.ProgramExplorer.Syntax.Program declared as Statement

Modifier and Type	Field and Description
Statement	ParamDeclarationBase.body
Statement	WhileLoopStatement.body
Statement	Handler.body
Statement	ForLoopStatement.body
Statement	TryCatchStatement.body
Statement	ConditionalStatement.elsestat
Statement	ForLoopStatement.init
Statement[]	BlockStatement.stats
Statement	ConditionalStatement.thenstat
Statement	ForLoopStatement.update

Methods in fmrisc.ProgramExplorer.Syntax.Program that return Statement

Modifier and Type	Method and Description
Statement	ParamDeclarationBase.getBody() Get body of declaration.
Statement	ParamDeclaration.getBody() Get body of declaration.

Methods in fmrisc.ProgramExplorer.Syntax.Program with parameters of type Statement

Modifier and Type	Method and Description
static ConstructorDeclaration	ConstructorDeclaration.construct(Identifier name, Parameter[] params, Statement body) Construction of a constructor declaration.
static ObjectMethodDeclaration	ObjectMethodDeclaration.construct(Identifier name, TypeExpression type, Parameter[] params, Statement body) Construction of an object method declaration
static ClassMethodDeclaration	ClassMethodDeclaration.construct(Identifier name, TypeExpression type, Parameter[] params, Statement body) Construction of a class method declaration
static ObjectMethodDeclaration	ObjectMethodDeclaration.construct(Identifier name, TypeExpression type, java.util.Vector<Parameter> params, Statement body) Construction of an object method declaration
static ClassMethodDeclaration	ClassMethodDeclaration.construct(Identifier name, TypeExpression type, java.util.Vector<Parameter> params, Statement body) Construction of a class method declaration
static ConstructorDeclaration	ConstructorDeclaration.construct(Identifier name, java.util.Vector<Parameter> params, Statement body) Construction of a constructor declaration.
static Handler	Handler.construct(Parameter param, Statement body) Construct an exception handler.
static BlockStatement	BlockStatement.construct(Statement[] stats) Construct a block statement
static TryCatchStatement	TryCatchStatement.construct(Statement body, Handler[] handlers) Construct a protected code block.
static ForLoopStatement	ForLoopStatement.construct(Statement init, ValueExpression cond, Statement update, Statement body) Construct a while loop.
static TryCatchStatement	TryCatchStatement.construct(Statement body, java.util.Vector<Handler> handlers) Construct a protected code block.
static WhileLoopStatement	WhileLoopStatement.construct(ValueExpression cond, Statement body) Construct a while loop.
static ConditionalStatement	ConditionalStatement.construct(ValueExpression cond, Statement thenstat, Statement elsestat) Construct a conditional statement.

Method parameters in fmrisc.ProgramExplorer.Syntax.Program with type arguments of type Statement

Modifier and Type	Method and Description
static BlockStatement	BlockStatement.construct(java.util.Vector<Statement> stats) Construct a block statement

Constructors in fmrisc.ProgramExplorer.Syntax.Program with parameters of type Statement

Constructor and Description
ParamDeclarationBase(Identifier name, Parameter[] params, Statement body) Construction of a constructor declaration.

Uses of Statement in fmrisc.ProgramExplorer.Tasks

Method parameters in fmrisc.ProgramExplorer.Tasks with type arguments of type Statement

Modifier and Type	Method and Description
static void	PreconditionTasks.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.

Constructors in fmrisc.ProgramExplorer.Tasks with parameters of type Statement

Constructor and Description
InvariantTask(ParamSymbol method, Statement stat, Formula goal, Formula invariant, SourcePosition pos, Formula cond, Formula body, java.io.File parent, StateType stateType, java.util.Set<VariableSymbol> variables, java.util.Set<ClassSymbol> exceptions, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct an invariant verification task.
TerminationTask(java.lang.String kind, ParamSymbol method, Formula goal, Statement stat, java.lang.String tag, java.io.File parent, StateType stateType, java.util.Set<VariableSymbol> variables, java.util.Set<ClassSymbol> exceptions, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct a termination verification task.