T - subtype of Type2 determining the kind VCContext for VCs being generated as PredB - kind of bindinds to consider from VCContext (i.e. FSB or RREF, see VCContext)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.
| 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) |
boolean isConfigured()
SectionManager config() throws VCGException
isConfigured()).VCGExceptionvoid setSectionManager(SectionManager manager) throws VCGException
VCGExceptionvoid setDefaultProperties(SectionManager manager)
void reset()
SectionManager getManager()
VCCollector<T,B> getVCCollector()
void typeCheck(String sectName, boolean sourceSect) throws VCGException
VCGExceptionVCEnvAnn createVCEnvAnn(ZSect term) throws VCGException
term - Z section to generate VCsVCGExceptionVCEnvAnn createVCEnvAnn(net.sourceforge.czt.base.ast.Term term) throws VCGException
term - Z section to generate VCsparents - list of parents for the on-the-fly sectionVCGExceptionvoid addParentSectionToIgnore(String parent)
parent - SortedSet<String> getParentsToIgnore()
boolean isAddingTrivialVC()
boolean isProcessingParents()
boolean isRaisingTypeWarnings()
boolean isCheckingDefTblConsistency()
Copyright © 2003–2016 Community Z Tools Project. All rights reserved.