Sign up ×

I'm came across this exercise while trying to learn Dafny: Write a method that will calculate the maximum value of an array and return its index. I'm definitely missing something here: (permalink)

method FindMax(a: array<int>) returns (i: int)
// Annotate this method with pre- and post-conditions
// that ensure it behaves as described.
requires a!= null && a.Length > 0;
ensures 0 <= i < a.Length ==> forall k :: 0 <= k < a.Length ==> a[k] <= a[i]; //*
   i := 0;
   var index: int:= 0;
   while(index < a.Length)
   invariant 0 <= index <= a.Length;
   invariant 0 <= i < a.Length;
   invariant forall k :: 0 <= k <= i ==> a[k] <= a[i]; //Error: might not be maintained
      if(a[index] >= a[i]) {i := index;}
      index := index + 1;
   return i; //Error: post-condition* might not hold


share|improve this question
I have tried to open link and got HTTP Error 503. –  amazpyel Mar 25 '14 at 10:35
I don't see anywhere that specifies the array elements being positive integers. I'm not familiar with Dafny, but it looks like you're requiring the array elements to be greater than 0. –  Kate Paulk Mar 25 '14 at 11:01
@amazpyel, that was a transient error because they were updating the compiler. Thanks for your help. I found the answer, mostly it was due to bad bounds (<= instead of <). If you want it, new permalink. –  qwersjc Mar 28 '14 at 2:31

Your Answer



Browse other questions tagged or ask your own question.