Boogie postcondition violation undetected

Apr 25, 2011 at 1:32 AM

Hi,

I have been trying Spec# with the following code. The code passes the verification even if I introduce a mutation error in the isEmpty() method (See code). Any reason why Boogie can't detect this error?

 

// Queue.ssc
// Rosemary Monahan
// 8th March 2007
// Array implementation of Queue - non circular
   
using System;
using Microsoft.Contracts;

namespace Q_ROR2{
class IntQueue {
  [Rep][SpecPublic] int[]! elements = new int[10];
  [SpecPublic] int head;
  [SpecPublic] int tail;
  invariant 0 <= head && head <= elements.Length;
   invariant 0 <= tail && tail <= elements.Length;
   invariant head <= tail;
  
 

  [NotDelayed] public IntQueue()
    ensures head ==0;
    ensures tail == 0;
    ensures elements.Length == 10;  //elements.length is Inaccessible
  {
    head = 0;
    tail = 0;
  } //both head and tail point to the same place =>empty

  public void EnQueue(int e)
    requires !IsFull();
    requires  0 <  elements.Length;
    modifies this.*;
    ensures tail == old(tail)+1;
    ensures head == old(head);
    ensures elements.Length == old(elements.Length);
  {
    expose (this) {
      elements[tail] = e; tail++;
    }
  }
 
 
  //Leaving out  requires  (Tail != 0) is picked up by the verifier
  public int DeQueue()
    requires !IsEmpty();
    modifies this.*;
    ensures tail == old(tail);
    ensures head == old(head)+1;
    ensures elements.Length == old(elements.Length);
  {
    expose (this) {
      return elements[head++];
    }
  }

[Pure] public bool IsEmpty()
 ensures result == (head == tail);
  {
      return (head >= tail); //mutated from return (head == tail);
  }

[Pure] public bool IsFull()
    ensures result == (tail == elements.Length);
  {
      return (tail == elements.Length); 
  }
}

}

Coordinator
Apr 25, 2011 at 8:51 PM

Hi,

Under your invariant:

    invariant head <= tail;

the conditions "head == tail" and "head >= tail" are the same.

  Rustan

Apr 26, 2011 at 12:38 AM

Thanks.

 

What about the following code, also with an error introduced that goes undetected:

// Bubble sort
// Rustan Leino, 29 April 2009
namespace BubbleSort2_AOR6{
public class Bubble {
  static void Sort_Forall(int[]! a)
    modifies a[*];
    ensures forall{int i in (0: a.Length), int j in (0: a.Length), i <= j; a[i] <= a[j]};
  {
    for (int n = a.Length; 0 <= --n; )
      invariant 0 <= n && n <= a.Length;
      invariant forall{int i in (n: a.Length), int k in (0: i); a[k] <= a[i]};
    {
      for (int j = 0; j < n; j++)
        invariant j <= n;
        invariant forall{int i in (n+1: a.Length), int k in (0: i); a[k] <= a[i]};
        invariant forall{int k in (0: j); a[k] <= a[j]};
      {
        if (a[j+1] < a[j]) {
          int tmp = a[j];  a[j] = a[j*1];  a[j+1] = tmp;              //mutated from  int tmp = a[j];  a[j] = a[j+1];  a[j+1] = tmp;
        }
      }
    }
  }
}
}

Coordinator
Apr 26, 2011 at 7:15 AM

What's the problem?  This program seems consistent with its specification.

Apr 27, 2011 at 12:44 AM

The swap is erroneous

      int tmp = a[j];  a[j] = a[j*1];  a[j+1] = tmp;

The swap in correct code is:

    int tmp = a[j];  a[j] = a[j+1];  a[j+1] = tmp;

So, I expect at least that the invariant forall{int k in (0: j); a[k] <= a[j]}; is not satisfied.

 

Apr 27, 2011 at 7:59 AM

The erroneous swap copies element a[j] to a[j+1], thereby establishing a[j] <= a[j+1]. Remaining elements are not touched. This seems to be sufficient for the invariant to hold...

Best, Mark

Apr 28, 2011 at 1:38 AM

Yes, makes sense. However, the code with the error distorts the array to be sorted.

To solve that, and have the specification detect such error, I added the following postcondition to the sort method:

 ensures forall{int i in (0: old(a).Length); exists{int j in (0: a.Length); old(a)[i] == a[j]} };

Which basically states that all elements in the old array have to exist in the new array. This postcondition cannot be verified by Boogie however. 

Is there something wrong with the postcondition or is it the fact that it uses existential quantifier?

Your thoughts are really appreciated!

Thanks,

Iman