SPARK言語

現在の SPARK 2014 は，Ada言語のサブセットです．しかし，別の言語として考えることが望ましそうです¹．それは，プログラムの正しさを示す言語として，捉えるべきと云うことになります．

プログラムの正しさを示そうとするとき，テストに全面的に頼ることはできません．全ての入力ベクトルを網羅することはできず，テストで正しさを示すことはできません²．従って，一般には，データの組み合わせ・制御フロー・データフローを用いて，代表値で網羅することを考えます．「テストは網羅だ」というのは，テスト技法の著者 B. Beizer の有名な格言ですが，代表値の網羅で全てが解決するわけではありません．

一方で，証明によって，正しさを示すというアプローチがあります．SPARKが目指している方向になります．

もちろん，証明を行うためには，何を証明して欲しいかを明確に記述する必要があります．それなしに，機械が証明すべきことを類推することはできません³．

ここでは，新しい SPARK の本⁴ から，典型的な例を示します．

pragma Spark_Mode (On);
package Sorters is
  type Array_Type is array ( Positive range <> ) of Integer;
  function Perm (A: in Array_Type,
                 B: in Array_Type) return Boolean
  with Global -> null,
       Ghost => True,
       Import => True;
  procedure Selection_Sort (Values : in out Array_Type)
    with Depends => (Values => Values),
         Pre     => Values'Length >= 1 and then
                    Values'Last   <= Positive'Last,
         Post    => (for all J in Values'First .. Values'Last - 1 =>
                    Values (J) <= Values (J + 1)) and then
                    Perm (Values'Old, Values);
end Sortes;  

上記は，パッケージ Sorters の仕様部です．このパッケージでは，Array_Type と関数 Perm および Selection_Sort 手続きを宣言しています．

最初に，pragma で，この仕様部が SPARK 言語であることを宣言しています．以下は，SPARK 特有の表現です．

関数 Perm の with 節にある Global は，引数以外で，外部からふるまいに影響を与える変数の有無を記述する箇所です．ここでは，null ですから，そのような変数は存在しないと云うことを宣言しています．次の Ghost は，証明の助けとなる一時的な存在（それが Ghost という名前の由来です）であることを示しています．Ghost 関数の実体は，もちろん与える必要があります．次の，Import は更に興味深い宣言になっています．この関数の実体は，SPARKでは与えず，この証明に関してより適した表現形式を利用するということを宣言しています．

次の手続き Selection_Sort は，もう少し一般的な SPARK 記述です．with節の最初の Depends は，変数の依存関係を示しています．Values は，in out モードですから，自分自身に依存していることになります．ここでは，余りに単純な例なので，記述の重複のようにも見えますが，そうでない場合も多く，証明のために記述は常に必要です．次の pre および post は，表明（assertion）としてよく知られた記述です．それぞれ，事前条件と事後条件を示しています．述語論理で記述ができ，事後条件には，全称限量子（for all）を用いています．

これらの記述は，証明器（prover）によって証明されます．証明器自身は，もちろん，SPARK の範囲外ですが，現在は Community 版においても，SMT（Satisfiable Modulo Theories）ソルバーの Alt-Ergo/CVC4/Z3が，同梱されています．

さて，全てが証明できるわけではないことに注意が必要です．証明不能の問題がありますし，複雑な算術演算は扱えません（基本的には線形に限られます）．したがって，実務的にはテストと併用ということになります．

それでもなお，証明を行うことはきわめて有効な手段です．テストというのは，時間も手間も大幅に必要とします．一部でも証明が可能であれば，全体の時間や手間を大幅に減らすことができるからです．

個人的には証明を意識してプログラムを作ると云うことが，何にもまして有効である気がします．

(NIL)