InvTranslate

Object
- InvTranslate

```
public class InvTranslate
extends Object
```
Provides a variable translation over an invariant at one program point (perhaps in a different program) to a similar invariant at a second program point. In general, on order for a translation to be possible, the invariants must be of the same class. For example, consider the invariants (x>y) at ppt1 and (p>q) at ppt2. Since the invariants are the same, the translation is (x → p) and (y → q).
The quality of the translation is also determined (approximately on a scale of 0 to 100). If the invariants are not of the same class, no translation is possible and the quality is zero. If the class and the formula are the same, the match is excellent (80). If the class is the same and the formula is different, the match is mediocre (40). The quality is increased for variables with exactly the same derivation and decreased for those with different derivations.
Other checks could be added to further specify the quality. For example, if one invariant is a precondition and the other is a postcondition, the quality should be reduced.

- Constructor Summary
  
  Constructors
  Constructor Description
  
  InvTranslate(Invariant i1, Invariant i2)
  Setup a translation from i1 to i2.
- Method Summary
  
  All Methods Instance Methods Concrete Methods
  Modifier and Type Method Description
  
  String toString()
  Returns a somewhat verbose description of the translation.
  - Methods inherited from class Object
    clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

- Constructor Detail
  - InvTranslate
```
public InvTranslate(Invariant i1,
                    Invariant i2)
```
    Setup a translation from i1 to i2. The quality and the variable map is set accordingly.
    
    Parameters:
    
    i1 - the invariant to translate from
    
    i2 - the invariant to translate to
- Method Detail
  - toString
```
@SideEffectFree
public String toString(@GuardSatisfied InvTranslate this)
```
    Returns a somewhat verbose description of the translation.
    
    Overrides:
    
    toString in class Object