I have been studying deductive verification of software lately, with weakest precondition, strongest postcondition, annotation calculus, and etc.

I came across the following rules for the while sentence:

enter image description here

But, my problem is when should I use which rule? I mean the second and third one that includes $t$, which is the variant here, is usually related to the loop condition, but when again when should I use the second while and when the third one? I couldn't find any clarification anywhere about when to choose which one. (Note that $t$ is not a variable of the program, but a variant used to prove termination.)


As you have already said, the second and third rule include a variant t to prove termination whereas the first rule does not consider it.

The second rule guarantees that the variant is always non-negative. This is necessary to have a lower bound for the variant which decreases every iteration.

The third rule relaxes that condition a little bit. The variant is always non-negative except in the last iteration (where e is false at the end of the block). This still guarantees termination (who cares about the variant if we know it's the last iteration?).

I think whether you choose the second or third rule is a matter of taste. Until now I knew only the second one. It should be easy to alter code or a variant whose correctness can be shown by the third rule such that it is also provable with the second one.

Choosing the first rule is of course only an option if you're not interested in termination.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.