日本ソフトウェア科学会第 34 回大会 (2017 年度) 講演論文集

Why3 を用いた区間演算ライブラリの検証
薮 智仁

石井 大輔

区間演算ライブラリは浮動小数点数を境界とした区間同士の四則演算を提供する. 演算が返す値は, 引数の区間中の各値についての演算結果と境界の演算による丸め誤差を含む区間である. 一般に区間演算のアルゴリズムは多数の条件分岐や丸め演算などにより複雑で, その実装の信頼性は高くない. 本研究の目的は正しさが検証された区間演算ライブラリの提供である. 検証には Why3 プラットフォームを用い, アノテーション付き実装から検証条件を生成し,SMT ソルバーと Coq により証明する. 検証プロセスにおいて非線形項を含む検証条件や浮動小数点数の複雑な公理を扱うため, (1) 浮動小数点数定理の実数定理による言い直し, (2) 区間の上下限による定理分割, (3) 中間変数による補助定理, の三つの戦略を用いた. その結果, 区間演算ライブラリに関するすべての検証条件を証明することができた.

Interval arithmetic libraries provide the four operators on the argument intervals whose bounds are floating-point numbers.
A returned value of the operators is another interval that contains every true values computed from the real values within
the arguments, plus rounded errors caused by the computation at the bounds. In general, an actual implementation should
be complicated because of large case analysis and round operations. As the existing code bases are implemented by humanhands, their correctness is not obvious, which come to be critical for the reliability. This work provides a mechanicallyverified implementation of the interval arithmetic library. For the verification, we utilize the Why3 platform and generates theverification conditions (VCs) from the specification; then, the Alt-Ergo SMT solver and the Coq proof assistant are applied
to the VCs to discharge all of them. To discharge all VCs, we use three strategies, (1) Restatement in the real theory, (2) Split
into the lower and upper part, and (3) Lemmas on intermediate variables. Finally, a mechanically-verified and executable
implementation of the interval arithmetic is provided.

め, 信頼性は低く, 当初の目的であった高信頼性を損

1 はじめになう恐れがある.

区間演算 (2 節) は実数を扱うための高信頼な手法

Why3 (3 節) は, 自動定理証明器 (例: SMT ソルバー)

である. 区間演算は数値の代わりに (一般的には浮動や対話定理証明器 (例: Coq) を統合するよう設計され小数点数の) 区間を扱い, 真の解を逃さないように慎たプログラム検証プラットフォームである. Why3 は

重な丸め方向の制御を行いながら演算を行う. 区間の検証対象を記述する仕様言語 WhyML と Why3 を提供し四則演算は引数として与えられる区間の境界のみをており, アノテーション付きプログラムを記述するこ

計算する効率的な方法で実装できる. 実装では繰り返とができる. ある仕様が与えられると, Why3 はその仕し処理は必要ないが, 多数の場合分けを行う. これは様を全て満たすことを保証するための検証条件 (VC)

引数区間の境界同士, 0 との大小関係, 特殊な値 ±∞ とを生成する. そしてユーザーがバックエンド証明器をNaN , を区別するためである. 例えば kv ライブラリの適用し, 生成されたすべての VC の証明することで, 与乗算の実装は 17 個の分岐を持つ. 基本的に既存の区えられた仕様の正しさを証明する. Why3 と Why3 の間演算プログラムは人間の手により実装しているた

バックエンド証明器は, 数値計算分野もサポートする
ように開発されてきた.

∗ Verification of Interval Arithmetic Library Using Why3.

This is an unrefereed paper. Copyrights belong to the Author(s).
Tomohito Yabu, Daisuke Ishii, 福井大学, University of Fukui.

我々の目標 (4 節) は正しさの検証された区間の四則演算プログラムを提供することである. 目標のために,
我々は kv ライブラリの実装を WhyML に変換し, Why3

の事前・事後条件をアノテーションする. 生成された

実際の実装は区間の境界同士のみを演算することですべての VC について, バックエンド証明器に SMT実装できる. 演算結果が表現不可能になった際は, 上

ソルバー (Alt-Ergo と Z3) と Coq を用い証明すること

下限をそれぞれ上向きと下向きに丸める. つまり理論

で, 区間演算プログラムの正しさの検証を行う (5 節) .

値より広い区間に近似する. なお, ある実数 x ∈ R に

検証プロセスは簡単ではない. 例えば SMT ソル

対して ▽(x), △(x) ∈ F ∪ {−∞, +∞} は, それぞれ x の下

バーは非線形項を含む検証条件を扱うことができず,向きと上向きの丸めを表す. ここで実装のための基礎

また回避策としての対話証明は膨大な数の浮動小数定理を導入する.

点数定理により困難である. そのため Why3 の単純な定理 2.2 (四則演算の実装) x, y ∈ I について以下が成利用では全ての VC を証明することはできない.
証明できない VC を検証するため, 我々は仕様に検り立つ:

証プロセスを支援する補助定理をアノテーションする

x + y = [▽(x + y), △(x + y)]

三つの戦略を提案する (6–7 節) .

x − y = [▽(x − y), △(x − y)]

区間の四則演算の検証実験において, アノテーション
された補助定理は証明タスクを徐々に簡単なタスクに(2.2)

