fmrisc.Proving.CVCL
Class CVCLFormulaMask

java.lang.Object
  fmrisc.Proving.CVCL.CVCLFormulaMask

public final class CVCLFormulaMask
extends java.lang.Object

Constructor Summary

CVCLFormulaMask()
Create formula mask with initial context.

Method Summary

Expression	getFormula(Identifier mask) Get formula associated to mask identifier
Expression	getMask(Expression f) Mask a formula.
java.util.Collection	getSymbols() Return mask symbols generated since last call of resetSymbols().
void	resetSymbols() Reset collection of generated mask symbols.

Methods inherited from class java.lang.Object

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

Constructor Detail

CVCLFormulaMask

public CVCLFormulaMask()

Create formula mask with initial context.

Method Detail

getMask

public Expression getMask(Expression f)

Mask a formula.

Parameters:

f - a formula expression

Returns:

an expression that replaces the formula (either a reference or a reference application)

getFormula

public Expression getFormula(Identifier mask)

Get formula associated to mask identifier

Parameters:

mask - identifier of a mask

Returns:

formula expression to which mask is bound (null, if none)

resetSymbols

public void resetSymbols()

Reset collection of generated mask symbols.

getSymbols

public java.util.Collection getSymbols()

Return mask symbols generated since last call of resetSymbols().

Returns:

collection of ValueSymbol objects representing the mask symbols.