loops - 具有递减迭代的循环不变量

Question

from (temp := num)
until (temp = index)
loop
{
   data[temp] := data[temp – 1]
   temp := temp – 1
}

所以，这是一个从 (temp) 到 when (temp=index) 的循环，我不确定循环不变量是什么，因为我以前从未使用过递减迭代。

我在想类似的东西： (∃i : temp...index) • (data[i] := data[i-1]) 但这是不正确的，因为基本情况不起作用。