daikon.tools
Class 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

InvTranslate()
an empty translation

Method Summary

String	toString() Returns a somewhat verbose description of the translation.
void	translate(Invariant i1, Invariant i2) Setup a translation from i1 to i2.

Methods inherited from class Object

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

Constructor Detail

InvTranslate

public InvTranslate()

an empty translation

Method Detail

translate

public void translate(Invariant i1,
                      Invariant i2)

Setup a translation from i1 to i2. The quality and the variable map is set accordingly.

toString

public String toString()

Returns a somewhat verbose description of the translation.

Overrides:

toString in class Object