私は本を読み進めています: 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 の不変性を維持するための割り当ての計算方法を教えてください。
ありがとう。