Select Git revision
DReverse.dfy
Brady James Garvin authored
DReverse.dfy 488 B
method Reverse<T>(list: seq<T>) returns (reversed: seq<T>)
ensures |reversed| == |list|
ensures
forall i | 0 <= i < |reversed| ::
reversed[i] == list[|list| - i - 1]
{
var result := [];
var index := |list|;
while index > 0
invariant |result| == |list| - index
invariant index >= 0
invariant
forall i | 0 <= i < |result| ::
result[i] == list[|list| - i - 1]
{
index := index - 1;
result := result + [list[index]];
}
return result;
}