x ∗ y = □{x y, x y, x y, x y}
x / y = x ∗ [▽(1 / y), △(1 / y)](0 < y)

分割し, 最終的にはバックエンド証明器 (特に Alt-Ergoと Coq) によりすべての VC を証明する (8 節) . 結果
として機械的に正しさが検証され, かつ実行可能な区

2. 1 区間演算の実装
区間演算を実装したライブラリは, Profil/Bias †1,

filib †2, INTLAB †3, kv †4 などがある.

間演算プログラムが提供できる.

区間演算のうち, 乗除演算は複数の場合分けに基づ

2 区間演算いて実装されている. これは, 効率的な演算や, 浮動小

区間演算 [7] は, 実数が厳密には表現不可能な計算機

数点数の演算結果が ±∞ や NaN になる場合を考慮す

上で高信頼な数値計算を行うための手法である. 区間
演算は実数演算を区間の演算に拡張したもので, 数値の代わりに真解を含んだ区間値を計算し, 結果としてるためである.
区間演算を実装コードのある分岐に着目し, その計算を取り出したものを以下のように形式化する:

得られる区間は演算がとりうるすべての結果を含む.

(有限) 区間 x = [x, x] は集合 {x ∈ R : x ≤ x ≤ x} と定義 2.3 (実装関数とその正しさ) 区間の集合を I :=して定義する. ただし x ≤ x とする. 実際の区間の実IR または I := IF, 演算 ⊙ ∈ {+, −, ∗, / } , 関係 B ⊆ I2 と装では, 下限 x と 上限 x は F ∪ {−∞, +∞} に制限する.

したとき, 実装 f ⊙, B は I × I から R ∪ {−∞, +∞, NaN}

ただし F は ±∞ と NaN を除いた浮動小数点数の集合の (連結) 部分集合への関数である.「 f ⊙, B は 正しい 」とし, F ∪ {−∞, +∞, NaN} を F∗ とする. 実数を境界との必要十分条件を以下に示す:する区間の集合は IR と表し, 浮動小数点数を境界とする場合は IF と表す. IR と IF を特に区別しない場
合は I と表す. ある実数の集合 S ⊆ R に対して, 包囲□S ∈ I は S ⊆ □S を満たす最小幅の区間である. ここで区間の四則演算を定義する.

したとき, 区間の四則演算は以下のように定義される:
ただし ⊙ = / の際は 0 < y と仮定する.

∀ x̃ ∈ x, ∀ ỹ ∈ y, x̃ ⊙ ỹ ∈ f ⊙, B (x, y)(2.3)

式 (2.3) では, 後件の一つ目の部分は演算結果が適切な区間かのチェックであり (例: 境界が NaN でない,
かつ大小関係を満たす) , 二つ目の部分は真値を含ん

定義 2.1 (区間の四則演算) x, y ∈ I, ⊙ ∈ {+, −, ∗, / } とx ⊙ y := □{x ⊙ y : x ∈ x, y ∈ y}∀x ∈ I, ∀y ∈ I, B(x, y) ⇒ f ⊙, B (x, y) ∈ I ∧(2.1)†1 http://www.ti3.tuhh.de/keil/profil/index_e.html†2 http://www2.math.uni-wuppertal.de/~xsc/software/
filib.html†3 http://www.ti3.tu-harburg.de/rump/intlab/†4 http://verifiedby.me/kv/

3. 1 Flocq

でいるかのチェックである.

Flocq †9 [3] は Coq 上で浮動小数点数を扱うための例えば乗算のときに, B がx≥0 ∧ x,0 ∧ y≥0 ∧ y,0(2.4)

ライブラリである. Flocq は, 様々な基数 (2, 10 や, 奇数の基数も) やビット数の浮動小数点数, 様々な丸めで, 実装f∗, 式 (2.4) (x, y) := [▽(x y), △(x y)](2.5)の場合が考えられる.

の指定をサポートしており, 450 を超える定理を持ち,約 12000 行からなる.

Why3 により浮動小数点数を用いた仕様から VC を

3 Why3 プラットフォーム

生成し, Coq 上で対話証明を行う際, Why3 は Flocq にWhy3 †5 [2] は演繹的プログラム検証のためのプラッ基づいた Coq の定理を生成する.

トフォームであり, 三つの機能 (1) 検証対象を記述する
ための仕様言語, (2) 仕様付きプログラムから最弱事前

4 区間演算ライブラリの正しさの検証

条件の計算に基づき 検証条件 (Verification Condition,

本研究の目標は, 区間演算ライブラリの正しさの検VC) を生成する機能, (3) VC を使用するバックエン証である. 正しいとは, 適切な区間が与えられた時に,ド自動・対話定理証明器に中継する機能, を提供しプログラムの出力結果が, 理論値を包囲する適切な区ている. Why3 は OCaml 風の言語を二つ持つ. 命令

間になっていること (式 (2.3)) である.

型プログラムを記述するための プログラミング言語

大まかな検証の流れは以下の四ステップからなる:

WhyML と, プログラムに仕様として付与する一階述(1) kv ライブラリの四則演算コードを WhyML に書き

語論理式を記述するための 論理言語 Why3 である.

直し, 区間演算の定義を Why3 でアノテーションし, (2)Why3 のバックエンド証明器には, SMT ソルバー [8]Why3 が記述コードから生成した VC に対して, SMT(例: Alt-Ergo †6), 定理証明支援系 (例: Coq †7) など

