# Anotation rules for while rule in deductive verification

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:

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 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?).