After loop iteration problem in Spec#

Mar 2, 2012 at 5:51 AM
Edited Mar 2, 2012 at 5:51 AM

 

 

Hi-

I'm suffer from tiny problem on spec# programming 

the subject is implementation of selectionsort and I've got the warning about  ' afterloop iteration : Loop invariant might not hold : a[i]<=a[min] '

 

Is there anybody who know the solution about this warning message, I had no idea even I tried everything I know ?? :)
Please help me!!!!!!!!!!!!!!!!!!!!!!!! 

--------

 

using System;
using Microsoft.Contracts;

public class Program
{
  static void Main(string![]! args) {
  int []! a = new int[]{3,1,7,5,8,3,2,-1,34};
  foreach(int e in a)
	Console.Write("{0} ",e);
	
  selectionSort(a);

  Console.WriteLine("Selection sort gives: ");  
  
  foreach(int e in a)
	Console.Write("{0} ",e);
 
    Console.ReadLine();
  }
  
  static void selectionSort(int[]! a)
  modifies a[*];
  {
	int i=0,j=0, min=0, temp1=0, temp2=0;

	for(i=0;i<a.Length-1;i++)
	invariant 0<=i && i<=a.Length;
	invariant a[i]<=a[min];
	{
	
		int variant = a.Length -i;
		
		for(j=i,min=i;j<a.Length;j++)
		{
		assume min<a.Length && min>=i;
			if(a[min]>a[j])
				min=j;
		}

		assume min<a.Length && min>=i;
		temp1=a[i];
		temp2=a[min];

		if(i<a.Length)
			a[i]=temp2;

		if(min<a.Length)
			a[min]=temp1;

		assert variant >=0;
	//	assert a.Length-i <variant;
		
	}
	return ;
  }
  

}

 

-----------------------------------------

Coordinator
Mar 2, 2012 at 7:41 PM

There are a number of problems with your program.

For example, consider what happens if a.Length is 0.  In that case, what does the invariant "a[i] <= a[min]" even mean on entry to the loop (when "i" and "min" are 0)?  (It is unfortunate that the Spec# verifier does not check for definedness of specifications, like Dafny does, for example.)

Also, you can change the "assume" statements in and after the inner loop to be declared as a loop invariant of the inner loop.  Again, be careful that you only dereference the array with indices that other specifications say are in range.

Finally, for the inner loop (and any loop, for that matter), the only thing known after the loop is what the loop invariant says.  So if you want something to be known about "a[min]" after the inner loop, then the loop invariant had better say something about that.