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