A stack is either <B>empty</B>, or it consists of two parts:
<UL>
  <LI>a top element
  <LI>a stack (the remaining elements)
</UL>
<DL>
  <DT><CODE>create_stack</CODE>
  <DD>
      <UL>
        <LI>Inputs: none
        <LI>Outputs: S (a stack)
        <LI>Preconditions: none
        <LI>Postconditions: S is defined and empty
      </UL>
  <DT><CODE>destroy_stack</CODE>
  <DD>
      <UL>
        <LI>Inputs: S (a stack)
        <LI>Outputs: S' (i.e. S changed)
        <LI>Preconditions: none
        <LI>Postconditions: S' is undefined. All resources (e.g.
            memory) allocated to S have been released. No stack
            operation can be performed on S'.
      </UL>
  <DT><CODE>is_empty</CODE>
  <DD>
      <UL>
        <LI>Inputs: S (a stack)
        <LI>Outputs: <CODE>is_empty</CODE> (boolean)
        <LI>Preconditions: none
        <LI>Postconditions: <CODE>is_empty</CODE> is true iff S is
            empty.
      </UL>
</DL>