Results 1 to 3 of 3

Math Help - Math Logic Finding the Weakest Precondition Calculus?

  1. #1
    Newbie
    Joined
    Feb 2010
    Posts
    17

    Math Logic Finding the Weakest Precondition Calculus?




    All 4 parts to this question concern the assertion P = {x=2^K & N>K}
    and one of 4 different assignment statements. You are to supply the
    missing assertions Q1, Q2, Q3, and Q4. Note that Q1 and Q2 should
    be the weakest preconditions for P with respect to the given statement;
    Q3 and Q4 should be postconditions with respect to the given statement
    whose weakest precondition would be P.

    Hint: The assignment axiom does not apply directly in the forward
    direction as in (c) and in (d). However, you can guess at Q3 and Q4
    by "looking" for x/4 and for K+1 in P and then substituting in reverse.
    You should then check your answer; i.e., check whether your
    post conditions do indeed have P as their weakest precondition using
    the assignment axiom directly.

    a)
    { } = Q1
    y <-- y/N
    {x=2^K & N>K}

    (b)
    { } = Q2
    x <-- x+x
    {x=2^K & N>K}

    (c)
    {x=2^K & N>K}
    x <-- x/4
    { } = Q3

    }

    (d)
    {x=2^K & N>K}
    y <-- K+1
    { } = Q4


    a)Attempt
    For this I see that
    (y<-- y/N) means Any y is replaced by y/N
    y/N is equivalent to N <--- y
    so y <---- N <---- y
    So the precondition is
    Q1= {x=2^K & y>K}
    well I not too sure about this.
    I think it could be Q1= {x=2^K & N>K}

    b)Attempt:
    x <-- x+x means replace x with x+x
    So Q2={ x+x =2^k & N>K}
    I don't think this is the weakest precondition.
    can this be simplified?

    c)Attempt:
    Q3={x/4=2^K & N>K}
    Im not too sure...


    d)Attempt:
    Post Condition
    Q4={x=2^(K+1-y+k)-y & N>K+1-y+K}
    When I replace K+1 with Y
    I get x=2^y-y+k & N>y-y+K
    this is exactly the same as the precondition

    Can someone check my answers and help me explain what the ones I get wrong?
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor

    Joined
    Aug 2006
    Posts
    18,966
    Thanks
    1785
    Awards
    1
    The questions you posted appear very course/textbook/instructor specific.
    That is to say, unless some person is in that same class I doubt the person would any idea what is being asked.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,561
    Thanks
    785
    This concerns Hoare Logic, a pretty standard way of reasoning about imperative programs.

    a)
    { } = Q1
    y <-- y/N
    {x=2^K & N>K}...

    a)Attempt
    For this I see that
    (y<-- y/N) means Any y is replaced by y/N
    y/N is equivalent to N <--- y
    so y <---- N <---- y
    So the precondition is
    Q1= {x=2^K & y>K}
    well I not too sure about this.
    I think it could be Q1= {x=2^K & N>K}
    The general inference rule (axiom) is {P[t/x]} x <-- t {P} where P[t/x] denotes replacing x by t in P. Since y does not occur in the postcondition, Q1 is the same as the postcondition, i.e., x=2^K & N>K. Indeed, if this holds before the assignment, then whatever you assign to y, the same formula will still be true.

    (b)
    { } = Q2
    x <-- x+x
    {x=2^K & N>K}...

    b)Attempt:
    x <-- x+x means replace x with x+x
    So Q2={ x+x =2^k & N>K}
    I don't think this is the weakest precondition.
    can this be simplified?
    You are correct, Q2 is (x=2^K & N>K)[x + x/x] (recall that [...] denotes a substitution), which is x+x =2^k & N>K. You can simplify it as 2x =2^k & N>K or x =2^{k-1} & N>K; this is not essential.

    (c)
    {x=2^K & N>K}
    x <-- x/4
    { } = Q3
    Finding the postcondition is trickier than applying a substitution; one has to "un-apply" a substitution, so that Q3[(x/4) / x] is x=2^K & N>K. Well, 4x=2^K & N>K as Q3 seems to work.

    d)Attempt:
    Post Condition
    Q4={x=2^(K+1-y+k)-y & N>K+1-y+K}
    When I replace K+1 with Y
    I get x=2^y-y+k & N>y-y+K
    this is exactly the same as the precondition
    To check, you need to replace y with K + 1 in the postcondition, not the other way around. Here, since y does not occur in the precondition, Q4 is the same as that precondition.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Weakest Metrizable Topology?
    Posted in the Differential Geometry Forum
    Replies: 2
    Last Post: October 17th 2011, 06:56 AM
  2. question in math logic
    Posted in the Discrete Math Forum
    Replies: 10
    Last Post: March 5th 2011, 04:35 PM
  3. Mainly logic with a little math
    Posted in the Algebra Forum
    Replies: 3
    Last Post: March 25th 2009, 07:48 AM
  4. discrete math help logic
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: February 23rd 2009, 06:27 AM
  5. math logic
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: April 3rd 2007, 06:28 AM

Search Tags


/mathhelpforum @mathhelpforum