ソルバーにより自動証明を試み, (3) 自動証明できながある. なお, SMT ソルバーをバックエンド証明器

い VC を Coq により対話証明を試み, (4) それでも VCとして用いた場合の結果は, (1) 検証条件の妥当性をを証明できない場合は, 本研究の提案する三戦略を用

判定 (Valid / Invalid), (2) 制限時間までに停止しないい証明する.

(Timeout) , (3) 決定不能 (Unknown) を出力, のいずれ

5 節 で VC の検証基本プロセスを示し, 6–7 節で基かとなる. Why3 は GUI も提供しており, 生成された本プロセスでは VC が証明できない場合に我々が提案

VC の一覧表示, VC の変形 (例: 複数の VC への分割),する効果的な三戦略を示し, 8 節 で実験結果を示す.

VC への証明器の割り当て, 証明器の入力・出力の確認などが行える.

WhyML と Why3 言語は実数用の real 型や, 64 ビッ

本研究で検証する VC (式 (2.3) を言い換えたもの)
は実数, 浮動小数点数, 区間の変数を含む一階述語論
理式として形式化できる.

ト浮動小数点数を表す double 型, さらにユーザー定義のレコード型などを提供する型システムを備える.

定義 4.1 (検証条件) I := IR または I := IF の区間 x とどちらの言語も仕様ごとに module または theory とy, 実装する演算子 ⊙, そして関係 B ⊆ I2 を仮定し, 式

してカプセル化するモジュールシステムを持つ. 標準

VC I⊙, B と VCC⊙, B を以下のように定義する:モジュールは標準ライブラリとして備わっている.

Why3 は数値計算ブログラムの検証に用いられてきた実績を持つ [1] [4] †8.
†5
†6
†7
†8

http://why3.lri.fr
http://alt-ergo.lri.fr
https://coq.inria.fr
参考文献は Why3 の前身での研究である.

VC I⊙, B :≡ B(x, y) ⇒ f ⊙, B (x, y) ∈ I
VCC⊙, B :≡ B(x, y) ⇒ ∀ x̃ ∈ x, ∀ ỹ ∈ y, x̃ ⊙ ỹ ∈ f ⊙, B (x, y)
このとき f ⊙, B は 2. 1 節 の実装関数を表す.

VC I⊙, B は演算結果が適切な区間であることをいい,†9 http://flocq.gforge.inria.fr

1
2

module IntervalMulExact
use import real.Real

3

type interval = { inf: real; sup: real }invariant { self.inf <= self.sup }4
5

predicate _in (a: real) (x: interval) =x.inf <= a <= x.sup

78

let make_zero () : interval
ensures { _in 0. result }= { inf = 0.; sup = 0. }

10
11
12
13

16
17
18
19
20
21
22
23
24
25
26
27
28

上下限値の大小関係を不変条件 (invariant) としてアノテーションする (5 行目) . そして, 7–8 行目であを定義する. さらに, 10–12 行目で 0 を含む区間を生成する WhyML 手続き make_zero を定義する. 最後に,

9

15

を WhyML のレコードとして定義する. このとき区間のる区間 x が, ある実数 a を含んでいるという述語 _in

6

14

ぎに, 4 行目で下限 (inf) と上限 (sup) を持つ区間型

let multiply (x y: interval) : interval
ensures { forall xx yy: real.
_in xx x /\ _in yy y ->_in (xx * yy) result }= if x.inf >= 0. thenif x.sup = 0. then make_zero ()else
if y.inf >= 0. thenif y.sup = 0. then make_zero ()else{ inf = x.inf * y.inf;
sup = x.sup * y.sup }else(* 省略 *)
end

14–27 行目で WhyML の区間の乗算手続き multiply を定義する. multiply は kv ライブラリにならった実装となっており, 13 個の分岐を持つ.

5. 2 検証
前節で書いた仕様の正しさを検証する. まず一つ目の検証ステップとして, Why3 プラットフォームを用いて手続き make_zero と multiply のそれぞれについて VC を生成し, バックエンド SMT ソルバーにより VC の証明を試みる. 5. 1 節 の例では, Alt-Ergo を用いて make_zero に対して生成された VC の証明を

1 秒以内で行うことができた. これはアノテーション
された手続きが正しいことを意味する. しかし, もう一方の multiply の VC を Alt-Ergo を用いて証明しよ

図1

実数境界区間の乗算コードの抜粋. スペースの関係で

multiply の 13 個の分岐中 10 個は省略.

うとすると, 1 分経っても終了しなかった. この場合,

VC を 22 個の部分的な VC に 分割 (split) し, 証明を試みる. SMT ソルバー (Alt-Ergo と Z3) は 22 個のう

VCC⊙, B は演算結果が演算 ⊙ の真の結果を含むこと

ち 14 個を証明し, 残りは 8 個となった.

をいう. 本研究の目標とする, 区間演算ライブラリの二つ目の検証ステップとして, Coq を用いた対話証

正しさの検証は, 検証対象から生成された VC I⊙, B と
VCC⊙, B が正しいことを, Why3 のバックエンド証明器

明を行う. ここでは, 図 1 の最後の分岐を取り上げ説を用いて証明することで行う.

