Ada方面是一个私有的包

Question

假设我拥有世界上最愚蠢的环形缓冲区.

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;

因为我的代码很糟糕,我想添加前置条件和后置条件,以使我不会滥用这个肯定.所以我改变Push的实现如下:

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

但是,我得到一个编译错误,因为我需要将方面定义放在过程的声明中,而不是在实现中.

问题是,这是一个包.我的声明是公开的.前置条件所依赖的值属于包体,声明不可见.为了将方面定义放在声明中,我将不得不重构我的代码以将实现细节暴露给包的公共部分(在本例中为readptr和writeptr).我不想那样做.

我可以想到一些这样的方法,例如让我执行Push()调用私有PushImpl()过程仅在实际上具有前置条件的主体中定义...但这太可怕了.这样做的正确方法是什么？

Answer 1

我认为当验证检查是私有的时,这总是会出现问题,并且解决方案是声明一个函数来进行检查:

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

(Is_Full无论如何都可能有用;在其他情况下可能不是这样).

如果你将实现保留在包体中,你也需要放在Is_Full那里,但你可以将它们移动到规范并使用表达式函数:

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;