|
/*@
|
|
requires \valid(list);
|
|
requires ValidArray : \valid( array + (0 .. MAX_SIZE - 1) );
|
|
requires EnoughSpace : index + n + 1 <= MAX_SIZE;
|
|
requires Linked : linked_n (root, array, index, n, bound);
|
|
|
|
requires GhostSeparation: \separated(list, array + (0 .. MAX_SIZE - 1)) ;
|
|
requires GhostSeparation: \separated(list, *(array + (index .. index + n - 1))) ;
|
|
requires GhostSeparation: \separated(*list, array + (0 .. MAX_SIZE - 1)) ;
|
|
|
|
requires Separation:
|
|
\forall integer y ;
|
|
index <= y < index + n ==>
|
|
\separated( * (array + y), array + (0 .. MAX_SIZE - 1));
|
|
|
|
requires Separation :
|
|
\forall integer y, z;
|
|
index <= y < index + n && index <= z < index + n && z != y ==>
|
|
\separated( *(array + y), *(array + z));
|
|
|
|
requires Unique:
|
|
\forall integer y, z;
|
|
index <= y < index + n && index <= z < index + n && y != z ==>
|
|
array[y] != array[z];
|
|
|
|
assigns array[index .. index + n];
|
|
|
|
ensures GhostSeparation: \separated(list, array + (0 .. MAX_SIZE - 1)) ;
|
|
ensures GhostSeparation: \separated(list, *(array + (index + 1 .. index + n))) ;
|
|
ensures GhostSeparation: \separated(*list, array + (0 .. MAX_SIZE - 1)) ;
|
|
|
|
ensures Separation:
|
|
\forall integer y ;
|
|
index + 1 <= y < index + n + 1 ==>
|
|
\separated( * (array + y), array + (0 .. MAX_SIZE - 1));
|
|
ensures Separation :
|
|
\forall integer y, z;
|
|
index + 1 <= y < index + n + 1 && index + 1 <= z < index + n + 1 && z != y ==>
|
|
\separated( *(array + y), *(array + z));
|
|
ensures Unique:
|
|
\forall integer y, z;
|
|
index <= y < index + n + 1 && index <= z < index + n + 1 && y != z ==>
|
|
array[y] != array[z];
|
|
|
|
ensures *list == \old(*list);
|
|
|
|
ensures SubArraySwipeRight : array_swipe_right{Pre, Post} (array, index + 1, index + n + 1);
|
|
ensures StillLinked: linked_n(root, array, index + 1, n, bound);
|
|
|
|
*/
|
|
void
|
|
array_push (struct list **array, int index, int n,
|
|
list_t list, struct list *root, struct list *bound)
|
|
{
|
|
if( n == 0 )
|
|
return;
|
|
//@ ghost linked_n_valid_range(root, bound, array, index, n);
|
|
//@ assert \valid(array[index .. index + n - 1]);
|
|
|
|
int i = index + n;
|
|
struct list *le = bound;
|
|
int sup = 0 ;
|
|
//@ assert LeftLinkedA : linked_n(root, array, index, i - index, le);
|
|
//@ assert LeftLinkedB : linked_n(root, array, index, i - index, bound);
|
|
/*@
|
|
loop invariant *list == \at(*list, Pre) ;
|
|
loop invariant IInBounds : index <= i <= index + n ;
|
|
loop invariant i == index + n <==> sup == 0;
|
|
loop invariant i < index + n <==> sup == 1;
|
|
loop invariant UnchangedLeft: unchanged{Pre, Here} (array, index, i);
|
|
loop invariant AfterISwipeRight: array_swipe_right{Pre, Here} (array, i + 1, index + n + 1);
|
|
loop invariant LeftLinked : linked_n(root, array, index, i - index, le);
|
|
loop invariant RightLinked: linked_n(le, array, i + 1, n - (i - index), bound);
|
|
loop invariant Separation:
|
|
\forall integer y ; index <= y < index + n + sup ==>
|
|
\separated( * (array + y), array + (0 .. MAX_SIZE - 1));
|
|
loop invariant GhostSeparation:
|
|
\separated(list, *(array + (i+1 .. index + n))) ;
|
|
loop assigns i, le, sup, array[index+1 .. index + n];
|
|
loop variant i - index;
|
|
*/
|
|
while (i > index){
|
|
sup = 1 ;
|
|
struct list *leNext;
|
|
|
|
//@ ghost linked_n_all_elements(root, le, array, index, i-index);
|
|
//@ ghost linked_n_all_elements(le, bound, array, i+1, n-(i-index));
|
|
//@ ghost Before:
|
|
array[i] = array[i-1];
|
|
//@ assert unchanged{Before, Here}(array, index, i);
|
|
//@ assert LeftLinked2: linked_n{Before}(root, array, index, i - index, le);
|
|
//@ ghost stay_linked(Before,Here,root,le,array,index, i-index);
|
|
//@ assert LeftLinked3: linked_n(root, array, index, i - index, le);
|
|
|
|
|
|
//@ assert RightLinked2: linked_n{Before}(le, array, i + 1, n - (i - index), bound);
|
|
//@ assert unchanged{Before, Here}(array, i + 1, n - index + 1);
|
|
/*@ ghost int NN = n - (i - index), II = i + 1; */
|
|
//@ ghost stay_linked(Before,Here,le,bound,array,II, NN);
|
|
//@ assert RightLinked3: linked_n(le, array, i + 1, n - (i - index), bound);
|
|
|
|
i--;
|
|
|
|
//@ assert LeftLinked4: linked_n(root, array, index, i - index + 1, le);
|
|
//@ assert RightLinked4: linked_n(le, array, i + 2, n - (i - index) - 1, bound);
|
|
|
|
if( i == index ){
|
|
leNext = root;
|
|
//@ assert LeftLinked5 : linked_n(root, array, index, i - index, leNext);
|
|
//@ assert SingleLinked1 : linked_n(leNext, array, i, 1, le);
|
|
//@ assert SingleLinked2 : linked_n(leNext, array, i+1, 1, le);
|
|
//@ assert AfterISwipeRight_PIf: array_swipe_right{Pre, Here} (array, i + 1, index + n + 1) ;
|
|
}
|
|
else{
|
|
leNext = array[i];
|
|
|
|
/*@ ghost int NNN = i - index, III = index; */
|
|
//@ ghost linked_n_split_segment_direct (root, le, array, III, NNN, leNext, 1);
|
|
/*@ assert from_lemma_linked_split_segment_right_direct:
|
|
NNN > 0 ==>
|
|
leNext == array[III + NNN] ==>
|
|
linked_n(root, array, III, NNN + 1, le) ==>
|
|
( linked_n(root, array, III, NNN, leNext) && linked_n(leNext, array, III + NNN, 1, le) );
|
|
*/
|
|
|
|
//@ assert LeftLinked5 : linked_n(root, array, index, i - index, leNext);
|
|
|
|
//@ assert SingleLinked1 : linked_n(leNext, array, i, 1, le);
|
|
//@ assert SingleLinked2 : linked_n(leNext, array, i+1, 1, le);
|
|
//@ assert AfterISwipeRight_PElse: array_swipe_right{Pre, Here} (array, i + 1, index + n + 1) ;
|
|
|
|
}
|
|
le = leNext;
|
|
//@ assert LeftLinked9 : linked_n(root, array, index, i - index, le);
|
|
//@ assert RightLinked9 : linked_n(le, array, i + 1, n - (i - index), bound);
|
|
}
|
|
//@ assert RightLinked10 : linked_n(root, array, index + 1, n, bound);
|
|
//@ ghost linked_n_all_elements(root, bound, array, index+1, n);
|
|
//@ ghost AlmostEnd:
|
|
array[index] = NULL ; // USELESS ?
|
|
|
|
//@ ghost stay_linked(AlmostEnd, Here, root, bound, array, index+1, n);
|
|
//@ assert RightLinked11 : linked_n(root, array, index + 1, n, bound);
|
|
}
|