logic - 用户指定值的 Hoare Logic Loop 变体

Question

我有以下问题：前提条件为真

int n = askUser();
int i = 0;
while(i<n){
  ...
  i++;
}

我正在考虑的变体是：n-i. 但是，我认为没有任何东西可以阻止用户提供负值，在这种情况下，变体将为负值（这与其定义相矛盾）。

是否可以将不变量指定为 |n| -i，还是必须将 n>=0 作为前提条件？

任何帮助或建议将不胜感激。