gov.nasa.jpf.symbc.veritesting.ast.transformations

Class TransformationData

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.transformations.TransformationData

public class TransformationData
extends java.lang.Object

Data class defining interface for invariants.

Field Summary

Fields

Modifier and Type	Field and Description
java.util.Set<Invariant>	invariants
DynamicRegion	region
boolean	runInvariants

Constructor Summary

Constructors

Constructor and Description
TransformationData(DynamicRegion region, java.util.Set<Invariant> invariants, boolean runInvariants)

Method Summary

Modifier and Type	Method and Description
void	checkInvariants()

Methods inherited from class java.lang.Object

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

Field Detail

region

public final DynamicRegion region

invariants

public final java.util.Set<Invariant> invariants

runInvariants

public final boolean runInvariants

Constructor Detail

TransformationData

public TransformationData(DynamicRegion region,
                          java.util.Set<Invariant> invariants,
                          boolean runInvariants)

Method Detail

checkInvariants

public void checkInvariants()
                     throws StaticRegionException

Throws:

StaticRegionException