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