Sign up ×
Software Quality Assurance & Testing Stack Exchange is a question and answer site for software quality control experts, automation engineers, and software testers. It's 100% free, no registration required.

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


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.