Gappa : automatic proof generation of arithmetic properties

by syoyo

http://lipforge.ens-lyon.fr/www/gappa/

[En]

Gappa is a cool program which validates your floating-point code.

Here is an example of gappa code(Cauculates x * (1-x) in [0, 1]. Taken from gappa’s site).


{ x in [0,1] -> float(x * float(1 - x)) in ? }

Then, gappa automatically computes it’s error bound,


$ echo "{ x in [0,1] -> float(x * float(1 - x)) in ? }" | src/gappa

[rounding_float,ne,24,149](x * [rounding_float,ne,24,149](1 - x)) in [0 {-0}, 1 {1}]

It’s quite nice!

Gappa code format is almost similar to C expression, thus it would be easy to
translate your floating point C code to gappa code.

Gappa is successfully used for CRlibm [1] and CGAL.

[Ja]

Gappa は浮動小数点計算の error bound を自動で計算してくれちゃうらしい。これもすげー。
CRlibm[1] や CGAL の浮動小数点計算の妥当性の検証に gappa が使われているとのこと。
CGAL はグラフィックスのひとなら聞いたことはあるかと思います。有名な幾何計算ライブラリですね。

Gappa はあくまで存在するコードに対して誤差を測定するようなので、
たとえば誤差ターゲットと定義域を指定して最適な sin の多項式近似コードを自動で見つける、
というところまではできないらしい。
CRlibm では多項式近似コードは maple で生成したとのこと。
# Intel’s libm のスライドに CRlibm ってのがあって、これってなんだろうって思っていたのですが、
# Correctly-Rounded libm のことだったのですね。

gappa, caduceus でロバストな floating point 計算コードと C プログラムを書くことができそうです。
あとは GI レンダリングの場合は数値積分やモンテカルロ法などもあるので、
それらも自動で検証できるようなツールもないか探してみたいと思います.
(PVS とかは積分も検証できるみたいですが、GI の場合は discontinuity やら singularity の問題があるので、
まじめに(連続)積分で考えない方がいいと思うので)

[1] CRlibm, an efficient and proven correctly-rounded mathematical library
http://lipforge.ens-lyon.fr/www/crlibm/

Advertisements