Why

アルゴリズムの正しさを証明するためのシステムとしてWhyをいうのがある。
こいつはoccaml風のアルゴリズム＋アサーションを入力として、各種定理証明器向けの入力を
出力するという代物です。

下はsqrtの例ですが、ここまで書かないと正しさを証明はできないということです！

let sqrt = fun (x : int) ->
  { x >= 0 }
  begin
    if x = 0 then 0 else
    if x <= 3 then 1 else	
      let y = ref x in let z = ref (x+1)/2 in
      begin
	while !z < !y do 
	  { invariant 
	      z > 0 
	  and y > 0 
	  and z = (x/y+y)/2
	  and x < (y+1)*(y+1) 
	  and x < (z+1)*(z+1)
	      variant y} 
	  y := !z;
	  z := (x / !z + !z) / 2
	done;
	!y
      end
  end		
  { result * result <= x and x < (result+1)*(result+1) }