Results 1 to 4 of 4

Math Help - Verifying a GCD program

  1. #1
    Newbie
    Joined
    Jan 2010
    Posts
    2

    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
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,517
    Thanks
    771
    {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.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Jan 2010
    Posts
    2
    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]
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,517
    Thanks
    771
    Quote Originally Posted by loggyb View Post
    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.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Fixing The Program (Program Correctness)
    Posted in the Discrete Math Forum
    Replies: 2
    Last Post: March 21st 2009, 02:17 PM
  2. TI program
    Posted in the Calculators Forum
    Replies: 0
    Last Post: December 22nd 2008, 03:20 AM
  3. TI Program
    Posted in the Calculators Forum
    Replies: 6
    Last Post: May 10th 2008, 04:40 AM
  4. Need help with program
    Posted in the Math Software Forum
    Replies: 2
    Last Post: February 26th 2008, 12:39 PM
  5. program on TI-84
    Posted in the Calculators Forum
    Replies: 7
    Last Post: August 29th 2006, 06:05 AM

Search Tags


/mathhelpforum @mathhelpforum