Proving correctness and termination of an (imperative) algorithm using Isabelle

Question

I'm an undergraduate student trying to prove correctness and termination of imperative version of Euclidean gcd and Euclidean extended gcd algorithm. I used IMP language to implement the first one and Hoare logic to prove correctness and termination:

lemma "⊢{λs. s ''a'' = n ∧ s ''b'' = m ∧ n > 0 ∧ m > 0 ∧ (gcd (s ''a'') (s ''b'') = gcd (n) (m))}
        WHILE (Or (Less (V ''b'') (V ''a'')) (Less (V ''a'') (V ''b'')))
        DO (IF (Less (V ''b'') (V ''a'')) THEN
               (''a'' ::= Sub (V ''a'') (V ''b''))
            ELSE
               (''b'' ::= Sub (V ''b'') (V ''a'')))
        {λs. s ''a'' = gcd (s ''A'') (s ''B'')}"
  apply (rule While'[where P = "λs. s ''a'' = n ∧ s ''b'' = m ∧ 0 < n ∧ 0 < m ∧ gcd (s ''a'') (s ''b'') = gcd n m"])
  apply auto
    apply (rule Assign')
    apply auto
    prefer 2
    apply (rule Assign')
  apply auto

remaining sub goals are:

proof (prove)
goal (3 subgoals):
 1. ⋀s. 0 < s ''a'' ⟹ m = s ''b'' ⟹ n = s ''a'' ⟹ s ''a'' < s ''b'' ⟹ False
 2. ⋀s. 0 < s ''b'' ⟹ m = s ''b'' ⟹ n = s ''a'' ⟹ s ''b'' < s ''a'' ⟹ False
 3. ⋀s. n = s ''a'' ⟹ m = s ''a'' ⟹ 0 < s ''a'' ⟹ s ''b'' = s ''a'' ⟹ s ''a'' = gcd (s ''A'') (s ''B'')

and I don't now how to finish the proof. The gcd function here is default gcd from GCD library. I also tried this definition from Arith2 library:

definition cd :: "[nat, nat, nat] ⇒ bool"
  where "cd x m n ⟷ x dvd m ∧ x dvd n"

definition gcd :: "[nat, nat] ⇒ nat"
  where "gcd m n = (SOME x. x>0 ∧ cd x m n & (∀y.(cd y m n) ⟶ y dvd x))"

Is what I wrote correct and how should I continue? Should I use these definitions instead or should I write recursive version of gcd function myself? Is this approach correct?

Answer 1

First of all, you have a type in one place, where you talk about s ''A'' and s ''B'' instead of s ''a'' and s ''b''. But that is of course not the problem you were asking about.

The problem here is that the precondition is too strong to work with the WHILE rule. It contains the conditions s ''a'' = n and s ''b'' = m, which clearly do not work as a loop invariant since the loop modifies the variables a and b, so after one loop iteration, one of the conditions s ''a'' = n and s ''b'' = m will no longer hold.

You need to figure out a proper invariant that is weaker than what you have now. What you have to do is to kick out the s ''a'' = n and s ''b'' = m. Then your proof goes through.

You can then recover the statement you actually want to show with the strengthen_pre rule.

So the start of your proof would look something like this:

lemma "⊢{λs. s ''a'' = n ∧ s ''b'' = m ∧ n ≥ 0 ∧ m ≥ 0 ∧ (gcd (s ''a'') (s ''b'') = gcd (n) (m))}
        WHILE (Or (Less (V ''b'') (V ''a'')) (Less (V ''a'') (V ''b'')))
        DO (IF (Less (V ''b'') (V ''a'')) THEN
               (''a'' ::= Sub (V ''a'') (V ''b''))
            ELSE
               (''b'' ::= Sub (V ''b'') (V ''a'')))
        {λs. s ''a'' = gcd (s ''a'') (s ''b'')}"
  apply (rule strengthen_pre) 
  defer
   apply (rule While'[where P = "λs. s ''a'' ≥ 0 ∧ s ''b'' ≥ 0 ∧ gcd (s ''a'') (s ''b'') = gcd n m"])

To avoid this awkward manual use of strengthen_pre, other versions of IMP allow annotating the invariants of WHILE loops directly in the algorithm itself, so that a VCG (verification condition generator) can automatically give you all the things you have to prove and you don't have to apply Hoare rules manually.

Addendum: Note however that there is also a problem with your postcondition:

{λs. s ''a'' = gcd (s ''a'') (s ''b'')}

This is not what you want to show! This just means that the value of a after the execution is the GCD of the values of a and b after the execution. This also happens to be true because a and b are always equal after the algorithm has finished – but what you really want to know is that the value of a after the execution is equal to the GCD of a and b before the execution, i.e. equal to gcd n m. You therefore have to change your postcondition to

{λs. s ''a'' = gcd n m}