private static final class WhileInvariantRule.Instantiation extends Object
Modifier and Type | Field and Description |
---|---|
ExecutionContext |
innermostExecutionContext |
LoopInvariant |
inv |
While |
loop |
Term |
progPost |
Term |
selfTerm |
Term |
u |
Constructor and Description |
---|
Instantiation(Term u,
Term progPost,
While loop,
LoopInvariant inv,
Term selfTerm,
ExecutionContext innermostExecutionContext) |
public final Term u
public final Term progPost
public final While loop
public final LoopInvariant inv
public final Term selfTerm
public final ExecutionContext innermostExecutionContext
public Instantiation(Term u, Term progPost, While loop, LoopInvariant inv, Term selfTerm, ExecutionContext innermostExecutionContext)