13. 契約プログラミング

1. はじめに

Sather は Eiffel から契約による設計 (DBC) を引き継ぎました DBC は呼び出し元が満たすべき条件 (precondition) と呼び出される側が保証すべき条件 (postcondition) からなっています。

Sather はそのほかに assert, invariant などの実行時安全ネットを用意しています。

これらの安全ネットを働かすかどうかはコンパイル時に決定することができます。詳しくは sacomp man page をみてください。大規模プログラムを作成するときにはどんなバグが潜んでいるか予期できないので、なるべく安全ネットを働かせるようにしましょう。

2. precondition

呼び出し元が保証すべき条件です。この条件が満たされないとき呼び出される側は文句を言ってプログラムが終了します。
以下のコードは array.sa の一部です。大きさを指定して ARRAY のインスタンスを作るときは、大きさは非負である必要があります。

   create(n:INT):SAME pre n>=0 is 
      -- Create a new array of size `n' all of whose elements are void.
      return new(n) end;

3. postcondition

呼び出された側が保証すべき条件です。この条件が満たされないと呼び出し側は文句を言ってプログラムが終了します。メッソドからの返り値は、予約語 'result' であらわします。

以下のコードは前に示した point.sa にセーフティネットをつけたものの一部です。


   const eta:FLT:= 0.00001;       -- 誤差の許容範囲

-- (中略)

   abs:FLT 
      post result >=0.0               -- 長さが正であることを確認
   is
      return (x*x+y*y).sqrt;
   end;

   rotate(theta:FLT):SAME 
      post result.abs/abs > 1.0-eta and result.abs/abs < 1.0+eta  -- 回転前後で原点からの距離の変化が
   is                                                                   -- 許容範囲以内に収まっていることを確認
      theta := y.atan2(x)+theta;
      return #SAME(self.abs*theta.cos, self.abs*theta.sin);
   end;

4. assert

メソッドの内部におきます。assert が false を返すと文句を言って終了します。

以下のコードも point.sa にセーフティネットをつけたものの一部です。

   out2file(a0,a1:ARRAY{POINT}) 
      pre a0.size > 0 and a1.size > 0  -- 配列の大きさが 0 より大きい事を前提とする。
   is
      f:FILE:=FILE::open_for_write(fout);
      assert ~f.error;        -- ファイルが開けなければ文句を言って終了
      p0,p1:POINT;
      i:INT;
      loop
	 i:=(a0.size+1).times!;
	 if i = a0.size then i:=0; end;
	 p0:=a0[i];
	 p1:=a1[i];
	 f + p0.x + "\t" + p0.y + "\t" + p1.x + "\t" + p1.y + "\n";
      end;
      f.close;
   end;

5. invariant

invariant：BOOL は特殊なメソッドで、インスタンスがこれを満たさなくなると文句を言って終了します。あまり使われることはありません。また、Sather-1.2.2 ではうまく働かないみたいです。

6. セーフティネット付 point.sa

付録にセーフティネット付 point.sa (point2.sa) をつけておきますので遊んでみてください。コンパイルするときに -chk オプションをつけます。

$ sacomp -chk point2.sa -o point2

7. 終わりに

今回は Sather の契約プログラミングについて述べてみました。これは大規模ソフトウェアを開発するときに有効な手法です。普段から pre, post, assert を使う癖をつけておくと良いかもしれません。