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.