net.sourceforge.czt.vcg.z

Interface VCG<T,B>

Type Parameters:

T - subtype of Type2 determining the kind VCContext for VCs being generated as Pred

B - kind of bindinds to consider from VCContext (i.e. FSB or RREF, see VCContext)

All Known Implementing Classes:

AbstractVCG, DomainCheckerVCG, FeasibilityVCG, RefinementVCG

public interface VCG<T,B>

A Verification Condition Generator interface implemented by various tools to generate VC conjectures enforcing specific consistency properties of specifications. Known implementations are for domain checking (or well-formedness) conditions, feasibility of operations, and refinement simulations.

We make use of generic types to maximize reuse of structure, if with different underlying types. The generic type R is used by the VCs to determine what kind of term it's being used. It gets instantiated mostly to Pred terms. Generic T and B are used by the VCG context to enforce the meta-specification protocol to be used by the specific VCGs. See Feasibility and Refinement VCGs for an example.

Author:

Leo Freitas

Method Summary

Modifier and Type	Method and Description
void	addParentSectionToIgnore(String parent)
SectionManager	config() Sets up available options according to the section manager's configuration.
VCEnvAnn	createVCEnvAnn(net.sourceforge.czt.base.ast.Term term) VC calculation for the given term, presuming it is a ZSect, Para, Pred, Expr or Decl.
VCEnvAnn	createVCEnvAnn(ZSect term) Process the given Z section to generate VCs.
SectionManager	getManager()
SortedSet<String>	getParentsToIgnore() Returns a unmodifiable set of section names not being processed for VC generation.
VCCollector<T,B>	getVCCollector()
Class<? extends VCEnvAnn>	getVCEnvAnnClass()
boolean	isAddingTrivialVC()
boolean	isCheckingDefTblConsistency()
boolean	isConfigured() True whenever section manager and VC collectors are not null, if the configuration flag is set as well.
boolean	isProcessingParents()
boolean	isRaisingTypeWarnings()
void	reset()
void	setDefaultProperties(SectionManager manager)
void	setSectionManager(SectionManager manager)
void	typeCheck(String sectName, boolean sourceSect)

Method Detail

isConfigured

boolean isConfigured()

True whenever section manager and VC collectors are not null, if the configuration flag is set as well.

Returns:

sectManager_ != null && getVCCollector() != null && isConfigured_

config

SectionManager config()
               throws VCGException

Sets up available options according to the section manager's configuration. It does nothing if no section manager is available.

Returns:

underlying section manager properly configured, if needed (see isConfigured()).

Throws:

VCGException

setSectionManager

void setSectionManager(SectionManager manager)
                throws VCGException

Throws:

VCGException

setDefaultProperties

void setDefaultProperties(SectionManager manager)

reset

void reset()

getManager

SectionManager getManager()

getVCCollector

VCCollector<T,B> getVCCollector()

getVCEnvAnnClass

Class<? extends VCEnvAnn> getVCEnvAnnClass()

typeCheck

void typeCheck(String sectName,
               boolean sourceSect)
        throws VCGException

Throws:

VCGException

createVCEnvAnn

VCEnvAnn createVCEnvAnn(ZSect term)
                 throws VCGException

Process the given Z section to generate VCs. The result is a Z sections with the given Z section as its parent, and with generated VCs as conjectures for its paragraphs.

Parameters:

term - Z section to generate VCs

Returns:

Z section as a list of VC conjectures

Throws:

VCGException

createVCEnvAnn

VCEnvAnn createVCEnvAnn(net.sourceforge.czt.base.ast.Term term)
                 throws VCGException

VC calculation for the given term, presuming it is a ZSect, Para, Pred, Expr or Decl. The result is Z sections named uniquely with standard toolkits as its parents, and with VC conjectures for the term, if any. The result is a wrapped VCEnvAnn.

Parameters:

term - Z section to generate VCs

parents - list of parents for the on-the-fly section

Returns:

VC Z section as a list of VC conjectures

Throws:

VCGException

addParentSectionToIgnore

void addParentSectionToIgnore(String parent)

Parameters:

parent -

getParentsToIgnore

SortedSet<String> getParentsToIgnore()

Returns a unmodifiable set of section names not being processed for VC generation.

Returns:

isAddingTrivialVC

boolean isAddingTrivialVC()

isProcessingParents

boolean isProcessingParents()

isRaisingTypeWarnings

boolean isRaisingTypeWarnings()

isCheckingDefTblConsistency

boolean isCheckingDefTblConsistency()