Array Permutation

Nov 22, 2012 at 2:42 PM

Hello,

My question is related to sorting algorithms, and how to fully specify them using SpecSharp (see QuickSort).

For instance I would like to be able to specify that the content of the array before and after calling the sorting function is the same.

I guess one way to do it is to use the following post-condition, giving that 'a' is the array being sorted:

 

  ensures forall{int k in (0:i); count{int v in (0:i); a[v] == a[k]} == count{int u in (0:i); old(a[u]) == a[k]}};

 

The problem is that SpecSharp throws then the following error:

 

C:\Windows\system32\unknown file(1,1): error CS2663: internal error: 7 name resolution errors detected

 

Which apparently is not well documented in this forum.

Here is the full source code:

using System;
using Microsoft.Contracts;

public class Program
{
  static void Main(string![]! args) {
    Console.WriteLine("Spec# says hello!");
  }

  static void simpleSwap(int[]! a, int i, int j)
  requires 0 <= i && i < a.Length;
  requires 0 <= j && j < a.Length;
  modifies a[i], a[j];
  ensures a[i] == old(a[i]);
  ensures a[j] == old(a[j]);
  ensures forall{int k in (0:i); count{int v in (0:i); a[v] == a[k]} == count{int u in (0:i); old(a[u]) == a[k]}};
  {
    int swapDude;
	swapDude = a[i];
	a[i] = a[j];
	a[i] = swapDude;
  }

}

Thanks!

Developer
Nov 23, 2012 at 8:15 PM

Hi,

You get the error because Spec# does not permit quantified variables within old-expressions. So the "old(a[u])" is what it complains about. Maybe as a workaround,you could pass two copies of the array (which you can express in a precondition) and modify only one of them. You can view the second array as a ghost parameter, which you use for specifications, but which is not needed to execute the program:

static void simpleSwap(int[]! a, int[]! b, int i, int j)
requires a != b && a.Length == b.Length;
requires forall{int i in (0:a.Length); a[i] == b[i]};
modifies a; // but not b

Then you can replace "old(a[u])" by "b[u]".

Cheers,
Peter
Nov 26, 2012 at 8:55 AM

Thanks!

Your workaround permits to get rid of the error.

But I still have problems proving that the following holds after a simple swap:

  ensures forall{int k in (0:a.Length); count{int v in (0:a.Length); a[v] == b[k]} == count{int u in (0:i); b[u] == b[k]}};

So I try to prove it in the case where there is no swap by using the dummy function:

  [Pure]
  static bool Lemma(int[]! a, int[]! b)
  requires a.Length == b.Length;
  requires forall{int i in (0:a.Length); a[i] == b[i]};
//  ensures forall{int k in (0:a.Length); count{int v in (0:a.Length); a[v] == b[k]} == count{int u in (0:i); b[u] == b[k]}};
  {
    return true;
  }

But Spec# throws a quite "deep" error that starts with

"Error    1    Internal Compiler Error: System.NullReferenceException: Object reference not set to an instance of an object.
   at System.Compiler.Normalizer.VisitBinaryExpression(BinaryExpression binaryExpression) in c:\codeplex_current_build\specsharp\SpecSharp\System.Compiler.Framework\Compiler\Normalizer.cs:line 752"

You can find the complete listing of the error here.

 

Thanks for your help!

Developer
Nov 27, 2012 at 2:07 PM

I think your postcondition does not verify since the second count-comprehension should range over (0:a.Length) rather than (0:i). This is probably a copy-and-paste error. The fixed condition does verify on my system. Isn't it great to have a verifier? :-)

I am sorry about the bug you ran into. We will look into this and see whether we can fix it.

Cheers,
    Peter