fmrisc.ProofNavigator.Semantics

Class Context

java.lang.Object

fmrisc.ProofNavigator.Semantics.Context

public final class Context
extends java.lang.Object

handling of formula contexts

Constructor Summary

Constructors

Constructor and Description
Context() construct a new context empty of assumptions

Method Summary

Modifier and Type	Method and Description
void	abort() return to the parent context discarding all the formulas that were added to the subcontext since the last call of open().
void	assume(Expression formula) add an assumption to the current (sub)context
void	close() close formula on top of formula stack with respect to current scope.
void	commit() return to the parent context and add to it all the formulas that were added to the subcontext since the last call of open().
Expression	getFormula() return the formula currently on the top of the stack
void	implies(Expression formula) conjoin formula to the current formula on the top of the stack
void	open() open a new subcontext subcontexts may be arbitrarily nested; every subcontext must be ultimately either aborted or commited.

Methods inherited from class java.lang.Object

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

Constructor Detail

Context

public Context()

construct a new context empty of assumptions

Method Detail

getFormula

public Expression getFormula()

return the formula currently on the top of the stack

Returns:

the formula on the top of the stack

assume

public void assume(Expression formula)

add an assumption to the current (sub)context

Parameters:

formula - the assumption to be added

implies

public void implies(Expression formula)

conjoin formula to the current formula on the top of the stack

Parameters:

formula - formula to be conjoined to top of stack

open

public void open()

open a new subcontext subcontexts may be arbitrarily nested; every subcontext must be ultimately either aborted or commited. if the subcontext is aborted, every formula created in it by implies() is discarded. if the subcontext is commited, every formula created in it by implies() is added to the parent context.

abort

public void abort()

return to the parent context discarding all the formulas that were added to the subcontext since the last call of open(). all assumptions added since the last call of open() are discarded.

commit

public void commit()

return to the parent context and add to it all the formulas that were added to the subcontext since the last call of open(). all assumptions added since the last call of open() are discarded.

close

public void close()

close formula on top of formula stack with respect to current scope.