= Solution
Allocate a distinct game and copy every destination entry from the corresponding source position:
``
def flip(k: Int): Flip = {
require(1 < k && k <= game.length)
val result = new Flip(game.length)
var i = 0
while (i < game.length) {
val source = if (i < k) k - 1 - i else i
result.game(i) = game(source)
i += 1
}
result.flips = k :: flips
result
}
``
The <loop invariant> says that the receiver is unchanged and destination positions before `i` equal the reversal of the first $k$ source entries followed by the untouched suffix. The <loop variant> is $game.length-i$. At exit the copying is complete. Reversal is a bijection on positions, so the destination remains a <permutation>. \b[The returned object's <array> is independent of the receiver's <array>], while the immutable tail of its history <list> can safely be shared. The source's only supplied constructor randomizes the new <array> before the copy; that work is redundant but does not affect correctness. An additional private constructor could avoid it without changing the required result.
Back to article page
