How to incorporate proof aspects into the specification so that every function and procedure has a Post aspect and, if required, a Pre aspect

Question

How to incorporate proof aspects into the specification so that every function and procedure has a Post aspect and, if required, a Pre aspect that outlines the proper behaviour of the code below:

package Stack with SPARK_Mode is
pragma Elaborate_Body;

   Stack_Size : constant := 100;
   type Pointer_Range is range 0 .. Stack_Size;
   subtype Index_Range is Pointer_Range range 1 .. Stack_Size;
   type Vector is array(Index_Range) of Integer;

   S: Vector;
   Pointer: Pointer_Range;

   function isEmpty return Boolean;
   procedure Push(X : in Integer)
     with
       Global => (In_out => (S, Pointer)),
       Depends => (S => (S, Pointer, X),
                   Pointer => Pointer);

   procedure Pop(X : out Integer)
     with
       Global => (input => S, in_out => Pointer),
       Depends => (Pointer => Pointer,
                   X => (S, Pointer));

end Stack;

Answer 1

In brief, you should add a Post-condition aspect to every subprogram in the package, and a Pre-condition aspect to those subprograms that need it.

Preconditions and postconditions in Ada are explained at http://www.ada-auth.org/standards/22rm/html/RM-6-1-1.html.

What is your problem, really? Is it about the syntax of the pre/post-condition aspects, or about their content and meaning? Or is it about the meaning of "proper behaviour" in the problem statement? In the last case, try to imagine what might be improper behaviour, or incorrect use, of a Push or Pop operation on a stack with a fixed maximum size.