1

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

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()仅在实际上具有前提条件的主体中定义的私有过程......但这太可怕了。这样做的正确方法是什么？

4

2 回答 2

5

我认为当验证检查是私有的时这总是一个问题，解决方案是声明一个函数来进行检查：

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;
于 2014-04-21T19:37:08.493 回答
2

合同方面旨在用于（子）类型和子程序的公共视图。

如果要将检查保留在私有视图中，则将其编写为子程序中的第一条语句很简单：

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

一些不请自来的建议：

  • 将合同公开，以便包的用户可以看到应该如何使用它。
  • Is_Empty从缓冲区弹出项目时插入类似的检查。
  • 使您的索引类型模块化：type Indexes is mod 16;
于 2014-04-22T07:58:13.043 回答