net.sourceforge.czt.vcg.z.dc

Class DomainCheckerCommand

java.lang.Object

net.sourceforge.czt.session.AbstractCommand

net.sourceforge.czt.vcg.z.VCGCommand<Pred>

net.sourceforge.czt.vcg.z.dc.DomainCheckerCommand

All Implemented Interfaces:

Command

public class DomainCheckerCommand
extends VCGCommand<Pred>

Domain checking VCG command.

Author:

leo

Constructor Summary

Constructors

Constructor and Description
DomainCheckerCommand()

Method Summary

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.

Methods inherited from class net.sourceforge.czt.vcg.z.VCGCommand

doCompute, parse, typeCheck

Methods inherited from class net.sourceforge.czt.session.AbstractCommand

compute, processProperties, traceInfo, traceLog

Methods inherited from class java.lang.Object

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

Constructor Detail

DomainCheckerCommand

public DomainCheckerCommand()

Method Detail

getVCEnvAnnClass

protected Class<? extends VCEnvAnn> getVCEnvAnnClass()

Description copied from class: VCGCommand

After generating VCs, the result ZSect is type checked and its VCEnvAnn added to the manager with a key according to this class.

Specified by:

getVCEnvAnnClass in class VCGCommand<Pred>

Returns:

generateVCS

protected VCEnvAnn generateVCS(ZSect zSect,
                               SectionManager manager)
                        throws VCGException

Description copied from class: VCGCommand

After parsing and type checking, generate VCs for the given zSect accordingly. The results must update the given section manager.

Specified by:

generateVCS in class VCGCommand<Pred>

Parameters:

zSect -

manager -

Returns:

environment with generated VCs

Throws:

VCGException