条件式 (2.4) を満たしている. 8 個の未証明の VC はこ

明する. 最後の分岐では multiply の引数が 2. 1 節 のの分岐に関するものであり, 以下の形になっている.

5 実数境界区間版の四則演算の検証≡ (式 (2.4)) ⇒VCC∗, 式 (2.4)

本節では, 検証の基本プロセスを説明し, 浮動小数∀ x̃ ∈ x, ∀ ỹ ∈ y, x̃ ỹ ∈ f∗, 式 (2.4) (x, y)

点数を扱う検証との比較のために, 実数を境界に扱う

ここで f∗, 式 (2.4) の定義は 式 (2.5) である (丸め演算「理想的な」区間演算のプログラムを考える.

は冗長であるが) .

(5.1)

まず始めに, Why3 は VC (5.1) と関連する公理を

5. 1 仕様

Coq の記述に変形する. これは以下のように Coq の証

Why3 の仕様言語による区間の乗算コードを 図 1 に明コンテキスト †10 に表示される:示す. まず, 2 行目で実数 theory (実数型 real や実数型の演算, 公理など) を現在の名前空間に導入する. つ†10 正確には読み込んだ VC に簡略化 (例: 変数名の置換,
前提の選別, 区間コンストラクタの展開) を施したも
のである.

表1

x.inf, x.sup, y.inf, y.sup ∈ R
H0 : x.inf ≤ x.sup

浮動小数点数と丸め演算の語彙の抜粋.

H1 : y.inf ≤ y.sup

述語/関数

定義

H2 : 0 ≤ x.inf

H3 : x.sup , 0

is_finite xx∈F

H4 : 0 ≤ y.inf

H5 : y.sup , 0

is_plus_infinity x

x = +∞

H6 : x.inf · y.inf ≤ x.sup · y.supdouble_le_real x yx ≤ y (x ∈ F∗, y ∈ R)

ge_zero x

0 ≤ x (x ∈ F∗ )is_gen_zero x

x = 0 (x ∈ F∗ )mul_down x y▽(x y) (F∗ ×F∗ → F∗ )mul_post d x y r

r = mul_down x y

xx, yy ∈ R

H7 : x.inf ≤ xx ≤ x.sup

H8 : y.inf ≤ yy ≤ y.sup.

x.inf · y.inf ≤ xx · yy ≤ x.sup · y.sup(d = Down のとき)

この VC は非線形項を含んでいる. 多くの SMT ソル
バーは非線形項を扱うことができない. つぎに, 前提

H0 –H8 の組み合わせと, Coq の Reals モジュールのための追加の分岐と丸め演算を除いて, 基本的に 図 1

定理 Rmult_le_compat (式 (5.2)) , Rmult_le_compatと同じである. 9–10 行の invariant は区間の境界が(式 (5.3)) を用いることで, このコンテキストのゴール

NaN の場合や [−∞, −∞] と [+∞, +∞] の区間を禁止しは証明できる.

ている. 述語 _in はある real の値がある double-境界区間に含まれていることをいう (12 行目) . 手続き∀r 1, r 2, r 3, r 4 ∈ R, 0 ≤ r 1 ⇒ 0 ≤ r 3 ⇒r1 ≤ r2 ⇒ r3 ≤ r4 ⇒ r1r3 ≤ r2r4

(5.2)

whole は区間 [−∞, +∞] を返す (18–20 行目) . 22–35∀r 1, r 2, r 3 ∈ R, r 1 ≤ r 2 ⇒ r 2 ≤ r 3 ⇒ r 1 ≤ r 3 (5.3)

行目の手続き multiply は 17 個の分岐からなる. こ

最終的な証明は 20 個のタクティック適用からなる †11.

れは 図 1 の 4 個の分岐が, それぞれ無限大の境界を扱

この分岐に対応するもう一つの VC I∗, 式 (2.4)

も同様に Coq で証明できる. さらに乗算の他の分岐も, また

うため 26 行目のように分岐が増え, 8 個の分岐になるためである.

乗算以外の三演算についてもこの方法で証明できる.
これまでみてきたように, 実数演算プログラムの仕6. 2 検証の最初の試み

様の検証には SMT ソルバーによる自動証明ができる

図 2 の丸め演算つき区間の乗算コードについて,ものもあれば, できないものもある. しかしできない

Why3 は 3 個の VC を生成し, さらに GUI のインター

場合も対話証明により検証を試みることができる.

フェイスを通して 32 個の VC に分割する. 図 2 の最後の分岐は, 5. 2 節 の条件式 (2.4) の場合であり, 同

6 浮動小数点数境界の区間演算の検証

じ VCC

つぎに浮動小数点数を境界とする区間演算の検証の内部表現 (Why3 による仕様) を 図 3 に示す. 変数に進める.

∗, 式 (2.4)

が生成される. この VC の Why3 上でxinf, xsup, yinf, および ysup は引数区間の境界を表し, 11–12 行目の rinf と rsup は乗算結果区間の境界

6. 1 仕様を表す. 2–5 行目と 13–14 行目は適切な区間であるこ

WhyML と Why3 の乗算の仕様を 図 2 に示す. まず始とをいい †12, 15–17 行目は乗算結果が真値を含むことめに, 浮動小数点数と丸め演算の定理を導入する (3–6をいう.

行目) . 導入する語彙の一部を 表 1 に示す. 残りの仕様

