
#ifndef STACKCAPACITYSIZETOP_H_INCLUDED
#define STACKCAPACITYSIZETOP_H_INCLUDED

#include "stack/stack_definition.h"

/*@
  logic size_type Capacity{L}(Stack* s) = s->capacity;

  logic size_type Size{L}(Stack* s) = s->size;

  logic value_type* Storage{L}(Stack* s) = s->obj;

  logic value_type Top{L}(Stack* s) = s->obj[s->size-1]; 
*/

#endif /* STACKCAPACITYSIZETOP_H_INCLUDED */

