logic - ユーザー指定値の Hoare Logic Loop バリアント

Question

次の問題があります: 前提条件が True

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

私が考えているバリアントは次のとおりn-iです。ただし、ユーザーが負の値を指定するのを止めるものは何もないと思います。その場合、バリアントは負になります(定義と矛盾します)。

不変量を |n| として指定することは可能ですか? - i、または前提条件として n>=0 を含める必要がありますか?

どんな助けや提案も大歓迎です。