|
//#define SEPARATE 1
|
|
//#include "nlist.h"
|
|
|
|
/*@
|
|
requires ValidArray : \valid( array + (0 .. MAX_SIZE - 1) );
|
|
requires ListNotEmpty : n >= 1;
|
|
requires Linked : linked_n (root, array, index, n, bound);
|
|
|
|
requires GhostSeparation: \separated(list, array + (0 .. MAX_SIZE - 1)) ;
|
|
requires GhostSeparation: \separated(list, *(array + (left .. index + n - 1))) ;
|
|
requires GhostSeparation: \separated(*list, array + (0 .. MAX_SIZE - 1)) ;
|
|
|
|
requires Separation:
|
|
\forall integer y ;
|
|
left <= y < index + n ==>
|
|
\separated( * (array + y), array + (0 .. MAX_SIZE - 1));
|
|
|
|
requires Separation:
|
|
\forall integer y, z;
|
|
left <= y < index + n && left <= z < index + n && y != z ==>
|
|
\separated(* (array+y), *(array+z));
|
|
|
|
requires Unique:
|
|
\forall integer y, z;
|
|
left <= y < index + n && left <= z < index + n && y != z ==>
|
|
array[y] != array[z];
|
|
|
|
requires Index0Bounds : 0 <= left <= index;
|
|
requires LinkedLeft : linked_n (array[left], array, left, index - left, root);
|
|
|
|
ensures *list == \old(*list);
|
|
ensures LinkedLeft : linked_n (\at(array[left], Pre), array, left, index-left, root);
|
|
ensures SubArraySwipeLeft : array_swipe_left{Pre, Post} (array, index, index + n - 1);
|
|
ensures LinkedNoHead : linked_n(root->next, array, index, n - 1, bound);
|
|
ensures unchanged{Pre, Post}(array, left, index) ;
|
|
|
|
ensures NoMoreHere:
|
|
\forall integer x ; left <= x < index+n-1 ==> array[x] != root ;
|
|
ensures NoMoreHere:
|
|
\forall integer x ; left <= x < index+n-1 ==> \separated(root, array[x]) ;
|
|
|
|
ensures GhostSeparation: \separated(list, array + (0 .. MAX_SIZE - 1)) ;
|
|
ensures GhostSeparation: \separated(list, *(array + (left .. index + n - 2))) ;
|
|
ensures GhostSeparation: \separated(*list, array + (0 .. MAX_SIZE - 1)) ;
|
|
|
|
ensures Separation :
|
|
\forall integer y;
|
|
left <= y < index + n - 1 ==>
|
|
\separated( * (array + y), array + (0 .. MAX_SIZE - 1));
|
|
|
|
ensures Separation:
|
|
\forall integer y, z;
|
|
left <= y < index + n - 1 && left <= z < index + n - 1 && y != z ==>
|
|
\separated(* (array+y), *(array+z));
|
|
|
|
ensures Unique:
|
|
\forall integer y, z;
|
|
left <= y < index + n - 1 && left <= z < index + n - 1 && y != z ==>
|
|
array[y] != array[z];
|
|
|
|
assigns array[index .. index + n - 2];
|
|
*/
|
|
void
|
|
array_pop (struct list **array, int index, int n,
|
|
list_t list, struct list *root, struct list *bound, int left)
|
|
{
|
|
//@ ghost struct list* array_left = array[left] ;
|
|
struct list *l = root->next;
|
|
int i = index;
|
|
//@ assert root == array[index] ;
|
|
//@ assert \separated(root, array + (left .. index + n - 1));
|
|
//@ assert \separated(&(root->next), array + (left .. index + n - 1));
|
|
|
|
/*@
|
|
loop invariant *list == \at(*list, Pre);
|
|
loop invariant IInBounds : index <= i <= index + n - 1;
|
|
loop invariant UnchangedLeft : unchanged{Pre, Here} (array, left, index);
|
|
loop invariant UnchangedRight: unchanged{Pre, Here} (array, i, index + n);
|
|
|
|
loop invariant BeforeISwipeLeft: array_swipe_left{Pre, Here} (array, index, i);
|
|
|
|
loop invariant LeftLinked : linked_n(array_left, array, left, index - left, root);
|
|
loop invariant CenterLinked: linked_n(root->next, array, index, i - index, l);
|
|
loop invariant RightLinked : linked_n(l, array, i + 1, n - 1 - (i - index), bound);
|
|
|
|
loop assigns i, l, array[index .. index + n - 2];
|
|
loop variant index + n - i;
|
|
*/
|
|
while (i < index + n - 1){
|
|
//@ ghost Before:
|
|
|
|
//@ ghost linked_n_all_elements(array_left, root, array, left, index - left);
|
|
//@ ghost linked_n_all_elements(root->next, l, array, index, i - index);
|
|
//@ ghost linked_n_all_elements(l, bound, array, i + 1, n - 1 - (i - index));
|
|
|
|
/*@ assert
|
|
\forall integer y;
|
|
left <= y < index + n ==>
|
|
\separated( * (array + y), array + i);
|
|
*/
|
|
array[i] = array[i+1];
|
|
//@ assert root->next == \at(root->next, Before);
|
|
//@ assert linked_n{Before}(root->next, array, index, i - index, l);
|
|
|
|
//@ ghost stay_linked(Before, Here, array_left, root, array, left, index - left) ;
|
|
|
|
//@ assert \forall integer k ; index <= k < i ==> *array[k] == \at(*array[k], Before) ;
|
|
//@ ghost stay_linked(Before, Here, root->next, l, array, index, i - index) ;
|
|
//@ assert SingletonI1 : linked_n(l, array, i + 1, 1, l->next);
|
|
//@ assert SinletonI : linked_n(l, array, i, 1, l->next);
|
|
|
|
//@ ghost linked_n_merge_segment_right(root->next, l->next, array, index, i - index, l) ;
|
|
|
|
//@ assert \forall integer k ; i+1 <= k < index+n ==> *array[k] == \at(*array[k], Before) ;
|
|
//@ ghost stay_linked(Before, Here, l, bound, array, i + 1, n - 1 - (i - index)) ;
|
|
|
|
i++;
|
|
l = l->next;
|
|
}
|
|
}
|