Skip to content
Snippets Groups Projects
Select Git revision
  • 5ee7dcb916a36fa770871f74419cbd6e8e3f0685
  • master default protected
2 results

grade_team_contribution.py

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