// Returns maximal element of array

method max(a : array<int>) returns (key : int)
  requires a.Length > 0;
  ensures exists  k :: 0 <= k < a.Length && a[k] == key;
  ensures forall k :: 0 <= k < a.Length => a[k] <= key;
{
  var i : nat := 0;



}