Skip to content
Snippets Groups Projects
Select Git revision
  • 89e43a3a05c428506420530ecd349e42401b576e
  • main default protected
  • solution
3 results

DReverse.dfy

Blame
  • 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;
    }