Once we have the annotation _Term(t; k) which is considered as a declaration with k:int. What is the value of k? k := t?

Would you please explain how can I get the verification condition of an inner loop and then of the outer loop? I’ve read the project presentation many times but I couldn’t understand it.

It has no value. It is purely used in the formulas, as described in the project description (in particular on page 12). If you try to use it to compute anything, that should be rejected by the type checker.

By applying the formulas from the project description (in particular the one on page 12) or from the script (they are the same).

If a k is present, then this variable is used as k, otherwise, you make one up.