[WIP]実装の自由度を確保して配列シャッフルの事後条件を書けるか？

「配列のランダムシャッフルと形式的証明」で、１以上の要素を格納する配列（と乱数列）を渡すと、その配列要素から生成しうる順列のうちいずれかを返す関数（と、その実装）を示した。

しかし著者は、先の記事に掲げた事後条件は 制約が強すぎる と考えている。

本記事では著者が感じている問題を述べる。そして、いつかこの問題を解決したい。

配列シャッフルの形式的仕様

まず先行記事に掲げた配列シャッフルの事前条件と事後条件およびプログラムを再掲する。

{P: b=B ∧ |r|=|b|-1 ∧ |b|>0}
n:= |b|
do n≠1 →
  p:= r[n-2] mod n
  b[p], b[n-1]:= b[n-1], b[p]
  n:= n-1
od
{Q: b=foldr (λ(r,n) b → swap(b, n-1, r mod n)) B (zip r [2..])}

ここで swap(b, i, j) = (b; i:b[j]; j:b[i]) であり foldr は Haskell の関数定義を借用しているものとする。

このプログラムは配列要素を並べ替える範囲を 後ろから 順に狭めていく。

別のシャッフル定義

前掲のプログラムとは逆に、配列要素を並べ替える範囲を 前から 狭めていくことができる。

{P: b=B ∧ |r|=|b|-1 ∧ |b|>0}
i:= 0
do i≠|b|-1 →
  o:= r[i] mod (|b|-i)
  b[i], b[i+o]:= b[i+o], b[i]
  i:= i+1
od
{Q: b=foldl (λb (r,i) → swap(b, i, i + r mod (|b|-i))) B (zip r [0..])}

前から後ろから、交互に範囲を狭めていくような別の定義も考えられる。

実装の自由度を含めた事後条件

TBD

友人からは決定的には記述しにくいので確率を含めて定義してみてはどうか、といった提案をもらっている。

{Q: b=perm(B)} としつつ以下のような制約を別途掲げてはどうか、というアイデアももらっている。（これで証明がどうなるのかは、まだ考察できていない）

bool v[|b|]
v[i]:= false for all i
while (v[i] = false for some i)
    v[random()] := true

前の章に掲げた Q は実装の詳細を規定してしまっている。つまりプログラマーの設計の楽しさを奪っている、ような気がしている。

全ての順列のうち、いずれかを返すという制約を明示しつつ、しかし実装の詳細までは縛らない、そのような事後条件の書き方を探していきたい。

参考書籍

• The Science of Programming（プログラミングの科学）