Modifier and Type | Method and Description |
---|---|
static VirtualDirectory |
Presenter.present(ParamSymbol symbol,
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.
|
Modifier and Type | Method and Description |
---|---|
static Formula |
Normalization.postCondition(ParamSymbol method)
Get normalized postcondition of method (may be null).
|
static Formula |
Normalization.preCondition(ParamSymbol method,
boolean init)
Get normalized precondition of method (may be null).
|
Constructor and Description |
---|
Satisfies(ParamSymbol method,
StateType stype,
TaskFolder invariants,
java.util.Vector<TheorySymbol> theories,
Declaration[][] decls,
ErrorStream out)
Create a judgement processor.
|
Terminates(ParamSymbol method,
StateType stype,
TaskFolder tasks,
java.util.Vector<TheorySymbol> theories,
Declaration[][] decls,
ErrorStream out)
Create a termination judgement processor.
|
Modifier and Type | Class and Description |
---|---|
class |
ParamSymbols<S extends ParamSymbol>
A set of parameterized symbols.
|
class |
ParamSymbolTable<S extends ParamSymbol>
A table of parameterized symbols.
|
Modifier and Type | Class and Description |
---|---|
class |
ClassMethodSymbol
A symbol denoting a class method.
|
class |
ConstructorSymbol
A symbol denoting a class constructor.
|
class |
MethodSymbol
A symbol denoting a method.
|
class |
ObjectMethodSymbol
A symbol denoting an object method.
|
Modifier and Type | Method and Description |
---|---|
ParamSymbol |
Environment.getCurrentMethod()
Get symbol of current method.
|
ParamSymbol |
ParameterSymbol.getParamSymbol()
Get the entity to which the variable belongs.
|
Modifier and Type | Method and Description |
---|---|
java.util.Set<ParamSymbol> |
ParamSymbol.getCall()
Get the set of methods called by this method.
|
java.util.Set<ParamSymbol> |
ParamSymbol.getRecursion()
Get the set of methods (directly or indirectly) recursively called
by this method.
|
Modifier and Type | Method and Description |
---|---|
static ParameterSymbol |
ParameterSymbol.construct(ParamSymbol psymbol,
Parameter parameter,
TypeExpression type)
Construct parameter symbol.
|
void |
Environment.enterMethod(ParamSymbol msymbol)
Enter from class level the constructor/method level.
|
Modifier and Type | Method and Description |
---|---|
void |
ParamSymbol.setCall(java.util.Set<ParamSymbol> call)
Set the set of methods directly called by this method.
|
void |
ParamSymbol.setRecursion(java.util.Set<ParamSymbol> recursion)
Set the set of methods (directly or indirectly) recursively called
by this method.
|
Modifier and Type | Method and Description |
---|---|
void |
TopWindow.propagateCondition(ParamSymbol method,
Statement statement,
Formula formula,
boolean pre)
Propagate condition through method body.
|
void |
TopWindow.showMethodDetail(ParamSymbol symbol)
Show details of method body.
|
Modifier and Type | Method and Description |
---|---|
ParamSymbol |
CallStatement.getMethodSymbol()
Get symbol of called method.
|
Modifier and Type | Method and Description |
---|---|
void |
CallStatement.setMethodSymbol(ParamSymbol msymbol)
Set symbol of called method.
|
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.
|
static void |
TerminationTasks.register(ParamSymbol method,
StateType stateType,
Name[] stateVars,
Name[] stateExcs,
java.util.Vector<TheorySymbol> theories,
Declaration[][] decls,
ErrorStream out)
Register the construction of termination tasks for a given method.
|
static void |
MethodTasks.register(ParamSymbol method,
StateType stateType,
Name[] stateVars,
Name[] stateExcs,
java.util.Vector<TheorySymbol> theories,
Declaration[][] decls,
ErrorStream out)
Register the construction of tasks for a given method.
|
Constructor and Description |
---|
CorrectnessTask(ParamSymbol method,
java.io.File parent,
StateType stateType,
Name[] stateVars,
Name[] stateExcs,
java.util.Vector<TheorySymbol> theories,
Declaration[][] decls,
ErrorStream out)
Construct a partial correctness task for a given method.
|
FrameTask(ParamSymbol method)
Construct the task of checking the frame condition.
|
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.
|
SpecTask(ParamSymbol method,
boolean satisfiable,
StateType stateType,
java.util.Vector<TheorySymbol> theories,
Declaration[][] decls,
ErrorStream out)
Construct a task for validating a specification.
|
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.
|