5. 2 節同様, 検証プロセスの一つ目のステップとしは, double の値の扱いや特殊な値 (例: ±∞ や NaN) のて自動証明を適用し, Alt-Ergo は 15 個の VC を 150 秒†11 証明は fourier タクティックによりさらに簡略化できる.

†12 VC を分割したため, VCC
では式 (2.3) の後件∗, 式 (2.4)
Iの一つ目である VC∗,
は前提に入る.
式 (2.4)

1
2
3
4
5
6

module IntervalMulRounded
use import real.Realuse import floating_point.Rounding
use import floating_point.SpecialValues
use import floating_point.DoubleFull
use import double_wrapper.DoubleWrapper

7
8
9
10

type interval = { inf: double; sup: double }invariant { (is_finite self.inf \/ is_minus_infinity self.inf)/\ (is_finite self.sup \/ is_plus_infinity self.sup) /\ le self.inf self.sup }11
12

predicate _in (a: real) (x: interval) = double_le_real x.inf a /\ real_le_double a x.sup

13
14
15
16

let make_zero () : interval
ensures { _in 0. result }= { inf = double_zero; sup = double_zero }

17
18
19
20

let whole () : interval
ensures { forall r:real. _in r result }= { inf = minus_infinity; sup = plus_infinity }

21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36

let multiply (x y: interval) : interval
ensures { forall xx yy: real. _in xx x /\ _in yy y -> _in (xx * yy) result }= if ge_zero x.inf then
if is_gen_zero x.sup then
if is_infinite y.inf || is_infinite y.sup then whole () else make_zero ()else
if ge_zero y.inf then
if is_gen_zero y.sup then
if is_infinite x.inf || is_infinite x.sup then whole () else make_zero ()else(* 補助定理をここに追加する *){ inf = mul_down x.inf y.inf; sup = mul_up x.sup y.sup }else(* 省略 *)
end

図2

浮動小数点数の乗算のコードの抜粋. スペース制限のため multiply は 5 個の分岐のみ示す.

以内で証明する. しかし VCC∗, 式 (2.4)

を含めた 17 個の宣言は追加の前提を導入するためである. また F∗ 値
域は実数の述語を用いて表現されるため, 上の Coq の

VC は 4 分経っても証明できない †13.
二つ目のステップとして, Coq を起動し未証明の VC

コンテキストはさらに複雑になる. そのため, 5. 2 節の対話証明を試みる. しかし浮動小数点数を扱う実装

同様に, 実数の定理 (例: 式 (5.2) や 式 (5.3)) を適用すのため, Why3 によって変換された Coq の定理は 5. 2 節

る場合, F∗ を展開する必要があり複雑化する. 結果との定理と比較して複雑になる. 例えば, VCC

して, 例え基本演算を考えたときでさえ, 多くの VC の∗, 式 (2.4)のCoq のコンテキストを 図 4 に示す. このように複雑手による証明は困難である.

になる理由は, 浮動小数点数の区間はユーザー定義オ
ブジェクトで表現され, 表 1 の語彙を用いるすべての7 補助定理による検証
丸め区間演算コードから生成された VC の証明が難†13 他の SMT ソルバー (例: Z3 や CVC4) も同様に証明できない.

しい場合に, 証明に有効な戦略がある. 本研究のアプ

1
2
3
4
5

forall (xinf:double) (xsup:double) (yinf:double) (ysup:double),((is_finite xinf) \/ (is_minus_infinity xinf)) /\((is_finite xsup) \/ (is_plus_infinity xsup)) /\ (le xinf xsup) /\((is_finite yinf) \/ (is_minus_infinity yinf)) /\((is_finite ysup) \/ (is_plus_infinity ysup)) /\ (le yinf ysup) ->678(* 分岐条件 *)(ge_zero xinf) -> (~ (is_gen_zero xsup)) -> (ge_zero yinf) -> (~ (is_gen_zero ysup)) ->

9
10
11
12
13
14
15
16
17

(* 区間の乗算 *)forall (rinf:double), (mul_post Down xinf yinf rinf) ->forall (rsup:double), (mul_post Up xsup ysup rsup) ->((is_finite rinf) \/ (is_minus_infinity rinf)) /\((is_finite rsup) \/ (is_plus_infinity rsup)) /\ (le rinf rsup) ->forall (xx:R) (yy:R),(_in xx (mk_interval xinf xsup)) /\ (_in yy (mk_interval yinf ysup)) ->(_in (xx*yy) (mk_interval rinf rsup)).

図3

Why3 でエンコードされた VCC.
∗, 式 (2.4)

x.inf, x.sup, y.inf, y.sup ∈ F∗と追加することでできる (結論は P と省略している) .

H0 : x.inf ∈ F ∨ x.inf = −∞H1 : x.sup ∈ F ∨ x.sup = +∞7. 1 二つの戦略

H2 : y.inf ∈ F ∨ y.inf = −∞この節では補助定理を追加する二つの戦略を提案

H3 : y.sup ∈ F ∨ y.sup = +∞する. 補助定理は仕様に WhyML コマンド assert で追H4 : x.inf ≤ x.sup

H5 : y.inf ≤ y.sup

