Какие верности-тройки правильные?

Question

Допустим, есть метод, который принимает два аргумента баланса и цены, что только делает следующее:

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

Я чувствую, что есть два возможных пути, чтобы написать это в Хора-тройка:

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

или

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

(=> имеет смысл) Что мне интересно, какой из них правильный? Или оба правильны?

Answer 1

Я намеревался, чтобы это был комментарий, но у меня нет репутации, чтобы высказаться.
Эти два трюка, конечно же, не эквивалентны. Если p0> = balance, правая часть первой тройки оценивается как true, а правая часть второй тройки - false. Я нахожусь на работе и не могу разобраться, какая из них правильная тройка сейчас, но я уверен, что кто-то более квалифицированный, чем я, ответит, прежде чем я закончу работу.

Если мы допустим баланс P: = p0 <, Q: = balance = b0 - p0, а R: = balance = b0, мы можем представить правые части ваших уравнений с (P => Q) v (-P => R) и (P^Q) v (-P^R) и создадим следующую таблицу истинности.

+ --- + --- + --- + ---------------------------- + ------ -------------------- +
| .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. , , , , , , |
+ --- + --- + --- + ---------------------------- + ------ ------------------ +

Это показывает, что эти два уравнения не эквивалентны.

Я бы предположил, что правильное значение для правой стороны будет (P => Q)^(-P => R), поскольку оба утверждения должны выполняться. Я новичок в hoare-logic, и кто-то более осведомленный, вероятно, может поправить меня.