Take the 2-minute tour ×
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
}

Thanks!

share|improve this question
    
I have tried to open link and got HTTP Error 503. –  amazpyel Mar 25 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 at 11:01
1  
@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 at 2:31

Your Answer

 
discard

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

Browse other questions tagged or ask your own question.