de.uka.ilkd.key.rule

Class AbstractLoopInvariantRule.Instantiation

java.lang.Object

de.uka.ilkd.key.rule.AbstractLoopInvariantRule.Instantiation

Enclosing class:

AbstractLoopInvariantRule

protected static final class AbstractLoopInvariantRule.Instantiation
extends java.lang.Object

A container for an instantiation of this 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.

Field Summary

Fields

Modifier and Type	Field and Description
ExecutionContext	innermostExecutionContext
LoopSpecification	inv
While	loop
Term	progPost
Term	selfTerm
Term	u

Constructor Summary

Constructors

Constructor and Description
Instantiation(Term u, Term progPost, While loop, LoopSpecification inv, Term selfTerm, ExecutionContext innermostExecutionContext)

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

u

public final Term u

progPost

public final Term progPost

loop

public final While loop

inv

public final LoopSpecification inv

selfTerm

public final Term selfTerm

innermostExecutionContext

public final ExecutionContext innermostExecutionContext

Constructor Detail

Instantiation

public Instantiation(Term u,
                     Term progPost,
                     While loop,
                     LoopSpecification inv,
                     Term selfTerm,
                     ExecutionContext innermostExecutionContext)