protected static final class AbstractLoopInvariantRule.Instantiation
extends java.lang.Object
LoopScopeInvariantRule
application; contains the update, the program with post condition, the
While
loop the LoopScopeInvariantRule
should be applied
to, the LoopSpecification
, the the self Term
.Modifier and Type | Field and Description |
---|---|
ExecutionContext |
innermostExecutionContext |
LoopSpecification |
inv |
While |
loop |
Term |
progPost |
Term |
selfTerm |
Term |
u |
Constructor and Description |
---|
Instantiation(Term u,
Term progPost,
While loop,
LoopSpecification inv,
Term selfTerm,
ExecutionContext innermostExecutionContext) |
public final Term u
public final Term progPost
public final While loop
public final LoopSpecification inv
public final Term selfTerm
public final ExecutionContext innermostExecutionContext
public Instantiation(Term u, Term progPost, While loop, LoopSpecification inv, Term selfTerm, ExecutionContext innermostExecutionContext)