public class DomainCheckerCommand extends VCGCommand<Pred>
| Constructor and Description |
|---|
DomainCheckerCommand() |
| Modifier and Type | Method and Description |
|---|---|
protected VCEnvAnn |
generateVCS(ZSect zSect,
SectionManager manager)
After parsing and type checking, generate VCs for the given zSect accordingly.
|
protected Class<? extends VCEnvAnn> |
getVCEnvAnnClass()
After generating VCs, the result ZSect is type checked and its VCEnvAnn
added to the manager with a key according to this class.
|
doCompute, parse, typeCheckcompute, processProperties, traceInfo, traceLogprotected Class<? extends VCEnvAnn> getVCEnvAnnClass()
VCGCommandgetVCEnvAnnClass in class VCGCommand<Pred>protected VCEnvAnn generateVCS(ZSect zSect, SectionManager manager) throws VCGException
VCGCommandgenerateVCS in class VCGCommand<Pred>zSect - manager - VCGExceptionCopyright © 2003–2016 Community Z Tools Project. All rights reserved.