#include <limits.h>
#include <stdio.h>
#include <stdlib.h>

typedef struct Stack Stack;
struct Stack {
int top;
int capacity;
int* array;
};

/*@
logic integer Capacity{L}(Stack* s) = s->capacity;
logic integer Size{L}(Stack* s) = s->top;
logic integer Top{L}(Stack* s) = s->array[s->top-1];
*/

/*@
predicate Empty{L}(Stack* s) = Size(s) == 0;
predicate Full{L}(Stack* s) = Size(s) == Capacity(s);
*/

/*@
predicate Invariant{L}(Stack* s) =
0 < Capacity(s) &&
0 <= Size(s) <= Capacity(s) &&
\valid_read(s->array + (0..Capacity(s)-1)) && \separated(s, s->array + (0..Capacity(s)-1));
*/

Stack* init(int capacity)
{
Stack* stack = (Stack*)malloc(sizeof(Stack*));
stack->capacity = capacity;
stack->top = 0;
stack->array = (int*)malloc(stack->capacity * sizeof(int));
return stack;
}

/*@
requires valid: \valid(s) && Invariant(s);
assigns \nothing;
ensures full: \result == 1 <==> Full(s);
ensures not_full: \result == 0 <==> !Full(s);
*/
int isFull(Stack* s)
{
return s->top == s->capacity;
}

/*@
requires valid: \valid(s) && Invariant(s);
assigns \nothing;
ensures empty: \result == 1 <==> Empty(s);
ensures not_empty: \result == 0 <==> !Empty(s);
*/
int isEmpty(Stack* s)
{
return s->top == 0;
}

/*@
predicate
Unchanged{K,L}(int* a, integer m, integer n) =
\forall integer i; m <= i < n ==> \at(a[i],K) == \at(a[i],L);

predicate
Unchanged{K,L}(int* a, integer n) =
Unchanged{K,L}(a, 0, n);
*/

/*@
requires \valid(s) && Invariant(s);
assigns s->top;
assigns s->array[s->top];

behavior not_full:
	assumes !Full(s);

	assigns s->top;
	assigns s->array[s->top];

	ensures \valid(s) && Invariant(s);
	ensures size: Size{Here}(s) == Size{Old}(s)+1;
	ensures top: Top(s) == ele;
	ensures not_empty: !Empty(s);
	ensures unchanged: Unchanged{Old,Here}(s->array,Size(s)-1);
	ensures storage: s->array == \old(s->array);
	ensures capacity: Capacity(s) == Capacity(\old(s));

behavior full:
	assumes Full(s);
	assigns \nothing;
	ensures \valid(s) && Invariant(s);
	ensures full: Full(s);
	ensures size: Size(s) == Size(\old(s));
	ensures unchanged: Unchanged{Old,Here}(s->array,Size(s));
	ensures storage: s->array == \old(s->array);
	ensures capacity: Capacity(s) == Capacity(\old(s));

complete behaviors;
disjoint behaviors;
*/
void push(Stack* s, int ele)
{
if (!isFull(s))
	s->array[s->top++] = ele;
}


/*@
requires \valid(s) && Invariant(s);
assigns s->top;
ensures \valid(s) && Invariant(s);

behavior not_empty:
	assumes !Empty(s);
	assigns s->top;
	ensures size: Size(s) == Size{Old}(s)-1;
	ensures !Full(s);
	ensures unchanged: Unchanged{Old,Here}(s->array,Size(s));
	ensures storage: s->array == \old(s->array);
	ensures capacity: Capacity(s) == Capacity(\old(s));
	
behavior empty:
	assumes Empty(s);
	assigns \nothing;
	ensures Empty(s);
	ensures unchanged: Unchanged{Old,Here}(s->array,Size(s));
	ensures size: Size(s) == Size{Old}(s);
	ensures storage: s->array == \old(s->array);
	ensures capacity: Capacity(s) == Capacity(\old(s));

complete behaviors;
disjoint behaviors;
*/
int pop(Stack* s)
{
if (!isEmpty(s))
	return s->array[--s->top];
return -1;
}


int main()
{
Stack* s = init(50);

/*push(s, 1);
push(s, 2);
push(s, 3);

printf("%d ", pop(s));
printf("%d ", pop(s));
printf("%d ", pop(s));*/

return 0;
}