Exercise 6.1.4.4: incorrect specification of permutation
qsantos opened this issue · 4 comments
qsantos commented
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 commented
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 commented
Alt-Ergo 2.3.3 and CVC4 1.6.
AllanBlanchard commented
Ok, I keep this issue open until I test this example with a more recent Ocaml + Alt-Ergo.
AllanBlanchard commented
With Alt-Ergo 2.4.0 that I will use in next version, it is OK.