/*@
	predicate Rev{K,L}(int* a,int* b)    = \true; 

	predicate Rev{K,L}(int* a,integer p) = \false; 
*/

void reverse(int* a) {
	int i = 0;
	//@ assert i <= 9;

	/*@
		loop invariant Rev{Pre,Here}(a, 0);
		loop assigns i;
	*/
	for (i=0; i<9; ++i)
		;
}