Allocate a distinct game and copy every destination entry from the corresponding source position:The loop invariant says that the receiver is unchanged and destination positions before
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
}i equal the reversal of the first source entries followed by the untouched suffix. The loop variant is . At exit the copying is complete. Reversal is a bijection on positions, so the destination remains a permutation. 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. Articles by others on the same topic
There are currently no matching articles.