Exercise 6.1.4.4: incorrect specification of permutation

[qsantos]

In the correction of 6.1.4.4, we are given the definition of permutation:

/*@
  inductive permutation{L1, L2}(int* arr, integer fst, integer last){
  case reflexive{L1}: 
    \forall int* a, integer b,e ; permutation{L1,L1}(a, b, e);
  case rotate_left{L1,L2}:
    \forall int* a, integer b, e, i ;
      b < i <= e ==> rotate{L1, L2}(a, b, i) ==> permutation{L1, L2}(a, b, e) ;
  case rotate_right{L1,L2}:
    \forall int* a, integer b, e, i ;
      b <= i < e ==> rotate{L1, L2}(a, i, e) ==> permutation{L1, L2}(a, b, e) ;
  case transitive{L1,L2,L3}:
    \forall int* a, integer b,e ; 
      permutation{L1,L2}(a, b, e) && permutation{L2,L3}(a, b, e) ==> 
        permutation{L1,L3}(a, b, e);
  }
*/

Note that rotate_left and rotate_right do not make any assumption on the rest of the array, outside the rotation. Thus, the following code is valid:

/*@
  requires \valid(arr + (0..1));
  assigns arr[0..1];
  ensures permutation{Pre, Post}(arr, 0, 2);
*/
void f(int arr[2]) {
    arr[0] = 0;
    //@assert rotate{Pre, Here}(arr, 1, 2);
}

I think the appropriate definition of permutation should be:

/*@
  inductive permutation{L1, L2}(int* arr, integer fst, integer last){
  case reflexive{L1}: 
    \forall int* a, integer b,e ; permutation{L1,L1}(a, b, e);
  case rotate_left{L1,L2}:
    \forall int* a, integer b, e, i ;
      b < i <= e ==> rotate{L1, L2}(a, b, i) ==> unchanged{L1, L2}(a, i, e) ==> permutation{L1, L2}(a, b, e) ;
  case rotate_right{L1,L2}:
    \forall int* a, integer b, e, i ;
      b <= i < e ==> unchanged{L1, L2}(a, b, i) ==> rotate{L1, L2}(a, i, e) ==> permutation{L1, L2}(a, b, e) ;
  case transitive{L1,L2,L3}:
    \forall int* a, integer b,e ; 
      permutation{L1,L2}(a, b, e) && permutation{L2,L3}(a, b, e) ==> 
        permutation{L1,L3}(a, b, e);
  }
*/

It does make life harder for the provers, and I had to insert the following asserts:

/*@
  requires beg+1 < end && \valid(arr + (beg .. end-1)) ;
  assigns arr[beg .. end-1] ;
  ensures permutation{Pre,Post}(arr, beg, end);
*/
void two_rotates(int* arr, size_t beg, size_t end){
  rotate(arr, beg, beg+(end-beg)/2) ;
  //@assert unchanged{Pre, Here}(arr, beg+(end-beg)/2, end);
  //@ assert permutation{Pre, Here}(arr, beg, end) ;
  //@ghost Mid: ;
  rotate(arr, beg+(end-beg)/2, end) ;
  //@assert unchanged{Mid, Here}(arr, beg, beg+(end-beg)/2);
}

[AllanBlanchard]

Exact! Thank you.

However, I do not need any assertions to prove the example with your definition or permutation. Which version version do you use for Alt-Ergo?

[qsantos]

Alt-Ergo 2.3.3 and CVC4 1.6.

[AllanBlanchard]

Ok, I keep this issue open until I test this example with a more recent Ocaml + Alt-Ergo.

[AllanBlanchard]

With Alt-Ergo 2.4.0 that I will use in next version, it is OK.