- calculate(Dialect, Type) - Method in class net.sourceforge.czt.vcg.util.CarrierSet
-
- calculateRefApplicationType(RefExpr) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
- calculateRefInitFinVCS(List<VC<Pred>>, ZName, ZName, ZName) - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCCollector
-
- calculateRefVCS(List<VC<Pred>>, ZName, ZName) - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCCollector
-
- calculateThmTable(String) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Calculate ThmTable for the VC ZSectName create on the fly
- calculateVC(Para) - Method in class net.sourceforge.czt.vcg.z.AbstractVCCollector
-
- calculateVC(Term, List<? extends InfoTable>) - Method in class net.sourceforge.czt.vcg.z.AbstractVCCollector
-
Calculate the verification condition for a given term in the context of
any available information tables.
- calculateVC(Para) - Method in class net.sourceforge.czt.vcg.z.dc.TrivialDCVCCollector
-
- calculateVC(Para) - Method in class net.sourceforge.czt.vcg.z.feasibility.TrivialFeasibilityVCCollector
-
- calculateVC(Para) - Method in class net.sourceforge.czt.vcg.z.TrivialVCCollector
-
- calculateVC(Term, List<? extends InfoTable>) - Method in interface net.sourceforge.czt.vcg.z.VCCollector
-
Calculate the verification condition for a given term in the context of
any available information tables.
- calculateVCEnv(Term) - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
Retrieves the ZSect VC Env for the given Term.
- calculateVCS(ZSect) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Creates the VC list for each paragraph within the given ZSect.
- calculateZSectVCEnv(ZSect) - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
Retrieves the ZSect VC Env for the given ZSect.
- CarrierSet - Class in net.sourceforge.czt.vcg.util
-
Calculates the carrier set of types.
- CarrierSet() - Constructor for class net.sourceforge.czt.vcg.util.CarrierSet
-
- CarrierSet(Factory) - Constructor for class net.sourceforge.czt.vcg.util.CarrierSet
-
- checkGlobalDef(String, Definition) - Static method in class net.sourceforge.czt.vcg.util.DefinitionTable
-
- checkInclBindingsWithinGivenSchBindings(ZName, ZName, SortedSet<Definition>) - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCCollector
-
- checkLocalDef(String, Definition) - Static method in class net.sourceforge.czt.vcg.util.DefinitionTable
-
- checkNeg(Pred) - Method in class net.sourceforge.czt.vcg.z.transformer.AbstractPredTransformer
-
- checkOpTableWithinListIfNeeded(List<? extends InfoTable>, boolean) - Static method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- checkOverallConsistency() - Method in class net.sourceforge.czt.vcg.util.DefinitionTable
-
- checkOverallConsistency(boolean) - Method in class net.sourceforge.czt.vcg.util.DefinitionTable
-
- checkPreviousState(String, ZName, ZName) - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCCollector
-
- checkSectionManager(String) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Checks whether there is a section manager or not, and raises the error
wrapped up as a CztException.
- checkStateBindings(String, ZName, BindingFilter) - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCCollector
-
Checks the given schema name in the definition table
- checkVCFileAndUpdateManager(String) - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- checkVCZSectConsistency(VCEnvAnn) - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
Makes sure the given VCEnvAnn is known within the underlying section manager,
and that its VC ZSect and original ZSect are also known.
- checkZStateInfo(AxPara) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
- cleanPossibleNameParameters(String) - Static method in class net.sourceforge.czt.vcg.util.AbstractVCNameFactory
-
- clear() - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCGContext
-
- clear() - Method in interface net.sourceforge.czt.vcg.z.VCGContext
-
- clearAddedPara() - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCCollector
-
- clearAddedPara() - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCCollector
-
- clearNecessaryTables() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- clearParentsToIgnore() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Clears both sets of parents to process and to ignore
- cloneTerm(T) - Static method in class net.sourceforge.czt.vcg.util.Definition
-
- collect(M...) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Collect all DC predicates from the terms within the given list.
- collectStateInfo(AxPara, Definition) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
Collects state information for the given AxPara, if it has one.
- collectStateInfo(AxPara, Definition) - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCCollector
-
- commandException(String, CommandException, String, boolean) - Static method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- compare(Definition, Definition) - Method in class net.sourceforge.czt.vcg.util.DefinitionComparator
-
- compareTo(Definition) - Method in class net.sourceforge.czt.vcg.util.Definition
-
- compareTo(CztError) - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- compute(String, SectionManager) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableService
-
Computes the definition table for the given ZSect and all its parents.
- computedBindings_ - Variable in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCCollector
-
- config() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Sets up available options according to the section manager's configuration.
- config() - Method in interface net.sourceforge.czt.vcg.z.VCG
-
Sets up available options according to the section manager's configuration.
- conj(UnificationEnv.UResult, UnificationEnv.UResult) - Static method in enum net.sourceforge.czt.vcg.util.UnificationEnv.UResult
-
A conjunction of two UResults.
- considerName(ZName) - Method in class net.sourceforge.czt.vcg.util.AfterBindings
-
- considerName(ZName) - Method in class net.sourceforge.czt.vcg.util.BeforeBindings
-
- considerName(ZName) - Method in interface net.sourceforge.czt.vcg.util.BindingFilter
-
- considerName(ZName) - Method in class net.sourceforge.czt.vcg.util.DashedBindings
-
- considerName(ZName) - Method in class net.sourceforge.czt.vcg.util.FinBindings
-
- considerName(ZName) - Method in class net.sourceforge.czt.vcg.util.InitBindings
-
- considerName(ZName) - Method in class net.sourceforge.czt.vcg.util.InputBindings
-
- considerName(ZName) - Method in class net.sourceforge.czt.vcg.util.OutputBindings
-
- considerName(ZName) - Method in class net.sourceforge.czt.vcg.util.StateBindings
-
Only allow numeric strokes
- create(Object[]) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCEnvAnn
-
- create(Object[]) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCEnvAnn
-
- create(Object[]) - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCEnvAnn
-
- createAxDefName(AxPara, String, String) - Method in class net.sourceforge.czt.vcg.util.DefaultVCNameFactory
-
- createCorrectnessVC(ZRefinementKind, Expr, Expr, Expr, Expr, Expr, Expr, Expr, Expr, Expr) - Method in class net.sourceforge.czt.vcg.z.transformer.refinement.ZPredTransformerRef
-
The various expressions involved in the VC for refinement.
- createDashedSchRef(ZName, ZNameList) - Method in class net.sourceforge.czt.vcg.z.transformer.feasibility.ZPredTransformerFSB
-
- createFeasibilityVC(ZRefinementKind, Expr, Expr, Expr, Expr, Expr, Expr) - Method in class net.sourceforge.czt.vcg.z.transformer.refinement.ZPredTransformerRef
-
Creates the feasibility VC predicate for refinement.
- createFinalisationOutputVC(ZRefinementKind, Expr, Expr, Expr) - Method in class net.sourceforge.czt.vcg.z.transformer.refinement.ZPredTransformerRef
-
- createFinalisationVC(ZRefinementKind, Expr, Expr, Expr) - Method in class net.sourceforge.czt.vcg.z.transformer.refinement.ZPredTransformerRef
-
- createGenericParamsRefExprs(ZNameList) - Method in class net.sourceforge.czt.vcg.z.transformer.feasibility.ZPredTransformerFSB
-
- createInitialisationInputVC(ZRefinementKind, Expr, Expr, Expr) - Method in class net.sourceforge.czt.vcg.z.transformer.refinement.ZPredTransformerRef
-
- createInitialisationVC(ZRefinementKind, Expr, Expr, Expr) - Method in class net.sourceforge.czt.vcg.z.transformer.refinement.ZPredTransformerRef
-
- createSchemaInclusion(Expr) - Method in class net.sourceforge.czt.vcg.z.transformer.feasibility.ZPredTransformerFSB
-
- createSchExpr(List<? extends Name>, Name, ZSchText) - Method in class net.sourceforge.czt.vcg.z.transformer.ZPredTransformer
-
For a zSchText (D | P) creates an \begin{schema}{schName}[genFormals] D \where P \end{schema}
- createSchRef(ZName, ZNameList) - Method in class net.sourceforge.czt.vcg.z.transformer.feasibility.ZPredTransformerFSB
-
- createSectionManager(Dialect) - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
This method should be called as few times as possible, as it returns
a brand new section manager .
- createSMKey(String, Class<K>) - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- createStateFinalisationVC(Expr, Expr) - Method in class net.sourceforge.czt.vcg.z.transformer.feasibility.ZPredTransformerFSB
-
- createStateInitialisationVC(Expr, Expr) - Method in class net.sourceforge.czt.vcg.z.transformer.feasibility.ZPredTransformerFSB
-
- createStateVCS(List<VC<Pred>>) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
- createUniqueName(String) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- createUniqueOnTheFlySchemaName() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- createUniqueZScectName() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- createVC(long, Para, VCType, Pred) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
- createVC(long, Para, VCType, Pred) - Method in class net.sourceforge.czt.vcg.z.TrivialVCCollector
-
- createVC(long, Para, VCType, Pred) - Method in interface net.sourceforge.czt.vcg.z.VCCollector
-
Given a paragraph and a VC, creates the underlying VC object.
- createVCCollectionException(String) - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCCollector
-
- createVCCollectionException(String, Throwable) - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCCollector
-
- createVCCollectionException(String) - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCCollector
-
- createVCCollectionException(String, Throwable) - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCCollector
-
- createVCConjPara(NameList, VC<Pred>) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Creates the ConjPara for the given VC.
- createVCConjPara(NameList, VC<Pred>) - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckerVCG
-
- createVCConjPara(NameList, VC<Pred>) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCG
-
- createVCEnvAnn(Term, List<? extends Parent>) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
VC calculation for the given term, presuming it is a ZSect, Para, Pred,
Expr or Decl.
- createVCEnvAnn(Term) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Create VCEnvAnn for term with on-the-fly ZSect with standard toolkit as parent.
- createVCEnvAnn(ZSect) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Process the given Z section to generate VCs.
- createVCEnvAnn(ZSect) - Method in interface net.sourceforge.czt.vcg.z.VCG
-
Process the given Z section to generate VCs.
- createVCEnvAnn(Term) - Method in interface net.sourceforge.czt.vcg.z.VCG
-
VC calculation for the given term, presuming it is a ZSect, Para, Pred,
Expr or Decl.
- createVCG() - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckUtils
-
- createVCG() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityUtils
-
- createVCG() - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementUtils
-
- createVCG() - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- createVCZSectHeader(String) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Creates a ZSect header as "\SECTION sectName_?? \parents sectName, ??" and with empty paragraphs
- createVCZSectPostcript(String, int, int) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- createVCZSectPreamble() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- createVCZSectPreamble() - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckerVCG
-
- createZNameAsString(ZName) - Static method in class net.sourceforge.czt.vcg.util.AbstractVCNameFactory
-
- cztException(String, CztException, String, boolean) - Static method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- cztExtensionDefault() - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- cztPathDefault() - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- generateVCS(ZSect, SectionManager) - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckerCommand
-
- generateVCS(ZSect, SectionManager) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityCommand
-
- generateVCS(ZSect, SectionManager) - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementCommand
-
- generateVCS(ZSect, SectionManager) - Method in class net.sourceforge.czt.vcg.z.VCGCommand
-
After parsing and type checking, generate VCs for the given zSect accordingly.
- genericType(Term) - Static method in class net.sourceforge.czt.vcg.util.UnificationEnv
-
- genParamType(Term) - Static method in class net.sourceforge.czt.vcg.util.UnificationEnv
-
- getAbbreviationName(AxPara) - Method in class net.sourceforge.czt.vcg.util.AbstractVCNameFactory
-
- getAbstractName() - Method in interface net.sourceforge.czt.vcg.z.refinement.util.ZRefinesAnn
-
- getAvailableSMTables() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- getAxDefName(AxPara) - Method in class net.sourceforge.czt.vcg.util.AbstractVCNameFactory
-
- getAxDefName(AxPara) - Method in class net.sourceforge.czt.vcg.util.DefaultVCNameFactory
-
- getBindingsFor(ZName) - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCCollector
-
Check whether bindings were already computed for the given name and
return a copy of them if so.
- getCarrierType() - Method in class net.sourceforge.czt.vcg.util.Definition
-
Carrier set, if available; null otherwise.
- getChildren() - Method in class net.sourceforge.czt.vcg.z.dc.DCVCEnvAnn
-
- getChildren() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCEnvAnn
-
- getColumn() - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- getCommand() - Static method in class net.sourceforge.czt.vcg.util.DefinitionTableService
-
- getCommand(SectionInfo) - Static method in class net.sourceforge.czt.vcg.util.DefinitionTableService
-
- getCommand() - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckUtils
-
Get a Command object for use in SectionManager
- getCommand() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityUtils
-
Get a Command object for use in SectionManager
- getCommand() - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementUtils
-
Get a Command object for use in SectionManager
- getCommand() - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
Get a Command object for use in SectionManager
- getCommandInfoType() - Static method in class net.sourceforge.czt.vcg.util.DefinitionTableService
-
- getConcreteName() - Method in interface net.sourceforge.czt.vcg.z.refinement.util.ZRefinesAnn
-
- getConjParaName(ConjPara) - Method in class net.sourceforge.czt.vcg.util.AbstractVCNameFactory
-
- getDCUtils() - Static method in class net.sourceforge.czt.vcg.z.dc.DomainCheckUtils
-
- getDefinitionKind() - Method in class net.sourceforge.czt.vcg.util.Definition
-
Tells you whether this name was declared via a constant
definition, or a variable declaration.
- getDefinitions(String) - Method in class net.sourceforge.czt.vcg.util.DefinitionTable
-
Get all the mapped definitions for a given section name.
- getDefinitionTable() - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- getDefName() - Method in class net.sourceforge.czt.vcg.util.Definition
-
- getDefTable() - Method in class net.sourceforge.czt.vcg.z.AbstractVCCollector
-
- getDescription() - Method in enum net.sourceforge.czt.vcg.z.feasibility.util.ZStateInfo
-
- getDialect() - Method in class net.sourceforge.czt.vcg.util.Definition
-
- getDialect() - Method in class net.sourceforge.czt.vcg.z.AbstractVCCollector
-
Visits the given term (e.g., term.accept(this)).
- getDialect() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- getDialect() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCGContext
-
- getDialect() - Method in interface net.sourceforge.czt.vcg.z.VCGContext
-
- getDomainCheckVCG() - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckUtils
-
- getErrors() - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- getErrorType() - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- getExceptions() - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- getExpr() - Method in class net.sourceforge.czt.vcg.util.Definition
-
For an equality definition (name==expr), this returns the
right-hand side of the definition, expr.
- getExtension() - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- getFactory() - Method in class net.sourceforge.czt.vcg.z.AbstractVCCollector
-
- getFactory() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- getFactory() - Method in interface net.sourceforge.czt.vcg.z.TermTransformer
-
- getFactory() - Method in class net.sourceforge.czt.vcg.z.transformer.AbstractTermTransformer
-
- getFeasibilityUtils() - Static method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityUtils
-
- getFeasibilityVCG() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityUtils
-
- getFileNameNoExt(String) - Static method in class net.sourceforge.czt.vcg.z.VCGUtils
-
For a file "./dir/foo.ext", returns "./dir/foo".
- getFreeParaName(FreePara) - Method in class net.sourceforge.czt.vcg.util.AbstractVCNameFactory
-
- getFSBVCCollector() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCG
-
- getFSBVCGContext() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
- getFSBVCNameFactory() - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCCollector
-
- getGenericName(Para) - Method in class net.sourceforge.czt.vcg.util.AbstractVCNameFactory
-
- getGenericName(Para) - Method in class net.sourceforge.czt.vcg.util.DefaultVCNameFactory
-
- getGenericParams() - Method in class net.sourceforge.czt.vcg.util.Definition
-
Returns the list of generic type parameters of this definition.
- getGenFormals() - Method in class net.sourceforge.czt.vcg.z.AbstractVC
-
- getGenFormals(Para, VC<Pred>) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- getGenFormals() - Method in interface net.sourceforge.czt.vcg.z.VC
-
- getGenParams() - Method in class net.sourceforge.czt.vcg.z.VCConfig
-
- getGivenParaName(GivenPara) - Method in class net.sourceforge.czt.vcg.util.AbstractVCNameFactory
-
- getInfo() - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- getInfo() - Method in class net.sourceforge.czt.vcg.z.AbstractVC
-
- getInfo() - Method in interface net.sourceforge.czt.vcg.z.feasibility.util.ZStateAnn
-
Returns the Info element.
- getInfo() - Method in interface net.sourceforge.czt.vcg.z.VC
-
- getInfoTables() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCGContext
-
- getInfoTables() - Method in interface net.sourceforge.czt.vcg.z.VCGContext
-
- getInitName() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCGContext
-
- getInitName() - Method in interface net.sourceforge.czt.vcg.z.VCGContext
-
Get the ZName for the state initialisation schema considered under this VCG context
- getLength() - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- getLine() - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- getLoc() - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- getLoc() - Method in class net.sourceforge.czt.vcg.z.AbstractVC
-
- getLoc() - Method in interface net.sourceforge.czt.vcg.z.VC
-
- getLocalDecls() - Method in class net.sourceforge.czt.vcg.util.Definition
-
- getLocation(ZName...) - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCCollector
-
- getLogger() - Method in class net.sourceforge.czt.vcg.z.AbstractVCCollector
-
- getLogger() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- getManager() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- getManager() - Method in interface net.sourceforge.czt.vcg.z.VCG
-
- getMessage(boolean) - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- getMessage() - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- getMessage() - Method in exception net.sourceforge.czt.vcg.z.VCGException
-
- getName() - Method in class net.sourceforge.czt.vcg.z.AbstractVC
-
- getName() - Method in interface net.sourceforge.czt.vcg.z.refinement.util.ZRefinesAnn
-
Returns the Name elements.
- getName() - Method in interface net.sourceforge.czt.vcg.z.VC
-
- getOnTheFlyZSectParents() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Default parents for on-the-fly ZSect to generate VC ZSect for.
- getOpBindings(ZName) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCGContext
-
- getOpBindings(ZName) - Method in interface net.sourceforge.czt.vcg.z.VCGContext
-
- getOpTable() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- getOpType(ZName) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCGContext
-
- getOpType(ZName) - Method in interface net.sourceforge.czt.vcg.z.VCGContext
-
For a given schema name representing an operation over the state schema,
return the
- getOriginalZSectName() - Method in class net.sourceforge.czt.vcg.z.VCEnvAnn
-
- getParentsToIgnore() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Returns a unmodifiable set of section names not being processed for VC generation.
- getParentsToIgnore() - Method in interface net.sourceforge.czt.vcg.z.VCG
-
Returns a unmodifiable set of section names not being processed for VC generation.
- getPrecedence() - Method in class net.sourceforge.czt.vcg.z.PredVC
-
- getPrecedence() - Method in class net.sourceforge.czt.vcg.z.VCConfig
-
- getPredTransformerFSB() - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCCollector
-
- getPredTransformerRef() - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCCollector
-
- getRefinementUtils() - Static method in class net.sourceforge.czt.vcg.z.refinement.RefinementUtils
-
- getRefinementVCG() - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementUtils
-
- getRefKind() - Method in interface net.sourceforge.czt.vcg.z.refinement.util.ZRefinesAnn
-
Returns the RefKind element.
- getRefKindDefault() - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCCollector
-
- getRefVCCollector() - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCG
-
- getSchBinding(ZName) - Static method in class net.sourceforge.czt.vcg.util.DefinitionKind
-
- getSchemaName(AxPara) - Method in class net.sourceforge.czt.vcg.util.AbstractVCNameFactory
-
- getSchExpr(ZName) - Static method in class net.sourceforge.czt.vcg.util.DefinitionKind
-
- getSchName() - Method in class net.sourceforge.czt.vcg.util.DefinitionKind
-
- getSectionInfo() - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- getSigSchemaName(ZName) - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCCollector
-
- getSigSchemaName(String) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCNameFactory
-
- getSigSchemaName(String) - Method in interface net.sourceforge.czt.vcg.z.feasibility.FSBVCNameFactory
-
Create a Schema signature name for given schema name
- getSource() - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- getSourceName(String) - Static method in class net.sourceforge.czt.vcg.z.VCGUtils
-
Get the CZT Source name from a given file.
- getSourcePara() - Method in class net.sourceforge.czt.vcg.z.VCSource
-
- getSourceVC() - Method in class net.sourceforge.czt.vcg.z.VCSource
-
- getSpecialBindings() - Method in class net.sourceforge.czt.vcg.util.Definition
-
Hide = null/old
Rename = new /old
- getStart() - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- getStateGenParams() - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCGContext
-
- getStateGenParams(ZStateInfo) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
- getStateName(ZStateInfo) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
- getStateName() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCGContext
-
- getStateName() - Method in interface net.sourceforge.czt.vcg.z.VCGContext
-
Get the ZName for the state schema considered under this VCG context
- getStateSchema(ZStateInfo) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
- getStateSchemaNames() - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCGContext
-
- getStateSchemas() - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCGContext
-
- getTermVisitor() - Method in interface net.sourceforge.czt.vcg.z.TermTransformer
-
Returns a visitor implementing a VCG protocol.
- getTermVisitor() - Method in class net.sourceforge.czt.vcg.z.transformer.AbstractTermTransformer
-
- getToolName() - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckUtils
-
Top-level CZT UI tool name.
- getToolName() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityUtils
-
Top-level CZT UI tool name.
- getToolName() - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementUtils
-
Top-level CZT UI tool name.
- getToolName() - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
Top-level CZT UI tool name.
- getTransformer() - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
- getTransformer() - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCCollector
-
- getTransformer() - Method in interface net.sourceforge.czt.vcg.z.VCCollector
-
- getTransitiveExceptions() - Method in exception net.sourceforge.czt.vcg.util.DefinitionException
-
- getType(Name, Stack<Stroke>) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- getType() - Method in class net.sourceforge.czt.vcg.z.AbstractVC
-
- getType() - Method in interface net.sourceforge.czt.vcg.z.VC
-
- getType() - Method in class net.sourceforge.czt.vcg.z.VCConfig
-
- getTypeId() - Method in enum net.sourceforge.czt.vcg.z.feasibility.ZFsbVCKind
-
- getTypeId(ZRefinementKind) - Method in enum net.sourceforge.czt.vcg.z.refinement.ZRefVCKind
-
- getTypes() - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- getUserDefinedSchemaPRE(ZName, ZNameList) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
User supplied predicate to be assumed as part of the given schema name
- getVC() - Method in class net.sourceforge.czt.vcg.z.AbstractVC
-
- getVC() - Method in interface net.sourceforge.czt.vcg.z.VC
-
- getVCCollector() - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckerVCG
-
- getVCCollector() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCG
-
- getVCCollector() - Method in interface net.sourceforge.czt.vcg.z.VCG
-
- getVCCount() - Method in class net.sourceforge.czt.vcg.z.AbstractVCCollector
-
- getVCCount() - Method in interface net.sourceforge.czt.vcg.z.VCCollector
-
- getVCEnvAnnClass() - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckerCommand
-
- getVCEnvAnnClass() - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckerVCG
-
- getVCEnvAnnClass() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityCommand
-
- getVCEnvAnnClass() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCG
-
- getVCEnvAnnClass() - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementCommand
-
- getVCEnvAnnClass() - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCG
-
- getVCEnvAnnClass() - Method in interface net.sourceforge.czt.vcg.z.VCG
-
- getVCEnvAnnClass() - Method in class net.sourceforge.czt.vcg.z.VCGCommand
-
After generating VCs, the result ZSect is type checked and its VCEnvAnn
added to the manager with a key according to this class.
- getVCFileName(String, String) - Static method in class net.sourceforge.czt.vcg.z.VCGUtils
-
For a file "./dir/foo.ext", returns "./dir/foosuffix.ext".
- getVCFileNameSuffix() - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckUtils
-
- getVCFileNameSuffix() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityUtils
-
- getVCFileNameSuffix() - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementUtils
-
- getVCFileNameSuffix() - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- getVCG() - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- getVCGContext() - Method in class net.sourceforge.czt.vcg.z.AbstractVCCollector
-
- getVCGContext() - Method in interface net.sourceforge.czt.vcg.z.VCCollector
-
- getVCGCreatedZSectTypeErrorWarningMessage(String, TypeErrorException) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCG
-
- getVCGCreatedZSectTypeErrorWarningMessage(String, TypeErrorException) - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCG
-
- getVCId() - Method in class net.sourceforge.czt.vcg.z.AbstractVC
-
- getVCId() - Method in interface net.sourceforge.czt.vcg.z.VC
-
- getVCName(Para, String, String) - Method in class net.sourceforge.czt.vcg.util.AbstractVCNameFactory
-
- getVCName(Para, String) - Method in class net.sourceforge.czt.vcg.util.AbstractVCNameFactory
-
For any given Z Paragraph, extract a meaningful name for this VC.
- getVCName(Para, String, String) - Method in class net.sourceforge.czt.vcg.util.DefaultVCNameFactory
-
- getVCName(Para, String) - Method in interface net.sourceforge.czt.vcg.util.VCNameFactory
-
Create a name for a VC related to the given Para.
- getVCNameFactory() - Method in class net.sourceforge.czt.vcg.z.AbstractVCCollector
-
- getVCNameFactory() - Method in interface net.sourceforge.czt.vcg.z.VCCollector
-
- getVCNameFactory() - Method in class net.sourceforge.czt.vcg.z.VCEnvAnn
-
- getVCPara() - Method in class net.sourceforge.czt.vcg.z.AbstractVC
-
- getVCPara() - Method in interface net.sourceforge.czt.vcg.z.VC
-
- getVCs() - Method in class net.sourceforge.czt.vcg.z.VCEnvAnn
-
- getVCSectDefaultParentsList() - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Returns the list of parents as a string of section names separated by SectionManager.SECTION_MANAGER_LIST_PROPERTY_SEPARATOR
- getVCSectDefaultParentsList() - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckerVCG
-
List of default parents for VC ZSect.
- getVCSectDefaultParentsList() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCG
-
List of default parents for VC ZSect.
- getVCSectDefaultParentsList() - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCG
-
List of default parents for VC ZSect.
- getVCSectionName(String) - Method in class net.sourceforge.czt.vcg.util.DefaultVCNameFactory
-
- getVCSectionName(String) - Method in interface net.sourceforge.czt.vcg.util.VCNameFactory
-
Creates a ZSect name to contains the various parts created during VCG, such
as NarrPara, AxPara (e.g., new schemas or axioms), and ConjPara of course.
- getVCSectName(String) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
VCSectName suffix.
- getVCSectName() - Method in class net.sourceforge.czt.vcg.z.dc.DCVCEnvAnn
-
- getVCSectName() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCEnvAnn
-
- getVCSectName() - Method in class net.sourceforge.czt.vcg.z.refinement.RefinementVCEnvAnn
-
- getVCSectName() - Method in class net.sourceforge.czt.vcg.z.VCEnvAnn
-
- getVCSectParents(String) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Creates a list of parents including the given section name, and all
those in the
AbstractVCG.getVCSectDefaultParentsList() (e.g., if it returns
"std_toolkit:mysect" and sectName is "xyz" the list will contain ("xyz", "std_toolkit", "mysect").
- getVCType(Pred) - Method in class net.sourceforge.czt.vcg.z.AbstractVCCollector
-
- getVCType(Pred) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
VC COLLECTOR METHODS
- getVCType(Pred) - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCCollector
-
VC COLLECTOR METHODS
- getZAbstractName() - Method in interface net.sourceforge.czt.vcg.z.refinement.util.ZRefinesAnn
-
This is a convenience method.
- getZConcreteName() - Method in interface net.sourceforge.czt.vcg.z.refinement.util.ZRefinesAnn
-
This is a convenience method.
- getZFactory() - Method in class net.sourceforge.czt.vcg.z.AbstractVCCollector
-
- getZSchTextPred(ZSchText) - Method in class net.sourceforge.czt.vcg.z.transformer.ZPredTransformer
-
Extract schema text predicates.
- GIVENSET - Static variable in class net.sourceforge.czt.vcg.util.DefinitionKind
-
- GIVENSET_VALUE - Static variable in class net.sourceforge.czt.vcg.util.DefinitionKind
-
- givenType(Term) - Static method in class net.sourceforge.czt.vcg.util.UnificationEnv
-
- parse(String, SectionManager) - Method in class net.sourceforge.czt.vcg.z.VCGCommand
-
Parse a given resource name with the section manager
- populateDeclList(ZDeclList, SortedSet<Definition>, boolean) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
- populateResultsToVCZSect(ZSect, List<VC<Pred>>) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Adds to the given VC Z section the list of VCs for each
corresponding paragraph as a conjecture paragraph.
- powerType(Term) - Static method in class net.sourceforge.czt.vcg.util.UnificationEnv
-
- predAsSchExpr(Pred) - Method in class net.sourceforge.czt.vcg.z.transformer.ZPredTransformer
-
Transforms a predicate into a (Sch)Expr (with empty Decl): P --> [ |P]
- PredVC - Class in net.sourceforge.czt.vcg.z
-
- PredVC(long, Para, VCType, Pred, String, VCConfig.Precedence, ZNameList) - Constructor for class net.sourceforge.czt.vcg.z.PredVC
-
- preferedMarkupDefault() - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- prePred(Expr) - Method in class net.sourceforge.czt.vcg.z.transformer.feasibility.ZPredTransformerFSB
-
- print(VCEnvAnn, Markup) - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
Prints the given VC ZSect environment in the given markup as a CZT string.
- printBenchmarkDefault() - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- printBenchmarks(int, long, SortedMap<String, List<Long>>) - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- printCollection(Collection<? extends Term>) - Static method in class net.sourceforge.czt.vcg.util.DefinitionTable
-
- printLocals(boolean) - Method in class net.sourceforge.czt.vcg.util.Definition
-
- printMap(SortedMap<ZName, SortedSet<Definition>>) - Static method in class net.sourceforge.czt.vcg.util.DefinitionTable
-
- printParseErrors(ParseException) - Static method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- printSpecialBindings(boolean) - Method in class net.sourceforge.czt.vcg.util.Definition
-
- printTerm(Term) - Static method in class net.sourceforge.czt.vcg.util.DefinitionTable
-
Uses a console print visitor to print the given term
- printToFile(VCEnvAnn, String, Markup) - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
Prints the given VC ZSect name as a file in the given path and given Markup.
- printToolDefaultFlagsUsage() - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckUtils
-
- printToolDefaultFlagsUsage() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityUtils
-
- printToolDefaultFlagsUsage() - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- printToolUsage() - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckUtils
-
- printToolUsage() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityUtils
-
- printToolUsage() - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- printTypeErrors(List<? extends ErrorAnn>) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Logs type ErrorAnn as warning if ERROR or if raising type checking warnings.
- printTypeErrors(TypeErrorException) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
- printTypeErrors(TypeErrorException) - Static method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- printUsage() - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
Print a usage message to System.err, describing the
command line arguments accepted by main.
- printVisitor_ - Static variable in class net.sourceforge.czt.vcg.util.DefinitionTable
-
console printing visitor
- processArg(String) - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckUtils
-
- processArg(String) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityUtils
-
- processArg(String) - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- processCollectedProperties() - Method in class net.sourceforge.czt.vcg.z.dc.DomainCheckUtils
-
- processCollectedProperties() - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityUtils
-
- processCollectedProperties() - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
- processConstDecl(ConstDecl, ZNameList, Stack<Stroke>, DefinitionKind) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
Add definition for the decl given with its underlying (power) type.
- processDeclList(ZNameList, List<Decl>, Stack<DefinitionKind>, Stack<Stroke>) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
Processes the expressions within the given declaration lists, where
a stack of strokes is carried along in order to enable processing DecorExpr.
- processDecorExpr(ZNameList, DecorExpr, Stack<Stroke>, Stack<DefinitionKind>) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- processInclDecl(InclDecl, ZNameList, Stack<Stroke>, Stack<DefinitionKind>) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- processRefExpr(ZNameList, RefExpr, Stack<Stroke>, Stack<DefinitionKind>) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
Processes given RefExpr as a SchExpr, if found.
- processRefName(ZNameList, ZName, Stack<Stroke>, Stack<DefinitionKind>) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
Look the reference name to see if already properly processed, raising
various errors in case it has not.
- processSchExpr(ZNameList, ZName, Expr, Stack<DefinitionKind>, Stack<Stroke>) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
Declares all the declared elements within a schema as its bindings, providing
expr is a SchExpr --- not yet handling complex schema expr.
- processVarDecl(VarDecl, ZNameList, Stack<Stroke>, DefinitionKind) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
Add a Definition for all names within a given VarDecl.
- prodType(Term) - Static method in class net.sourceforge.czt.vcg.util.UnificationEnv
-
- PROP_VCG_ADD_TRIVIAL_VC - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
When this property is true, the VCG will
add trivial (true, \forall x @ true and true) VCG predicates.
- PROP_VCG_ADD_TRIVIAL_VC_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
- PROP_VCG_APPLY_TRANSFORMERS - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
Each VCG tool could apply term transformers to generated VCs.
- PROP_VCG_APPLY_TRANSFORMERS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
- PROP_VCG_CHECK_DEFTBL_CONSISTENCY - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
Checks definition table information is consistent according to
the checkOverallConsistency() method.
- PROP_VCG_CHECK_DEFTBL_CONSISTENCY_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
- PROP_VCG_DOMAINCHECK_ADD_TRIVIAL_VC_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.dc.DomainCheckPropertyKeys
-
- PROP_VCG_DOMAINCHECK_APPLY_TRANSFORMERS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.dc.DomainCheckPropertyKeys
-
- PROP_VCG_DOMAINCHECK_PARENTS_TO_IGNORE_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.dc.DomainCheckPropertyKeys
-
- PROP_VCG_DOMAINCHECK_PREFERRED_MARKUP_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.dc.DomainCheckPropertyKeys
-
- PROP_VCG_DOMAINCHECK_PROCESS_PARENTS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.dc.DomainCheckPropertyKeys
-
- PROP_VCG_DOMAINCHECK_RAISE_TYPE_WARNINGS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.dc.DomainCheckPropertyKeys
-
- PROP_VCG_DOMAINCHECK_USE_INFIX_APPLIESTO - Static variable in interface net.sourceforge.czt.vcg.z.dc.DomainCheckPropertyKeys
-
When this property is true, whenever the domain checker
need to create \appliesTo predicates, it uses its infix version.
- PROP_VCG_DOMAINCHECK_USE_INFIX_APPLIESTO_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.dc.DomainCheckPropertyKeys
-
- PROP_VCG_FEASIBILITY_ADD_GIVENSET_VCS - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
When this property is true, the VCG will
add VC predicates to ensure given sets are non-empty.
- PROP_VCG_FEASIBILITY_ADD_GIVENSET_VCS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
- PROP_VCG_FEASIBILITY_ADD_TRIVIAL_VC_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
- PROP_VCG_FEASIBILITY_APPLY_TRANSFORMERS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
- PROP_VCG_FEASIBILITY_CREATE_ZSCHEMAS - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
When creating precondition for Z schemas, could generate VC as a
flat list of compact Z Schemas.
- PROP_VCG_FEASIBILITY_CREATE_ZSCHEMAS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
- PROP_VCG_FEASIBILITY_PARENTS_TO_IGNORE_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
- PROP_VCG_FEASIBILITY_PREFERRED_MARKUP_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
- PROP_VCG_FEASIBILITY_PROCESS_PARENTS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
- PROP_VCG_FEASIBILITY_RAISE_TYPE_WARNINGS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
- PROP_VCG_FEASIBILITY_ZSTATE_NAME - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
Z state schema name given by the user as a property or through \zstate
- PROP_VCG_FEASIBILITY_ZSTATE_NAME_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
- PROP_VCG_PARENTS_TO_IGNORE - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
When processing parent sections, it is useful to avoid certain
parents, like toolkits, which have stable / discharged VCs.
- PROP_VCG_PARENTS_TO_IGNORE_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
- PROP_VCG_PROCESS_PARENTS - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
When this property is true, the VCG will
process all the parent sections of the section being
processed, except for those set to be ignored.
- PROP_VCG_PROCESS_PARENTS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
- PROP_VCG_RAISE_TYPE_WARNINGS - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
Each processed section produce, for each VC kind being generated, a
new ZSection with its owner as a parent, where VCs reside.
- PROP_VCG_RAISE_TYPE_WARNINGS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
- PROP_VCG_REFINEMENT_ADD_GIVENSET_VCS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_ADD_TRIVIAL_VC_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_APPLY_TRANSFORMERS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_CONCRETE_STATE_NAME - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_CONCRETE_STATE_NAME_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_CREATE_ZSCHEMAS - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_CREATE_ZSCHEMAS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_IO - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_IO_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_KIND - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_PARENTS_TO_IGNORE_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_PREFERRED_MARKUP_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_PROCESS_PARENTS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_RAISE_TYPE_WARNINGS_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_REFKIND_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_RETRIEVE_NAME - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_RETRIEVE_NAME_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCG_REFINEMENT_ZSTATE_NAME_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- PROP_VCGU_LATEX_OUTPUT_WRAPPING_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
- PROP_VCGU_PREFERRED_MARKUP_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
- PROP_VCGU_PREFERRED_OUTPUT_MARKUP - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
When generating VCs from the AST in memory, we will use CZT printers.
- PROP_VCGU_PRINT_BENCHMARK - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
Top-level utility classes should print benchmark times for various
activities like parsing, type checking, and VCG times per file.
- PROP_VCGU_PRINT_BENCHMARK_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.VCGPropertyKeys
-
- value() - Method in class net.sourceforge.czt.vcg.util.DefinitionKind
-
Underlying value for a definition kind.
- valueOf(String) - Static method in enum net.sourceforge.czt.vcg.util.Definition.BindingType
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum net.sourceforge.czt.vcg.util.UnificationEnv.UResult
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum net.sourceforge.czt.vcg.z.dc.DCVCCollector.ApplType
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum net.sourceforge.czt.vcg.z.feasibility.util.ZStateInfo
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum net.sourceforge.czt.vcg.z.feasibility.ZFsbVCKind
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum net.sourceforge.czt.vcg.z.refinement.util.ZRefinementKind
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum net.sourceforge.czt.vcg.z.refinement.ZRefVCKind
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum net.sourceforge.czt.vcg.z.VCConfig.Precedence
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum net.sourceforge.czt.vcg.z.VCType
-
Returns the enum constant of this type with the specified name.
- values() - Static method in enum net.sourceforge.czt.vcg.util.Definition.BindingType
-
Returns an array containing the constants of this enum type, in
the order they are declared.
- values() - Static method in enum net.sourceforge.czt.vcg.util.UnificationEnv.UResult
-
Returns an array containing the constants of this enum type, in
the order they are declared.
- values() - Static method in enum net.sourceforge.czt.vcg.z.dc.DCVCCollector.ApplType
-
Returns an array containing the constants of this enum type, in
the order they are declared.
- values() - Static method in enum net.sourceforge.czt.vcg.z.feasibility.util.ZStateInfo
-
Returns an array containing the constants of this enum type, in
the order they are declared.
- values() - Static method in enum net.sourceforge.czt.vcg.z.feasibility.ZFsbVCKind
-
Returns an array containing the constants of this enum type, in
the order they are declared.
- values() - Static method in enum net.sourceforge.czt.vcg.z.refinement.util.ZRefinementKind
-
Returns an array containing the constants of this enum type, in
the order they are declared.
- values() - Static method in enum net.sourceforge.czt.vcg.z.refinement.ZRefVCKind
-
Returns an array containing the constants of this enum type, in
the order they are declared.
- values() - Static method in enum net.sourceforge.czt.vcg.z.VCConfig.Precedence
-
Returns an array containing the constants of this enum type, in
the order they are declared.
- values() - Static method in enum net.sourceforge.czt.vcg.z.VCType
-
Returns an array containing the constants of this enum type, in
the order they are declared.
- VC<R> - Interface in net.sourceforge.czt.vcg.z
-
- VCCollectionException - Exception in net.sourceforge.czt.vcg.z
-
TODO: should it include underlying VC?
- VCCollectionException(Dialect, String) - Constructor for exception net.sourceforge.czt.vcg.z.VCCollectionException
-
Creates a new instance of VCGException
- VCCollectionException(Dialect, String, Throwable) - Constructor for exception net.sourceforge.czt.vcg.z.VCCollectionException
-
- VCCollectionException(Dialect, Throwable) - Constructor for exception net.sourceforge.czt.vcg.z.VCCollectionException
-
- VCCollectionException(Dialect, String, String, Throwable) - Constructor for exception net.sourceforge.czt.vcg.z.VCCollectionException
-
- VCCollector<T,B> - Interface in net.sourceforge.czt.vcg.z
-
Interface characterising VC collection semantics for CZT Terms.
- VCConfig - Class in net.sourceforge.czt.vcg.z
-
- VCConfig(String, VCConfig.Precedence) - Constructor for class net.sourceforge.czt.vcg.z.VCConfig
-
- VCConfig(String, VCConfig.Precedence, ZNameList) - Constructor for class net.sourceforge.czt.vcg.z.VCConfig
-
- VCConfig.Precedence - Enum in net.sourceforge.czt.vcg.z
-
- VCEnvAnn - Class in net.sourceforge.czt.vcg.z
-
- VCEnvAnn(String, List<VC<Pred>>, VCNameFactory) - Constructor for class net.sourceforge.czt.vcg.z.VCEnvAnn
-
Create the given environment as place holder a VC ZSect list of VCs per paragraph.
- VCEnvAnn(String, List<VC<Pred>>, VCNameFactory, BaseFactory) - Constructor for class net.sourceforge.czt.vcg.z.VCEnvAnn
-
- VCEnvAnnVisitor<R> - Interface in net.sourceforge.czt.vcg.z
-
- VCG<T,B> - Interface in net.sourceforge.czt.vcg.z
-
A Verification Condition Generator interface implemented by various tools to generate VC conjectures
enforcing specific consistency properties of specifications.
- vcg(File) - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
Given a file containing one or more ZSects, prints a CZT string corresponding
to the section(s) in the file.
- VCG_DOMAINCHECK_SOURCENAME_SUFFIX - Static variable in interface net.sourceforge.czt.vcg.z.dc.DomainCheckPropertyKeys
-
- VCG_DOMAINCHECK_TOOLKIT_NAME - Static variable in interface net.sourceforge.czt.vcg.z.dc.DomainCheckPropertyKeys
-
- VCG_DOMAINCHECK_VCNAME_SUFFIX - Static variable in interface net.sourceforge.czt.vcg.z.dc.DomainCheckPropertyKeys
-
- VCG_FEASIBILITY_SIGSCHEMA_SUFFIX - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
- VCG_FEASIBILITY_SOURCENAME_SUFFIX - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
- VCG_FEASIBILITY_TOOLKIT_NAME - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
- VCG_FEASIBILITY_VCNAME_SUFFIX - Static variable in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityPropertyKeys
-
- VCG_REFINEMENT_SOURCENAME_SUFFIX - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- VCG_REFINEMENT_TOOLKIT_NAME - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- VCG_REFINEMENT_VCNAME_SUFFIX - Static variable in interface net.sourceforge.czt.vcg.z.refinement.RefinementPropertyKeys
-
- VCGCommand<R> - Class in net.sourceforge.czt.vcg.z
-
Abstract command for all VCG activities.
- VCGCommand() - Constructor for class net.sourceforge.czt.vcg.z.VCGCommand
-
- VCGContext<T,B> - Interface in net.sourceforge.czt.vcg.z
-
VCG contextual information to be used by various VC generation tools.
- VCGException - Exception in net.sourceforge.czt.vcg.z
-
- VCGException(Dialect, String) - Constructor for exception net.sourceforge.czt.vcg.z.VCGException
-
Creates a new instance of VCGException
- VCGException(Dialect, String, Throwable) - Constructor for exception net.sourceforge.czt.vcg.z.VCGException
-
- VCGException(Dialect, Throwable) - Constructor for exception net.sourceforge.czt.vcg.z.VCGException
-
- VCGException(Dialect, String, String, Throwable) - Constructor for exception net.sourceforge.czt.vcg.z.VCGException
-
- VCGPropertyKeys - Interface in net.sourceforge.czt.vcg.z
-
Contains String constants for the keys used in VCG properties.
- vcgToFile(File) - Method in class net.sourceforge.czt.vcg.z.VCGUtils
-
Calculates the VCG results (see
VCGUtils.vcg(java.io.File)) and
writes then to a file according to
#getVCFilename(java.lang.String, java.lang.String) .
- VCGUtils<T,B> - Class in net.sourceforge.czt.vcg.z
-
- VCGUtils() - Constructor for class net.sourceforge.czt.vcg.z.VCGUtils
-
- VCNameFactory - Interface in net.sourceforge.czt.vcg.util
-
- VCSource - Class in net.sourceforge.czt.vcg.z
-
- VCSource(Para) - Constructor for class net.sourceforge.czt.vcg.z.VCSource
-
- VCSource(VC<?>) - Constructor for class net.sourceforge.czt.vcg.z.VCSource
-
- VCType - Enum in net.sourceforge.czt.vcg.z
-
- VCTYPE_DC_DEFAULT - Static variable in interface net.sourceforge.czt.vcg.z.dc.DomainCheckPropertyKeys
-
- visit(Term) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- visit(Term) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Visits the given term (e.g., term.accept(this)).
- visit(Term) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
Calculates DC for given term (i.e.
- visit(Term) - Method in class net.sourceforge.czt.vcg.z.feasibility.AbstractFeasibilityVCCollector
-
Calculates DC for given term (i.e.
- visit(Term) - Method in interface net.sourceforge.czt.vcg.z.TermTransformer
-
Visit the given term.
- visit(Term) - Method in class net.sourceforge.czt.vcg.z.transformer.AbstractTermTransformer
-
- visit(Term) - Method in interface net.sourceforge.czt.vcg.z.VCCollector
-
Visits a given term.
- visitAndPred(AndPred) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements conjunction:
AndPred : P \land Q
This covers the Z/EVES domain check rules for:
DC(P \land Q) \iff DC(P) \land (P \implies DC(Q))
The RHS of this equivalence is the result this method returns.
- visitAnn(Ann) - Method in class net.sourceforge.czt.vcg.z.TrivialVCCollector
-
- visitApplExpr(ApplExpr) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
Application expression is one of the most important cases
as it handles function application (potentially) outside
their domains, which is the main point of domain checks.
- visitAxPara(AxPara) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
Schema or generic schema definition (vertical).
- visitAxPara(AxPara) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements various axiomatic description paragraphs:
AxPara (from axdef) : \begin{axdef} D \where P \end{axdef}
AxPara (from gendef) : \begin{gendef}[X] D \where P \end{gendef}
AxPara (from schema) : \begin{schema} D \where P \end{schema}
AxPara (from genschema): \begin{schema}[X] D \where P \end{schema}
AxPara (from abbrev.) : \begin{zed} N[X] == E \end{zed}
This covers the Z/EVES domain check rules for:
DC(\begin{zed} N[X] == E \end{zed}) \iff DC(E)
DC(\begin{xxx}[X] D \where P \end{xxx}) \iff DC(D) \land DC(D) \land (\forall D @ DC(P))
The RHS of this equivalence is the result this method returns.
- visitAxPara(AxPara) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
This implements various axiomatic description paragraphs:
AxPara (from axdef) : \begin{axdef} D \where P \end{axdef}
AxPara (from gendef) : \begin{gendef}[X] D \where P \end{gendef}
AxPara (from schema) : \begin{schema} D \where P \end{schema}
AxPara (from genschema): \begin{schema}[X] D \where P \end{schema}
AxPara (from abbrev.) : \begin{zed} N[X] == E \end{zed}
This covers the Z/EVES domain check rules for:
DC(\begin{zed} N[X] == E \end{zed}) \iff DC(E)
DC(\begin{xxx}[X] D \where P \end{xxx}) \iff DC(D) \land DC(D) \land (\forall D @ DC(P))
The RHS of this equivalence is the result this method returns.
- visitBindExpr(BindExpr) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
The production for schema binding expressions is as follows:
BindExpr : \lblot x == E1; ...
- visitBranch(Branch) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- visitBranch(Branch) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
DC the expression E on a Freetype branch "b \ldata E \rdata" as "DC(E)".
- visitBranch(Branch) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
- visitCondExpr(CondExpr) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
The production for conditional schema expressions is as follows:
CondExpr : \IF P \THEN E1 \ELSE E2
This covers the Z/EVES domain check rules for:
DC(\IF P \THEN E1 \ELSE E2) \iff DC(P) \land (\IF P \THEN DC(E1) \ELSE DC(E2))
The RHS of this equivalence is the result this method returns.
- visitConjPara(ConjPara) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements domain check for conjecture paragraphs:
ConjPara : [X] "theorem" N \vdash? Pred.
- visitConjPara(ConjPara) - Method in class net.sourceforge.czt.vcg.z.feasibility.TrivialFeasibilityVCCollector
-
- visitConstDecl(ConstDecl) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements DC for constant declarations
ConstDecl: n[X,...] == E
which in Z/EVES is considered as Standard Z
axiomatic definition paragraph with OmitBox
(i.e.
- visitDCVCEnvAnn(DCVCEnvAnn) - Method in interface net.sourceforge.czt.vcg.z.dc.DCVCEnvAnnVisitor
-
Visits a DCVCEnvAnn.
- visitDefinition(Definition) - Method in interface net.sourceforge.czt.vcg.util.DefinitionTable.DefinitionVisitor
-
- visitDirective(Directive) - Method in class net.sourceforge.czt.vcg.z.dc.TrivialDCVCCollector
-
- visitDirective(Directive) - Method in class net.sourceforge.czt.vcg.z.feasibility.TrivialFeasibilityVCCollector
-
- visitExpr0N(Expr0N) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements various expression list productions:
SetExpr : \{ x, y \}
TupleExpr : (x, y)
ProdExpr : X \cross Y
as well as the Expr2N abstract class.
- visitExpr1(Expr1) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements various unary schema expressions:
NegExpr : \lnot S
PreExpr : \pre S
RenameExpr : S[new/old]
DecorExpr : S~'
BindSelExpr: S.x
HideExpr : S \ (x,...)
as well as the general expressions:
PowerExpr : \power X
TupleSelExpr: (x, y).1
leaving only ThetaExpr leaf class to be trated
separately within the Expr1 subtree.
- visitExpr2(Expr2) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements various binary schema expressions:
CompExpr : S1 \comp S2
PipeExpr : S1 \pipe S2
ProjExpr : S1 \proj S2
AndExpr : S1 \land S2
OrExpr : S1 \land S2
ImpliesExpr: S1 \implies S2
IffExpr : S1 \iff S2
as well as the general SchExpr2 abstract class, hence
leaving only ApplExpr leaf class to be trated separately
within the Expr2 subtree.
- visitExprPred(ExprPred) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
ExprPred is never created by some user expression, but through parsing
in order to embed expressions within the predicate term subtree.
- visitFact(Fact) - Method in class net.sourceforge.czt.vcg.z.dc.TrivialDCVCCollector
-
This implements the Fact predicates:
TruePred : true
FalsePred: false
This covers the Z/EVES domain check rules for:
DC(true) \iff true
DC(false) \iff true
The RHS of this equivalence is the result this method returns.
- visitFact(Fact) - Method in class net.sourceforge.czt.vcg.z.feasibility.TrivialFeasibilityVCCollector
-
This implements the Fact predicates:
TruePred : true
FalsePred: false
This covers the Z/EVES domain check rules for:
DC(true) \iff true
DC(false) \iff true
The RHS of this equivalence is the result this method returns.
- visitFeasibilityVCEnvAnn(FeasibilityVCEnvAnn) - Method in interface net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCEnvAnnVisitor
-
Visits a DCVCEnvAnn.
- visitFreePara(FreePara) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- visitFreePara(FreePara) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements various free type paragraphs:
FreePara : N ::= c | b \ldata E \rdata | ...
- visitFreePara(FreePara) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
- visitFreetype(Freetype) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- visitFreetype(Freetype) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
DC the branch list of each individual Freetype
- visitFreetype(Freetype) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
DC the branch list of each individual Freetype
- visitGenParamType(GenParamType) - Method in class net.sourceforge.czt.vcg.util.CarrierSet
-
The carrier set of \power~T is the power expression
for the carrier set of T.
- visitGivenPara(GivenPara) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- visitGivenPara(GivenPara) - Method in class net.sourceforge.czt.vcg.z.dc.TrivialDCVCCollector
-
- visitGivenPara(GivenPara) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
[A, B] --> \lnot A = \{\} \land \lnot B = \{\}
- visitGivenType(GivenType) - Method in class net.sourceforge.czt.vcg.util.CarrierSet
-
- visitIffPred(IffPred) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements equivalence:
IffPred : P \iff Q
This covers the Z/EVES domain check rules for:
DC(P \iff Q) \iff DC(P) \land DC(Q)
The RHS of this equivalence is the result this method returns.
- visitImpliesPred(ImpliesPred) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements implication:
ImpliesPred : P \implies Q
This covers the Z/EVES domain check rules for:
DC(P \implies Q) \iff DC(P) \land (P \implies DC(Q))
The RHS of this equivalence is the result this method returns.
- visitInclDecl(InclDecl) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements DC for schema inclusion declarations
InclDecl: S[E1, ....] or S
This covers the Z/EVES domain check rules for:
DC(S[E1,...]) \iff DC(E) \land ....
- visitLambdaExpr(LambdaExpr) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
The production for lambda expressions is as follows:
LambdaExpr : \lambda D | P @ E
This covers the Z/EVES domain check rules for:
DC(\lambda D | P @ E) \iff DC(D) \land (\forall D @ DC(P) \land (P \implies DC(E)))
The RHS of this equivalence is the result this method returns.
- visitLatexMarkupPara(LatexMarkupPara) - Method in class net.sourceforge.czt.vcg.z.dc.TrivialDCVCCollector
-
- visitLatexMarkupPara(LatexMarkupPara) - Method in class net.sourceforge.czt.vcg.z.feasibility.TrivialFeasibilityVCCollector
-
For LaTeX inputs, a markup paragraph list of directives is collected.
- visitLetExpr(LetExpr) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
The production for let expressions is as follows:
LetExpr : \LET x == E1; ....
- visitMemPred(MemPred) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements relational operators (i.e.
- visitMuExpr(MuExpr) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
The production for mu expressions is as follows:
MuExpr : \mu D | P @ E
This covers the Z/EVES domain check rules for:
DC(\mu D | P @ E) \iff DC(D) \land (\forall D @ DC(P) \land (P \implies DC(E))) \land (\exists_1 D @ P)
The RHS of this equivalence is the result this method returns.
- visitNameSectTypeTriple(NameSectTypeTriple) - Method in class net.sourceforge.czt.vcg.z.dc.TrivialDCVCCollector
-
- visitNameSectTypeTriple(NameSectTypeTriple) - Method in class net.sourceforge.czt.vcg.z.feasibility.TrivialFeasibilityVCCollector
-
- visitNameTypePair(NameTypePair) - Method in class net.sourceforge.czt.vcg.z.dc.TrivialDCVCCollector
-
- visitNameTypePair(NameTypePair) - Method in class net.sourceforge.czt.vcg.z.feasibility.TrivialFeasibilityVCCollector
-
- visitNarrPara(NarrPara) - Method in class net.sourceforge.czt.vcg.z.TrivialVCCollector
-
- visitNegPred(NegPred) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements negation:
NegPred : \lnot P
This covers the Z/EVES domain check rules for:
DC(\lnot P) \iff DC(P)
The RHS of this equivalence is the result this method returns.
- visitNewOldPair(NewOldPair) - Method in class net.sourceforge.czt.vcg.z.dc.TrivialDCVCCollector
-
- visitNewOldPair(NewOldPair) - Method in class net.sourceforge.czt.vcg.z.feasibility.TrivialFeasibilityVCCollector
-
- visitNumExpr(NumExpr) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
DC for NumExpr is just true, despite Z/EVES not mentioning them.
- visitOper(Oper) - Method in class net.sourceforge.czt.vcg.z.dc.TrivialDCVCCollector
-
- visitOper(Oper) - Method in class net.sourceforge.czt.vcg.z.feasibility.TrivialFeasibilityVCCollector
-
- visitOptempPara(OptempPara) - Method in class net.sourceforge.czt.vcg.z.TrivialVCCollector
-
- visitOrPred(OrPred) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements disjunction:
OrPred : P \lor Q
This covers the Z/EVES domain check rules for:
DC(P \lor Q) \iff DC(P) \land (P \lor DC(Q))
The RHS of this equivalence is the result this method returns.
- visitPara(Para) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- visitPara(Para) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Retrieves for the given paragraph a corresponding VC
based over information on the current definition table.
- visitParent(Parent) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
For parent sections, calculate their dependent ZSect VCs by looking up the section manager,
unless this parent is set to be ignored (see
AbstractVCG.getParentsToIgnore()).
- visitPowerType(PowerType) - Method in class net.sourceforge.czt.vcg.util.CarrierSet
-
The carrier set of \power~T is the power expression
for the carrier set of T.
- visitProdType(ProdType) - Method in class net.sourceforge.czt.vcg.util.CarrierSet
-
- visitQnt1Expr(Qnt1Expr) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements various quantified schema expression productions:
ExistsExpr : \exists D | P @ SE, where SE could also be a schema
Exists1Expr: \exists_1 D | P @ SE, where SE could also be a schema
ForallExpr : \forall D | P @ SE, where SE could also be a schema
This covers the Z/EVES domain check rules for:
DC(qnt D | P @ SE) \iff DC(D) \land (\forall D @ DC(P)) \land DC(SE)
The RHS of this equivalence is the result this method returns.
- visitQntPred(QntPred) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements various quantified predicate productions:
ExistsPred : \exists D | P @ Q,
Exists1Pred: \exists_1 D | P @ Q
ForallPred : \forall D | P @ Q
This covers the Z/EVES domain check rules for:
DC(qnt D | P @ Q) \iff DC(D) \land (\forall D @ DC(P) \land (P \implies DC(Q)))
The RHS of this equivalence is the result this method returns.
- visitRefExpr(RefExpr) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
The production for reference expressions is as follows:
RefExpr : S[E1, ...] or S
This covers the Z/EVES domain check rules for:
DC(S[E1, ...]) \iff DC(E) \land ....
- visitRefinementVCEnvAnn(RefinementVCEnvAnn) - Method in interface net.sourceforge.czt.vcg.z.refinement.RefinementVCEnvAnnVisitor
-
Visits a DCVCEnvAnn.
- visitSchemaType(SchemaType) - Method in class net.sourceforge.czt.vcg.util.CarrierSet
-
- visitSchExpr(SchExpr) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
The production for schema expressions or schema constructions is as follows:
SchExpr: [ D | P ] or just S
This covers the Z/EVES domain check rules for:
DC(S \defs SE) \iff DC(SE), which is just a SchText as below
DC([ D | P ]) \iff DC(D) \land (\forall D @ DC(P))
The RHS of this equivalence is the result this method returns.
- visitSect(Sect) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
For UnparsedZSect or NarrSect, just return an empty list - no VCs.
- visitSetCompExpr(SetCompExpr) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements quantified expression productions, which
turns out to be just SetCompExpr (and abstract class QntExpr),
since the other element, MuExpr, is dealt with separately.
- visitSignature(Signature) - Method in class net.sourceforge.czt.vcg.util.CarrierSet
-
- visitStroke(Stroke) - Method in class net.sourceforge.czt.vcg.z.TrivialVCCollector
-
- visitTerm(Term) - Method in class net.sourceforge.czt.vcg.util.CarrierSet
-
- visitTerm(Term) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- visitTerm(Term) - Method in class net.sourceforge.czt.vcg.z.AbstractVCCollector
-
For terms in general, just assume nothing is known about them,
hence their VC is the worst possible (i.e.
- visitTerm(Term) - Method in class net.sourceforge.czt.vcg.z.TrivialVCCollector
-
For terms in general, just assume nothing is known about them,
hence their VC is the worst possible (i.e.
- visitThetaExpr(ThetaExpr) - Method in class net.sourceforge.czt.vcg.z.dc.TrivialDCVCCollector
-
This implements ThetaExpr for schemas:
ThetaExpr: \theta S
which in Z is given as
DC(\theta S) \iff true
The RHS of this equivalence is the result this method returns
- visitThetaExpr(ThetaExpr) - Method in class net.sourceforge.czt.vcg.z.feasibility.TrivialFeasibilityVCCollector
-
This implements ThetaExpr for schemas:
ThetaExpr: \theta S
which in Z is given as
DC(\theta S) \iff true
The RHS of this equivalence is the result this method returns
- visitType(Type) - Method in class net.sourceforge.czt.vcg.z.TrivialVCCollector
-
- visitUnparsedPara(UnparsedPara) - Method in class net.sourceforge.czt.vcg.z.TrivialVCCollector
-
- visitVarDecl(VarDecl) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements DC for variable declarations
VarDecl: x,...: E
This covers the Z/EVES domain check rules for:
DC(x, ....: E) \iff DC(E)
The RHS of this equivalence is the result this method returns
- visitVCGEnvAnn(VCEnvAnn) - Method in interface net.sourceforge.czt.vcg.z.VCEnvAnnVisitor
-
Visits a ZSectDCEnvAnn.
- visitZBranchList(ZBranchList) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- visitZBranchList(ZBranchList) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
DC a list of Branch from a Freetype
- visitZBranchList(ZBranchList) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
DC a list of Branch from a Freetype
- visitZDeclList(ZDeclList) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
This implements DC for a list of declarations
D1 ; D2 ...
- visitZExprList(ZExprList) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
EXPRESSION TERMS
- visitZFreetypeList(ZFreetypeList) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- visitZFreetypeList(ZFreetypeList) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
DC a list of Freetype from a FreePara
- visitZFreetypeList(ZFreetypeList) - Method in class net.sourceforge.czt.vcg.z.feasibility.FeasibilityVCCollector
-
- visitZName(ZName) - Method in class net.sourceforge.czt.vcg.z.dc.TrivialDCVCCollector
-
- visitZName(ZName) - Method in class net.sourceforge.czt.vcg.z.feasibility.TrivialFeasibilityVCCollector
-
- visitZNameList(ZNameList) - Method in class net.sourceforge.czt.vcg.z.dc.TrivialDCVCCollector
-
- visitZNameList(ZNameList) - Method in class net.sourceforge.czt.vcg.z.feasibility.TrivialFeasibilityVCCollector
-
- visitZNumeral(ZNumeral) - Method in class net.sourceforge.czt.vcg.z.dc.TrivialDCVCCollector
-
for numbers is just true, despite Z/EVES not mentioning them.
- visitZNumeral(ZNumeral) - Method in class net.sourceforge.czt.vcg.z.feasibility.TrivialFeasibilityVCCollector
-
for numbers is just true, despite Z/EVES not mentioning them.
- visitZParaList(ZParaList) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- visitZSchText(ZSchText) - Method in class net.sourceforge.czt.vcg.z.dc.DCVCCollector
-
Z schema text is part of many productions in the Z grammar.
- visitZSect(ZSect) - Method in class net.sourceforge.czt.vcg.util.DefinitionTableVisitor
-
- visitZSect(ZSect) - Method in class net.sourceforge.czt.vcg.z.AbstractVCG
-
Bootstraps the whole VC generation process by visiting the Z section parents and paragraphs systematically.
- visitZStrokeList(ZStrokeList) - Method in class net.sourceforge.czt.vcg.z.TrivialVCCollector
-