我正在阅读这本书：1990 年代的编程。
我在解决要求我们解决的练习 10.12 时遇到困难：
var f : array of int {0<=#f}
; var s : bool
; s : s == (Ai,j|0<=i & i<=j & j<#f : f.i<=f.j)
我引入了新的变量 n 使得
s == (Ai,j|0<=i & i<=j & j<n : f.i<=f.j) & n=#f
这导致我不变
I0 : s == (Ai,j|0<=i & i<=j & j<n : f.i<=f.j)
I1 : 0<=n & n<=#f
和守卫
B : n != #f
绑定函数是
t = #f - n
任务取得进展
n:=n+1
我知道解决方案很简单，但是在尝试保持 I0 的不变性时总是卡住。
请有人告诉我如何计算分配以保持 I0 的不变性？
谢谢。