= Solution
Check entries against their own indices, stopping on the first mismatch:
``
def isIdentity: Boolean = {
var i = 0
while (i < game.length && game(i) == i) {
i += 1
}
i == game.length
}
``
The <loop invariant> is $0\leq i\leq game.length$ and $game(j)=j$ for every $j<i$. The <loop variant> is $game.length-i$. A false guard means either every position has passed or the next position is wrong, so \b[the returned Boolean is true exactly for the identity <permutation>]. Neither the game nor its history is changed. <Short-circuit evaluation> protects the final indexed comparison.
Back to article page
