[tlaplus] Tautological Inductive Invariant in "Euclid Writes an Algorithm: A Fairytale"

[Alex Weisberger <alex.m.weisberger@xxxxxxxxx>]

Hi everyone,

I recently came across the great resource by Mr. Lamport - Euclid Writes an Algorithm: A Fairytale: https://lamport.azurewebsites.net/pubs/euclid.pdf

One thing that jumped out to me as I was reading is something that I keep bumping into when writing specs: the inductive invariant of a spec is often tautological.

For example, the paper specifies an algorithm (Euclid's algorithm) for the greatest common divisor of two numbers. The inductive invariant used is:

∧ x ∈ Number 

∧ y ∈ Number 

∧ GCD(x , y) = GCD(M , N )

where GCD(x, y) is defined independently of the algorithm presented in the paper. 

My question is, isn't this tautological, since we are comparing two different algorithms for computing the same thing? It's like saying "the algorithm is correct if it matches the output of the algorithm." I've run into this when writing specs practically, because I often can't think of an inductive variant other than "the algorithm does what it's supposed to." 

Do other people run into this? I wonder if I'm looking at this in the wrong way.

-Alex

-- 
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/109f9d64-5feb-458c-a59f-d39383d261cbn%40googlegroups.com.