public class InvTranslate extends Object
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 and Description|
Setup a translation from i1 to i2.