加できる. 補助定理を追加することにより, 証明の一

H6 : 0 ≤ x.inf

H7 : x.sup , 0

部が後回しにされ, 現在の証明プロセスが単純化され

H8 : 0 ≤ y.inf

H9 : y.sup , 0

ることがある. assert コマンドを追加すると, Why3

r.inf, r.sup ∈ F∗

はコマンドに対する追加の VC を生成し, 自動または

H10 : r.inf = ▽(x.inf · y.inf)

対話証明器のどちらかで証明する必要がある.

H11 : r.sup = △(x.sup · y.sup)

7. 1. 1 戦略 1: 浮動小数点数定理の実数定理による

H12 : r.inf ∈ F ∨ r.inf = −∞言い直し

H13 : r.sup ∈ F ∨ r.sup = +∞我々は 5 節 で証明した実数区間版の定理を補助定

H14 : r.inf ≤ r.sup

理として与えることを検討した. 実験では, • ∈ {I, C}

xx, yy ∈ R

H15 : x.inf ≤ xx ≤ x.sup

H16 : y.inf ≤ y.supr.inf ≤ xx · yy ≤ r.sup
図4としたとき, 丸め区間演算プログラムから生成された.

VCCの Coq のコンテキスト.
∗, 式 (2.4)

VC•⊙, B を証明する効果的な戦略は, 補助定理∀x ∈ IR, ∀y ∈ IR, VCC⊙, B
を 追 加 す る こ と だ と 分 かった. 例 え ば, 6. 2 節 の
I
VC∗,
と VCC
式 (2.4)∗, 式 (2.4)

を証明するために, 5. 2 節

ローチの鍵は SMT ソルバー, 特に Alt-Ergo の自動証で証明した ∀x ∈ IR, ∀y ∈ IR, VCC

明プロセスを, 多くの前提から可能な限り推論できることで Alt-Ergo の証明プロセスを助けることができ,よう誘導することである. これは前提 VC I⊙, B または
VCC⊙, B のどちらかに補助定理 L を証明できるようになる. 最終的に, 図 2 の 32 行目に以B(x, y) ⇒ L(x, y) ⇒ P∗, 式 (2.4)

を前提とする下の assert コマンドを追加した:
assert { forall xinf xsup yinf ysup : real.
xinf >= 0. -> xsup <> 0. ->yinf >= 0. -> ysup <> 0. ->forall xx yy : real.
xinf <= xx <= xsup ->yinf <= yy <= ysup ->xinf*yinf <= xx*yy <= xsup*ysup };

1
2
3
4
5
6

実験では, この戦略により Alt-Ergo は 6. 2 節 で説明した未証明の VC の証明を補助することを確認した †14.

78
9

7. 1. 2 戦略 2: 区間の境界による定理分割10

本実験では, VC を証明するためにさらなる補助定理を追加する必要があった. もう一つの補助定理は,

11
12
13

assert を用いて VC を上限と下限に定理を分割することである. 下限の補助定理は以下のようになる:

ただし f ⊙, B (x, y) は演算結果の下限を表す. 例えばf∗, 式 (2.4) (x, y) = ▽(x y) である.
∗, 式 (2.4)

1516∀ x̃ ∈ x, ∀ ỹ ∈ y, x̃ ⊙ ỹ ≥ f ⊙, B (x, y)

VCC

14

を証明するために, 一つ目の戦略による補助定理に加えて,

let multiply (x y: interval) : interval(* 事後条件は省略 *)= if not ge_zero x.inf &&not le_zero x.sup thenif not ge_zero y.inf &&not le_zero y.sup thenlet inf1 = mul_down x.inf y.sup in
let inf2 = mul_down x.sup y.inf in
let sup1 = mul_up x.inf y.inf in
let sup2 = mul_up x.sup y.sup in
if lt inf1 inf2 &&gt sup1 sup2 then(* 補助定理をここに追加する *){ inf = inf1; sup = sup1 }else(* 省略 *)

図5

浮動小数点数区間に対する multiply の別の分岐.

る. 二つ目は, 11–12 行目の if 文から与えられる条件▽(x · y) < ▽(x · y) ∧ △(x · y) > △(x · y)

以降, 条件 式 (7.1) ∧ 式 (7.2) は B ′ と省略する. つぎIに, この分岐のための VC∗,
B′ は以下である:

B ′ (x, y) ⇒ [▽(x · y), △(x · y)] ∈ IFと, 上限の補助定理をプログラムに挿入する必要があ
る. Alt-Ergo はこれらの assert を 3.1 秒と 9.7 秒で証明し, 最終的に VCC∗, 式 (2.4)

を 16.5 秒で証明する.

(7.3)

さらに結論を分解したものを以下に示す:

B ′ (x, y) ⇒▽ (x · y) ∈ IF∪{−∞} ∧ △(x · y) ∈ IF∪{+∞} ∧▽ (x · y) ≤ △(x · y)

(7.4)

また, VCC∗, B′ を以下に示す:′

7. 2 もう一つの戦略
今までに導入した二つの戦略で, 四則演算の目標
コードの 4 個以外の分岐の VC は証明できる. 二つの戦略でも証明できない場合に, 証明を補助するもう一つの戦略がある.

