allow me to respectfully disagree: in logic, a tautology is a formula that is true in every interpretation . Although any tautology is trivially an inductive invariant, it is useless because it carries no information and does not help you prove any property.
More to the point, comparing the outcomes of the executions of an algorithm to an independent definition is not tautological, and the example of Euclid's algorithm illustrates this quite well. The GCD operator is defined "declaratively" as the least common divisor of the two inputs to the algorithm, whereas the specification of the algorithm is operational, based on successive subtraction. These two concepts are very different: in particular, the algorithm doesn't involve division or modulus, and the definition of GCD doesn't involve subtraction.
The idea of verifying the algorithm against the mathematical (declarative) definition is that you trust the latter a priori and gain confidence in the former by checking that it returns the same result for any valid inputs. Perhaps the idea doesn't get fully across because (1) the algorithm is so small and familiar and (2) the relevant mathematical facts that are used in the proof of the algorithm are stated without proof, but I don't see why you consider the comparison tautological.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/98409D54-4FDD-4885-B383-4701033BB8C5%40gmail.com.