Ada aspects which are private to a package

Question

Let's say I have the stupidest ring buffer in the world.

size: constant := 16;
subtype T is integer;

package RingBuffer is
  procedure Push(value: T);
  function Pop return T;
end;

package body RingBuffer is
  buffer: array(0..size) of T;    
  readptr: integer := 0;
  writeptr: integer := 1;

  procedure Push(value: T) begin
    buffer(writeptr) := value;
    writeptr := (writeptr + 1) mod size;
  end;

  function Pop return T
  begin
    readptr := (readptr + 1) mod size;
    return buffer(readptr);
  end;
end;

Because my code sucks, I want to add preconditions and postconditions to make I don't misuse this sure. So I change the implementation of Push as follows:

procedure Push(value: T) with
  pre => readptr /= writeptr
is begin
  buffer(writeptr) := value;
  writeptr := (writeptr + 1) mod size;
end;

However, I get a compile error because I need to put the aspect definitions in the declaration of the procedure, not in the implementation.

The thing is, this is a package. My declaration is public. The values that the precondition is depending on belong to the package body, which isn't visible to the declaration. In order to put the aspect definition in the declaration I'm going to have to refactor my code to expose implementation details into the public part of the package (in this case, readptr and writeptr). And I don't want to do that.

I can think of a few ways round this, such as having my implementation of Push() call a private PushImpl() procedure defined only in the body which actually has the precondition... but that's horrible. What's the right way to do this?

Answer 1

I think this is always going to be a problem when the validation checks are private, and that the solution is to declare a function to do the check:

package RingBuffer is
   function Is_Full return Boolean;
   procedure Push(value: T) with Pre => not Is_Full;
   function Pop return T;

(Is_Full is probably useful anyway; in other cases it might not be so).

If you leave the implementation in the package body, you’ll need to put Is_Full there too, but you could move them to the spec and use an expression function:

package RingBuffer is
   function Is_Full return Boolean;
   procedure Push(value: T) with Pre => not Is_Full;
   function Pop return T;
private
   buffer: array(0..size) of T;
   readptr: integer := 0;
   writeptr: integer := 1;
   function Is_Full return Boolean is (Readptr = Writeptr);
end RingBuffer;

Answer 2

The contract aspects are intended to be used in the public view of (sub)types and subprograms.

If you want to keep the check in the private view, then it is simple to write it as the first statement in the subprogram:

begin
   if Is_Full then
      raise Constraint_Error with "Ring buffer is full.";
   end if;
   ...

Some unsolicited advise:

• Make the contracts public, so the users of the package can see how it should be used.
• Insert a similar Is_Empty check when popping an item from the buffer.
• Make your index type modular: type Indexes is mod 16;