B (x, y) ⇒ ∀ x̃ ∈ x, ∀ ỹ ∈ y, ▽ (x·y) ≤ x̃ ỹ ≤ △(x·y) (7.5)
VC を証明するために, 一つ目の戦略に従って以下の補助定理を 13 行目に assert する:∀x ∈ IR, ∀y ∈ IR,′

この節では multiply の別の分岐を考える. 図 5 は未証明の 4 個の分岐のうちの一つのみを記述するよう, コードを修正している. この分岐の条件は二段階からなる. 一つ目 (3–6 行目) は, 未証明の 4 個の分岐に共通する条件

x<0<x ∧ y<0<y(7.2)

で, 境界の演算の四つの場合の一つを指定している.

assert { forall rinf : double.
rinf = mul_down x.inf y.inf ->forall xx yy : real.
_in xx x -> _in yy y ->double_le_real rinf (xx*yy) };(7.1)

であり, これは引数の区間が 0 を含むことを述べてい†14 この補助定理は, 6. 2 節 同様に Coq で証明できる.

B (x, y) ⇒ ∀ x̃ ∈ x, ∀ ỹ ∈ y, x y ≤ x̃ ỹ ≤ x y
これは Coq により証明できる. この補助定理により
I
VC∗,
B′ は Alt-Ergo により 91 秒で証明できる. しかし

VCC∗, B′ は 300 秒でも証明できない.
図 5 の目標のプログラムの検証を達成するために,

7–10 行目で導入されている中間変数に着目する. VC
はこれらの変数を用いて書き換えられる. 例えば,VC (7.5) は以下のように書き換えられる:示的に述べ, 結びつける役割をする.

(式 (7.1)) ⇒ ∀inf1 ∈ IF, ∀sup1 ∈ IF,

8 実験結果∀inf2 ∈ IF, ∀sup2 ∈ IF,
inf1 = ▽(x · y) ⇒ inf2 = ▽(x · y) ⇒6 節 から 7 節 で述べた浮動小数点数の区間演算プ

sup1 = △(x · y) ⇒ sup2 = △(x · y) ⇒ログラムの検証結果を表 2 に示す. それぞれのカラム

inf1 < inf2 ∧ sup1 > sup2 ⇒∀ x̃ ∈ x, ∀ ỹ ∈ y, inf1 ≤ x̃ ỹ ≤ sup1

は以下である:

(7.6)

– 演算子

この変形をより一般化した形式で述べ, 三つ目の戦略– Why3 が生成した VC (および補助定理) の数を導入する.

– SMT ソルバー (Alt-Ergo) で証明した VC の数

7. 2. 1 戦略 3: 中間変数による補助定理– 対話証明器 (Coq) で証明した VC の数

あ る 実 装 f ⊙, B (x, y) が あ る と き, 合 成 関 数– Alt-Ergo による自動証明と, Coq による型検査に

h ⊙, B (g ⊙, B (x, y)) に分解することができる. ただしかかった実行時間 (秒)g ⊙, B : IF2 → IFn かつ h ⊙, B : IFn → IF である. した

本実験は RAM 16 GB を持つ 2.4-GHz Intel Core i5

がって VC は合成式と (ベクトル値の) 中間変数で書プロセッサで行った. また検証には Why3 (バージョき直すことができる. 例えば VCC⊙, B はン 0.87.3) 上で Alt-Ergo (バージョン 1.30) と Z3 (バーB(x, y) ⇒n∀v ∈ IF , v = g ⊙, B (x, y) ⇒ L(x, y, v) ⇒ジョン 4.5.0), 定理証明支援系 Coq (バージョン 8.6) を用いて行い, 実行メモリは 2.5 GB に設定した.

∀ x̃ ∈ x, ∀ ỹ ∈ y, h ⊙, B (v)と書き直せる. ここで L は引数と中間変数の論理式で9 関連研究ある. 三つ目の戦略は上の形式の VC に補助定理 L と

9. 1 区間演算プログラムの検証

して追加する.

Ayad ら [1] による区間演算プログラムの検証事例が式 (7.6) の条件 inf1 < inf2 ∧ sup1 > sup2 は検証ある. Ayad らは Why3 と同様な検証プラットフォームを単純化する補助定理の例である. 実験ではいくつか

Frama-C 上で, バックエンド証明器に SMT ソルバーの補助定理 L を追加することにより VCC∗, B′ を証明でと Coq を用い, 本研究とは若干異なる実装の IF 四則

きた. 例えば inf1 について, 以下を追加した:演算コードの検証に成功している.

inf1 , NaN

上記のコードの乗算部分を Why3 に書き換え, 検証

inf1 ∈ F ⇒ x ∈ F ∧ y

実験を行ったところ, 同様にすべての VC を証明でき

inf1 ∈ F ⇒ inf1 ≤ x y

ることが確認できた.

inf1 ∈ F ⇒ ∀ x̃ ∈ x, ∀ ỹ ∈ y, inf1 ≤ x̃ ỹ

Ayad らと我々のコードを比較してみたところ, (1)∀ x̃ ∈ x, ∀ ỹ ∈ y, inf1 ≤ x̃ ỹ

Ayad らも本研究で提案する戦略 1 のように, 式 (5.2)

この補助定理は Alt-Ergo によりそれぞれ 1.5 秒, 4.8に相当する定理を追加し証明の補助をしているが, 戦

