Hi, I'm learning program verification using Hoare triples. I would like to work through each section of a program and hopefully someone can point out if I've made any errors or if I haven't done enough for the proof.

Part 1:

{a > 0 ∧ b ≥ 0}

m := a; n := b

{Invariant: gcd(m,n) = gcd(a,b) ∧ n ≥ 0 }

Proof:

Pre -> [m:=a; n:=b]Invariant

[m:=a;n:=b][Invariant]

[m:=a; n:=b]{gcd(m,n) = gcd(m,n) ∧ b ≥ 0 }

So to prove:

{a > 0 ∧ b ≥ 0} -> {gcd(m,n) = gcd(m,n) ∧ b ≥ 0 }

Which is true right? As gcd(m,n)=gcd(m,n) and b ≥ 0 from the precondition?

Have I done enough, is this correct? Does it make any sense at all ?

Thanks,

Bob