net.sourceforge.czt.vcg.z

Class AbstractVCCollector<T,B>

java.lang.Object

net.sourceforge.czt.vcg.z.AbstractVCCollector<T,B>

Type Parameters:

R -

All Implemented Interfaces:

net.sourceforge.czt.base.visitor.TermVisitor<Pred>, net.sourceforge.czt.util.Visitor<Pred>, VCCollector<T,B>

Direct Known Subclasses:

TrivialVCCollector

public abstract class AbstractVCCollector<T,B>
extends Object
implements VCCollector<T,B>

Abstract VCG for CZT terms. For unknown/unprocessed terms, it returns false as the generated VC (e.g., the most difficult one to discharge).

Author:

Leo Freitas

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	AbstractVCCollector()
	AbstractVCCollector(Factory factory) Creates a new instance of AbstractVCCollector

Method Summary

Modifier and Type	Method and Description
protected void	afterCalculateVC(VC<Pred> vc)
protected void	beforeCalculateVC(net.sourceforge.czt.base.ast.Term term, List<? extends InfoTable> tables)
protected abstract Pred	calculateVC(Para term)
VC<Pred>	calculateVC(net.sourceforge.czt.base.ast.Term term, List<? extends InfoTable> tables) Calculate the verification condition for a given term in the context of any available information tables.
protected DefinitionTable	getDefTable()
protected Dialect	getDialect() Visits the given term (e.g., term.accept(this)).
protected Factory	getFactory()
protected Logger	getLogger()
long	getVCCount()
VCGContext<T,B>	getVCGContext()
VCNameFactory	getVCNameFactory()
protected abstract VCType	getVCType(Pred vc)
protected Factory	getZFactory()
protected void	resetDefTable()
void	resetVCCount()
protected void	setVCGContext(VCGContext<T,B> c)
void	setVCNameFactory(VCNameFactory vcf)
protected void	stepVCCounter()
Pred	visitTerm(net.sourceforge.czt.base.ast.Term term) For terms in general, just assume nothing is known about them, hence their VC is the worst possible (i.e.

Methods inherited from class java.lang.Object

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

Methods inherited from interface net.sourceforge.czt.vcg.z.VCCollector

addedPara, createVC, getTransformer, visit

Constructor Detail

AbstractVCCollector

protected AbstractVCCollector()

AbstractVCCollector

public AbstractVCCollector(Factory factory)

Creates a new instance of AbstractVCCollector

Parameters:

factory -

Method Detail

getVCGContext

public VCGContext<T,B> getVCGContext()

Specified by:

getVCGContext in interface VCCollector<T,B>

setVCGContext

protected final void setVCGContext(VCGContext<T,B> c)

getFactory

protected Factory getFactory()

getVCNameFactory

public VCNameFactory getVCNameFactory()

Specified by:

getVCNameFactory in interface VCCollector<T,B>

setVCNameFactory

public final void setVCNameFactory(VCNameFactory vcf)

Specified by:

setVCNameFactory in interface VCCollector<T,B>

getLogger

protected Logger getLogger()

getDefTable

protected DefinitionTable getDefTable()

resetDefTable

protected void resetDefTable()

getZFactory

protected Factory getZFactory()

getVCCount

public long getVCCount()

Specified by:

getVCCount in interface VCCollector<T,B>

resetVCCount

public void resetVCCount()

Specified by:

resetVCCount in interface VCCollector<T,B>

stepVCCounter

protected void stepVCCounter()

getDialect

protected Dialect getDialect()

Visits the given term (e.g., term.accept(this)). It also must take care of default results in case of possibly null terms, as they appear within a properly parsed Z Spec(!)

Parameters:

term - term to visit

visitTerm

public Pred visitTerm(net.sourceforge.czt.base.ast.Term term)

For terms in general, just assume nothing is known about them, hence their VC is the worst possible (i.e. false). That means, if our implementation fails to recognise some term, it will always lead to a safe result (i.e. an impossible VC to prove!). An alternative implementation would be to raise an exception.

Specified by:

visitTerm in interface net.sourceforge.czt.base.visitor.TermVisitor<Pred>

Parameters:

term -

beforeCalculateVC

protected void beforeCalculateVC(net.sourceforge.czt.base.ast.Term term,
                                 List<? extends InfoTable> tables)
                          throws VCCollectionException

Throws:

VCCollectionException

afterCalculateVC

protected void afterCalculateVC(VC<Pred> vc)
                         throws VCCollectionException

Throws:

VCCollectionException

calculateVC

protected abstract Pred calculateVC(Para term)
                             throws VCCollectionException

Throws:

VCCollectionException

getVCType

protected abstract VCType getVCType(Pred vc)
                             throws VCCollectionException

Throws:

VCCollectionException

calculateVC

public VC<Pred> calculateVC(net.sourceforge.czt.base.ast.Term term,
                            List<? extends InfoTable> tables)
                     throws VCCollectionException

Calculate the verification condition for a given term in the context of any available information tables. These tables MUST come from the section manager of this collector. They could be, for instance, tables for definitions, operators, and other related conjectures. Runs the VC generation algorithms over the given term and definition table. The definition table is important in order to make sure the types of known names can be properly inspected. For instance, assuming expressions are ground (i.e., just names), the VC for domain checking "x \cup y" will ultimately depend on \cup being a total function or having the types of x and y within its domain. The definition table should contain such declared type information. If null is given, then applies$to will always be used.

Specified by:

calculateVC in interface VCCollector<T,B>

Parameters:

term -

tables -

Returns:

Throws:

VCCollectionException