秒, 32 秒, 200 秒, 13.7 秒で証明できた. 同様にして

略 2–3 の補助を必要としていない, (2) Ayad らのコー

sup1 についての補助定理を追加し, Alt-Ergo によりそ

ドはいくつかの場合を考慮しておらず限定的である,

れぞれ 1.5 秒, 8.9 秒, 14.1 秒, 216 秒, 6.0 秒で証明でことが分かった.

CI
きた. 最終的に VC∗,
B′ と VC∗, B′ は Alt-Ergo によりそれぞれ 14.6 秒と 0.1 秒で証明できた.
中間変数の導入は実装関数 f ⊙, B を二段階に分解す

そのため, 別の区間演算プログラムや応用プログラ
ムについて, 自動証明がうまくいかなかった場合に,我々の提案する三戦略の効果が期待される.

ることによって VC を単純化する. しかし, この分解は分岐の条件と結果の条件の間の推論を困難にする.

9. 2 CRlibm

追加した補助定理は, 引数と中間変数の間の関係を明

一般の浮動小数点数を用いた数値計算プログラム

表2

浮動小数点数境界の区間演算プログラムの検証結果

演算

VC (内, 補助定理)

Alt-Ergo (1.30)

Coq (8.6)

CPU 時間

加算

2 (0)

2

0

11.37s

減算

2 (0)

2

0

13.29s

乗算

102 (72)86

16

947.29s

除算

37 (21)29

8104.47sの証明が多数報告されている.

本研究により, 高信頼な数値計算ライブラリに対して,CRlibm [6] は効率的かつ丸めの正しさが証明されそれ自体の信頼性も高めることが可能になった. また,た数学ライブラリであり, C の標準数学ライブラリ

自動証明では全ての検証条件ができない他のプログ

libm の置き換えを目的としたものである. CRlibm でラム検証にも, 本研究で提案した三戦略による検証技の正しさの証明は, 自動定理証明器 Gappa などを用い法を適用することが期待される.

て区間解析により数値誤差を求め証明している.

今後の課題としては, 証明した WhyML から実行コー

CRlibm と本研究の違いは 3 つある: (1) CRlibm はドへの変換, 同様のアプローチによる区間演算の初等演算結果が指定した丸め方向の最も近い値であるか

関数や応用プログラムの検証, 提案した三戦略の適用どうかを証明しているが, 本研究の軽量かつ半自動的の自動化がある.

な証明とは違い, 複雑な証明からなる, (2) CRlibm は
主に初等関数の丸めの正しさの証明であり, 本研究と謝辞 本研究の一部は科研費 15K15968 の補助を得て行った.

は異なる性質を証明している. 本研究のアプローチを
初等関数の実装コードの検証に応用することも期待

参考文献

出来る, (3) CRlibm は C で実装してありそのまま実行[1] A. Ayad and C. Marché: Multi-Prover Verification of
Floating-Point Programs, IJCAR, LNAI 6173, pp. 127–141,
2010.
[2] F. Bobot, J.-C. Filliâtre, C. Marché, and A. Paskevich.: Why3: Shepherd your herd of provers, International
Workshop on Intermediate Verification Languages (Boogie),
pp. 53–64, 2011.
[3] S. Boldo and G. Melquiond.: Flocq: A Unified Libraryfor Proving Floating-point Algorithms in Coq, E. Antelo,
D. Hough, and P. Ienne.: IEEE Symposium on Computer
Arithmetic, pp. 243–252, 2011.
[4] S. Boldo, F. Clément, J.-C. Filliâtre, M. Mayero, G.
Melquiond, and P. Weis.: Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program,
Journal of Automated Reasoning, 50(4):423–456, 2013.
[5] S. Conchon, M. Iguernlala, K. Ji, G. Melquiond, andC. Fumex.: A Three-Tier Strategy for Reasoning About
Floating-Point Numbers in SMT, CAV, LNCS 10427, pp.
419–435, 2017.
[6] C. Daramy-Loirat, D. Defour, F. de Dinechin, M. Gallet,
N. Gast, C. Q. Lauter, and J.-M. Muller.: CR-LIBM - A
library of correctly rounded elementary functions in doubleprecision, Version 1.0 beta 5, 2016.
[7] Moore, R.E., 1966. Interval Analysis, Prentice-Hall.
[8] 梅村晃広: SMT ソルバ・SMT ソルバの技術と応用, コ
ンピュータソフトウェア, 2010, 27 (3):24–35.

可能であるが, 本研究の検証コードはそのまま実行できない. ただし Why3 の extract 機能を用いれば実行可能コードへの変換は可能である.

9. 3 自動証明器の浮動小数点数理論のサポート
最近, SMT ソルバーにおける浮動小数点数理論のサポートの開発が進んでいる. Conchon ら [5] は, 実数理論に基づいた浮動小数点数に関する公理系を用意し,浮動小数点数理論に基づく述語論理式を扱う手法を提案している. その求解処理では, 戦略の一つとして非線形実数算術の求解系を呼び出して利用している.
同様の仕組みにより, 本研究の戦略も自動化することが考えられる.

10 まとめと今後の課題
自動的・対話的な定理証明器を用いた, 区間演算ライブラリの検証事例の提案手法と実験結果を示した.