logichoare-logic

Which hoare-triples is correct?

Lets say there is a method that takes two arguments balance and price, that only does the following:

if(price < balance) {
    balance = balance - price;
}

I feel like there are two possible ways to write this in a hoare-triple:

(| price=p0 ^ balance = b0 |) buy (| ((p0 < balance) => balance = b0 - p0) v ((p0 >= balance) => balance = b0) |)

or

(| price=p0 ^ balance = b0 |) buy (| ((p0 < balance) ^ (balance = b0-p0)) v ((p0 >= balance) ^ (balance = b0))

( => is implication) What I'm wondering is which one is correct? Or are both correct?

Solution

  • I intended for this to be a comment, but I don't have the reputation to comment.
    The two hoare-triples certainly aren't equivalent. If p0 >= balance, the right side of the first triple evaluates to true, while the right side of the second triple evaluates to false. I'm at work, and can't work out which is the correct hoare-triple right now, but I'm sure someone more qualified than me will answer before I've finished at work.

    If we let P := p0 < balance, Q := balance = b0 - p0, and R := balance = b0, we can represent the right sides of your equations with (P => Q) v (-P => R) and (P ^ Q) v (-P ^ R), and create the following truth table.

    +---+---+---+----------------------------+------------------------+
    | .P | Q | .R | (P => Q) v (-P => R) | (P ^ Q) v (-P ^ R) |
    +---+---+---+----------------------------+------------------------+
    | .T | .T | .T | . . . . . . . . T . . . . . . . . | . . . . . . .T . . . . . . . |
    | .T | .T | .F | . . . . . . . . T . . . . . . . . | . . . . . . .T . . . . . . . |
    | .T | .F | .T | . . . . . . . . T . . . . . . . . | . . . . . . .F . . . . . . . |
    | .T | .F | .F | . . . . . . . . T . . . . . . . . | . . . . . . .F . . . . . . . |
    | .F | .T | .T | . . . . . . . . T . . . . . . . . | . . . . . . .T . . . . . . . |
    | .F | .T | .F | . . . . . . . . T . . . . . . . . | . . . . . . .F . . . . . . . |
    | .F | .F | .T | . . . . . . . . T . . . . . . . . | . . . . . . .T . . . . . . . |
    | .F | .F | .F | . . . . . . . . T . . . . . . . . | . . . . . . .F . . . . . . . |
    +---+---+---+----------------------------+------------------------+

    This shows that the two equations are not equivalent.

    I would guess that the correct value for the right side would be (P => Q) ^ (-P => R), because both statements must hold. I'm new to hoare-logic, and someone more knowledgeable can probably correct me.