fmrisc.ProgramExplorer.Semantics

Class TCCGenerator

java.lang.Object

fmrisc.ProgramExplorer.Semantics.TCCGenerator

public class TCCGenerator
extends java.lang.Object

A generator of type-checking conditions (tccs).

Constructor Summary

Constructors

Constructor and Description
TCCGenerator(TheorySymbol tsymbol, java.util.Vector<TheorySymbol> theories, LogicEnvironment env, java.io.File parent, ErrorStream out) Construct a type checking condition generator.

Method Summary

Methods

Modifier and Type	Method and Description
void	abort() Return to the parent context discarding all the assumptions and tasks that were added to the subcontext since the last call of open().
void	addTasks(TaskFolder folder) Add generated tasks to task folder and reset state.
void	assume(Formula formula) Create an assumption.
void	commit() Return to the parent context and add to it all the tasks that were created since the last call of open().
int	getDepth() Return depth of context stack.
void	open() Open a new subcontext.
void	prove(java.lang.String name, SourcePosition position, Formula formula, StateType resultType, Name[] stateVars, Name[] stateExcs) Create a new task to prove the given formula.
java.io.File	setDirectory(java.io.File parent) Set new parent directory for generating task directories.

Methods inherited from class java.lang.Object

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

Constructor Detail

TCCGenerator

public TCCGenerator(TheorySymbol tsymbol,
            java.util.Vector<TheorySymbol> theories,
            LogicEnvironment env,
            java.io.File parent,
            ErrorStream out)

Construct a type checking condition generator.

Parameters:

tsymbol - the theory in which the tcc generator operates.

theories - the list of all theories referenced in dependence order.

env - the environment holding the referenced declarations

parent - the directory used to create subdirectories for tcc tasks

out - a stream for printing messages

Method Detail

setDirectory

public java.io.File setDirectory(java.io.File parent)

Set new parent directory for generating task directories.

Parameters:

parent - the new parent directory.

Returns:

the old directory.

addTasks

public void addTasks(TaskFolder folder)

Add generated tasks to task folder and reset state.

Parameters:

folder - the folder to add the tasks to.

assume

public void assume(Formula formula)

Create an assumption.

Parameters:

formula - the formula representing the assumption.

prove

public void prove(java.lang.String name,
         SourcePosition position,
         Formula formula,
         StateType resultType,
         Name[] stateVars,
         Name[] stateExcs)

Create a new task to prove the given formula. The formula is also added to the current set of assumptions.

Parameters:

name - the name of the task

position - a related source position (may be null)

formula - the formula to be proved

resultType - the current result type (null, if none)

stateVars - the current state vars (null, if none)

stateExcs - the current state exceptions (null, if none)

open

public void open()

Open a new subcontext. Subcontexts may be arbitrarily nested; every subcontext must be ultimately either aborted or committed. If the subcontext is aborted, every task created in it is discarded. If the subcontext is committed, every task created in it is added to the parent context.

abort

public void abort()

Return to the parent context discarding all the assumptions and tasks that were added to the subcontext since the last call of open().

commit

public void commit()

Return to the parent context and add to it all the tasks that were created since the last call of open(). All assumptions added since the last call of open() are discarded.

getDepth

public int getDepth()

Return depth of context stack.