Skip to main content

ADT of stack: value and operator definition

Short answer

ADT specification includes value definition (abstract typedef describing the set of values) and operator definition (header, precondition, postcondition). For STACK, the value is an ordered sequence accessible only at the top; operations push, pop, empty, and stacktop are defined with preconditions (e.g., pop on non-empty stack) and postconditions that specify the LIFO behavior without storage details.

Describe value definition and operator definition of ADT and apply it to describe STACK.

Value definition and operator definition

An ADT specification has two parts.

  • Value definition: describes the set of values of the type. It has the keyword abstract typedef (the type and its structure) and an optional condition that restricts the values.
  • Operator definition: gives each operation as a header (name and parameters), an optional precondition (what must be true before the call) and a postcondition (what is true after the call). Together they describe the effect without implementation.

Applying it to STACK

A stack is an ordered collection of elements in which insertion and deletion take place only at one end, the top (LIFO).

/* Value definition */
abstract typedef <<eltype>> STACK(eltype);
   /* an ordered sequence of items of type eltype; the first item is the top */

/* Operator definition */
abstract empty(s)
   STACK(eltype) s;
   postcondition empty == (len(s) == 0);

abstract push(s, elt)
   STACK(eltype) s;  eltype elt;
   postcondition s == <elt> + s(before);          /* elt becomes the top */

abstract eltype pop(s)
   STACK(eltype) s;
   precondition  empty(s) == FALSE;               /* no pop on empty stack */
   postcondition pop == first(s(before));         /* returns old top     */
                 s == sub(s(before), 1, len(s(before)) - 1);

abstract eltype stacktop(s)
   STACK(eltype) s;
   precondition  empty(s) == FALSE;
   postcondition stacktop == first(s);            /* read top, no removal */

The preconditions of pop and stacktop correspond to the stack underflow check in any implementation.

✓ Answer checked by Claude Opus 5.5 (high effort)

Related questions

All Data Structure and Algorithm chapter 1 questions →