3

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

ありがとう。

4

0 に答える 0