# Thread: Verifying a GCD program

1. ## Verifying a GCD program

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

2. {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 }
So, for now you are only verifying these two assignments: "m:=a; n:=b", right?

I am not sure I understand everything you wrote. I am not familiar with the notation "Pre -> [m:=a; n:=b]Invariant". The way I learned it, a triple has the form {P}program{Q} where "program" is written without square brackets. I am also not sure this makes sense:
{a > 0 ∧ b ≥ 0} -> {gcd(m,n) = gcd(m,n) ∧ b ≥ 0 }
because it is neither a formula (because of braces) nor a triple.

More importantly, to prove this fragment, I believe one needs to use the rules for compound statement (semicolon), assignment, and the rule of consequence. I am not sure where you use them.

3. Hi,
I actually haven't even gotten into the program yet. The first step in proving a program using this method is to prove that the precondition implies the [assignment part][invariant]

4. Originally Posted by loggyb
Hi,
I actually haven't even gotten into the program yet. The first step in proving a program using this method is to prove that the precondition implies the [assignment part][invariant]
But the invariant is the formula after the first two assignments, right? So you have the following triple from you first post:
{a > 0 ∧ b ≥ 0}m := a; n := b{gcd(m,n) = gcd(a,b) ∧ n ≥ 0 }
To derive it, you need the rules I mentioned.