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) に公開する必要があります。そして、私はそれをしたくありません。

私はこれを回避するいくつかの方法を考えることができます.callの実装を、実際に前提条件を持つ本体でのみ定義されPush()たプライベートPushImpl()プロシージャにするなどです...しかし、それは恐ろしいことです。これを行う正しい方法は何ですか？

4

2 に答える 2

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 に答える