https://twitter.com/#!/wtakuo/status/173781581570387968 の解法を探るために使ったAlloyコード

gistfile1.txt

open util/ordering [Array]

sig Num {}
sig Array {
  at: Num -> one Num
}

pred update(a, a': Array, i, v: Num) {
  a'.at = a.at ++ i -> v
}

fact Traces {
  all a: Array - last | one i: Num | some v: Num |
    update [a, a.next, i, v]
}

check {
  no a: Array | some k, v: Num | let a' = a.next |
  {
      update [a, a', a.at [k], v]
      a'.at [a'.at [k]] != v
  }
}