typedef struct stack {
	int capacity;
	int size;
	int *elems;
} Stack;

/*@
	requires \valid(st);
	requires \separated(st, (st->elems)+(0..st->capacity-1));
	requires \valid(st->elems+(0..st->capacity-1));		// eg: stack of size 50 is defined form 0 to 49
	requires 0 <= st->size < st->capacity;				// cant push if stack is full
	assigns st->elems[st->size], st->size;
	ensures \at(st->size, Here) == \at(st->size, Old) + 1;
	ensures st->elems[\old(st->size)] == x;
	ensures st->elems[\at(st->size, Here) - 1] == x;
	//ensures substack{Old,Here}(st);
  @*/
void push (Stack *st, int x){

	//@ assert 0 <= st->size < st->capacity;
	//@ assert 0 <= st->capacity;
	//@ assert \at(st->size, Here) == \at(st->size, Pre);
	st->elems[st->size] = x;
	//@ assert HELPER: \at(st->size,Here) == \at(st->size, Pre);
	//@ assert HELPER2: st->elems[\at(st->size, Pre)] == x;
	//@ assert BOUND: 0 <= st->size < st->capacity;
	//@ assert 0 <= st->capacity;
	//@ assert \at(st->size, Here) == \at(st->size, Pre);
	st->size++;
	//@ assert 0 <= st->size <= st->capacity;
	//@ assert 0 <= st->capacity;
	//@ assert \at(st->size, Here) == \at(st->size, Pre) + 1;

}