General Information
Tutorials
Reference Manuals
Libraries
Translation Tasks
Tools
Administration
|
|
Abstract data types to be used in specifications
This module implements a stack named NAMEStack,
whose elements are of type TYPE.
Values of this type can be pushed onto the stack and popped off of it in
the usual way, and in addition each element of the stack can be indexed
directly and its value obtained.
All of the operations exported by this module are implemented as macros,
using the facilities of the obstack module
(see Memory Object Management of Library Reference Manual).
The module is instantiated by
$/Adt/Stack.gnrc +instance=NAME +referto=TYPE :inst
where NAME identifies the Stack instance and TYPE
is the element type.
All entities exported by this module can be used in specifications
of type .lido, .init, .finl, and .con.
They can also be used in .pdl specifications or in C modules
if the interface file NAMEStack.h is imported there.
The following macros are supplied by the module:
int NAMEStackEmpty
- Yields the value 1 if the stack has no elements, 0 otherwise.
This operation must appear in an expression context.
size_t NAMEStackSize
- Yields the number of elements in the stack.
This operation must appear in an expression context.
void NAMEStackPush(TYPE v)
- Push an element onto the stack.
The parameter
v must be an expression that yields a value of type
TYPE. That value becomes the new top element of the stack.
The previous top element becomes the new second element, and so on.
This operation must appear in a statement context.
TYPE NAMEStackPop
- Remove the top element of the stack.
The previous second element becomes the new top element, and so on.
This operation must appear in an expression context, and yields the value
(of type TYPE).
TYPE NAMEStackTop
- Obtain the contents (of type
TYPE)
of the top element of the stack without changing the state of the stack.
This operation must appear in an expression context.
TYPE NAMEStackElement (i)
- Obtain the contents (of type
TYPE) of a specific element of the stack
without changing the stack. The argument gives the distance of the desired
element from the top of the stack (0 for the newest element, 1 for the next
newest, and so on).
There is no check on the validity of the value of i.
This operation must appear in an expression context.
TYPE NAMEStackArray (i)
- Obtain the contents (of type
TYPE)
of a specific element of the stack without changing the state of the stack.
For the purpose of this operation, the stack is considered to be an array.
Element 0 is the oldest value on the stack, element 1 is the next oldest,
and so on.
There is no check on the validity of the value of i.
This operation must appear in an expression context.
void ForEachNAMEStackElementDown (i)
- Cycle through the elements of the stack, from the most recent to the oldest.
The parameter
i must be declared as an lvalue of type
TYPE* and will point, in turn, to each element of the stack.
This operation must appear in a context where
for (i=...; i>=...;i--) is allowed.
void ForEachNAMEStackElementUp (i)
- Cycle through the elements of the stack, from the oldest to the most
recent.
The parameter
i must be declared as an lvalue of type
TYPE* and will point, in turn, to each element of the stack.
This operation must appear in a context where
for (i=...; i<...;i++) is allowed.
|
