Uses of Class
fmrisc.ProgramExplorer.Judgements.StatJudgement

Packages that use StatJudgement

Package	Description
fmrisc.ProgramExplorer.InOut
fmrisc.ProgramExplorer.Judgements
fmrisc.ProgramExplorer.Semantics
fmrisc.ProgramExplorer.Syntax
fmrisc.ProgramExplorer.Syntax.Program

Uses of StatJudgement in fmrisc.ProgramExplorer.InOut

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

Modifier and Type	Method and Description
static void	PrettyPrinter.print(StatJudgement spec, int width, java.io.PrintWriter out) Print statement judgement.

Uses of StatJudgement in fmrisc.ProgramExplorer.Judgements

Methods in fmrisc.ProgramExplorer.Judgements that return StatJudgement

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).
StatJudgement	Satisfies.extendFrame(StatJudgement S, java.util.Set<VariableSymbol> vars) Extend judgement to the denoted set of modifiable variables.

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

Modifier and Type	Method and Description
StatJudgement	Satisfies.extendFrame(StatJudgement S, java.util.Set<VariableSymbol> vars) Extend judgement to the denoted set of modifiable variables.

Uses of StatJudgement in fmrisc.ProgramExplorer.Semantics

Methods in fmrisc.ProgramExplorer.Semantics that return StatJudgement

Modifier and Type	Method and Description
StatJudgement	ParamSymbol.getBodyJudgement() Get body statement judgement.

Methods in fmrisc.ProgramExplorer.Semantics with parameters of type StatJudgement

Modifier and Type	Method and Description
void	ParamSymbol.setBodyJudgement(StatJudgement bjudge) Set body statement judgement.

Uses of StatJudgement in fmrisc.ProgramExplorer.Syntax

Methods in fmrisc.ProgramExplorer.Syntax with parameters of type StatJudgement

Modifier and Type	Method and Description
void	ASTVisitor.visit(StatJudgement tree)
void	ASTPrinter.visit(StatJudgement spec)
void	ASTVisitorBase.visit(StatJudgement tree)

Uses of StatJudgement in fmrisc.ProgramExplorer.Syntax.Program

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

Modifier and Type	Method and Description
StatJudgement	Statement.getJudgement() Get command judgement.
StatJudgement	StatementBase.getJudgement() Get command judgement.
StatJudgement	VariableStatement.getJudgement() Get command judgement.

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

Modifier and Type	Method and Description
void	Statement.setJudgement(StatJudgement spec) Set command judgement.
void	StatementBase.setJudgement(StatJudgement judgement) Set command judgement.
void	VariableStatement.setJudgement(StatJudgement judgement) Set command judgement.