そのプログラム、正しく書けている?「形式検証」入門:第三回 SPARK
形式検証に関連するコラム「形式検証」入門の第三回を掲載いたします。
今回の内容は、弊社が代理店をしているAdaCoreのパートナー企業であるニルソフトウェアの代表者、伊藤様に作成いただきました。
第三回 SPARK
今回は,SPARKについて,説明したいと思います.SPARKは,Ada言語(第一回)のサブセットであり,形式検証(第二回)をサポートしている言語です.
■歴史
Ada は人の名前に由来していました.では,SPARK はどこから来たのでしょうか.昔,SPADE(Southampton Program Analysis Development Environment)というPascal言語のサブセットがありました(ちなみに,Pascalも人の名前です.さまざまな功績を残しています.最初の機械式計算機と云われる Pascaline[注1] の発明者でもあり,パンセという有名な本を残しています).この SPADE を拡張するときにベースの言語をPascalからAdaに変更しました.できあがったのが,SPADE Ada Kernel で,略して,SPARK になりました[注2].略語ですので,人名のAdaとは異なり,全て大文字になります(’R’は,たぶん発音しやすいように追加されたのではと思います).
*注1: https://www.britannica.com/technology/Pascaline
*注2:SPARKも長い歴史を持ち,0.1版は,1999年に発行されています.http://docs.adacore.com/sparkdocs-docs/SPARK_LRM.htm
SPADEは,Pascalで書かれたプログラム解析が目的でした.SPARKも同様です.解析のために幾つかの注記を追加しています.一つ例を見てみます.但し,これは最新のSPARK 2014の記法ではなく,その前の SPARK 2005 の記述法に基づいています.
図 1 SPARK 2005 での記述
これを現在のSPARKの書き方にすると,次になります.
図 2 SPARK 2014 での記述
手続き Add は,in out モードの大域変数を利用していることを示しています(2行目). オブジェクト Total は,自分自身とXに依存し(3行目),Grand_Totalは,自分自身とXに依存していることを示しています.先の図1も書き方は異なっていますが,同じ内容を示しています.図2にある’+’ の記号は自分自身を含むことを示しています.
注目すべきは,図1の古い書き方は,”–“ で始まっていることです.Ada言語では行コメントを示します.ツールを使えば,解釈しますが,Adaコンパイルに通した場合,この記述は除かれることになります.最終的なコードには影響を及ぼしません.一方で,現在のSPARKは,Adaのアスペクト(Aspects)[注]の記法を利用しつつ,新たなキーワードを持っています.
SPARK 2014 では,コメントの範疇から,より独立した言語に近づいたと考えることもできます.主たる役割は,自分自身が正しいプログラムであることを検査し,確認することだと云えます.
*注: Ada 2012 で導入された新しい記法.その名の通り,キーワードが示す側面(aspect)から見たときに,真といえることを記載します.
図 3 Ada と SPARK の関係を示すベン図
Adaから見ると,SPARK は Ada のサブセットになります.例えば,以下に示す構文は,SPARKでは除かれています(図3 における[A]の領域です).
- アクセス型と割当て演算子
- 副作用のある式(関数呼び出しを含む)[注1]
- 別名化[注2]
- goto 文
- 被制御型(controlled types)
- 例外処理(例外送出文を用いることはできます.例外送出が実行されないことを証明しようとします)
これらは,あいまいさを含んでいる(副作用のある式,別名化など),或いは,検証を困難にする要素になります(アクセス型など.ちなみに,アクセス型は,C言語でいうポインタに類似しています).
逆に,SPARKで拡張している部分もあります.前述のように,大域変数やデータフローの依存関係を示すために利用するキーワード, Global やDepends です.アスペクトという枠組はAdaと共通です.しかし,これらキーワードは,SPARK特有です(図3における[C]領域).
*注1:例えば,次のような in out モードを持つオブジェクト(一般の変数のことをAdaではオブジェクトという)をパラメータにとる関数を利用したときに副作用に関する問題が発生します.
function F (X : in out Integer) return Integer;
*注2:二つの名前が同一のオブジェクトを指している場合です.
- 静的検証
静的検証とは,プログラムを動作させることなく,実装が仕様に合致していることを示す行為を指します.テストは,実際に動かして確認するので,動的検証になります.
SPARKの静的検証には2種類あります.一つが,入出力するデータの依存性に関わる検査です.これまでのGlobalやDependsによって規定されたアスペクトを確認します.フロー分析と呼びます.もう一つが,今回のテーマである形式検証になります.今回はフロー分析については,詳細を省略しています.
- 形式検証
SPARKの形式検証の目的は,実行時エラーがないこと,機能が正しいこと,を示すことにあります.
- 実行時エラーがないこと
SPARKが見つけることの出来る実行時エラーは,次のようなものです.
- 配列範囲外アクセス
- 副型の範囲違反
- 計算時のオーバーフロー
- ゼロ割
副型の範囲違反は,制約記述が可能なAda言語で可能となる静的に検出可能なエラーです.
検証とは,満足すべき条件を記述した上で,その条件を実際に満足していることを示すことでした.実行時エラーに関しては,明示的に条件を書く必要がありません(常に起こって欲しくないことだからです).SPARKの証明器であるGNATprove が,これら実行時エラーのために,自動的に検証条件を生成します(なお,検証条件については,「第二回 形式検証とは」を参照下さい.前回は,VCと書いていますが,同じです).逆に言えば,全ての実行時エラーが見つかると主張しているわけではありません.あくまで,前述の実行時エラーに限定されます.
- 機能が正しいこと
「契約による設計(Design by Contract, DbC)」により示します.その契約内容は,表明と呼ばれる事前条件・事後条件などで示します.即ち,中心的なアイデアは,「呼び出し側が約束(事前条件)を守ってくれれば,結果を出す(事後条件)」ということです.このことによって,機能が正しいことを示せると考えます.
即ち,ある副プログラムがあり,示されている表明(事前・事後条件)をプログラムが満足しているとき,そのプログラムは「機能的に正しい」と考えます.
次からは,この表明の書き方について,説明します.
- 表明の記述
代表的な表明である事前条件と事後条件には,複数の書き方が存在します.これら条件が複雑になったとき,書き方を選択することで,見通しを良くすることができます.
図 4 事前条件サンプル
Preで始まる行が,事前条件を示しています(2行目).ここでは,プログラムが単純過ぎるため,事後条件は省略しています.
この手続き Increment は,単純です.オブジェクトXを受け取って,1増加させてから新しいオブジェクトXを出力します.
しかし,Xが整数型の最大値の場合,1を加えることはできません.従って,この手続きを実行するためには,Xは,整数型の最大値より1だけ小さい必要があります.
ここでの事前条件は,そのことを示しています(整数型なので,最大値Integer’Lastより小さい最大の値は,Integer’Last – 1です).
ツールは,5行目にあるように,オーバーフローがないことを出力します.ここでは,便宜上プログラム中に記述していますが,実際は,コンソールやレポートに出力します.
図5 事後条件サンプル(同一関数の2つの書き方)
図5では,2種類の事後条件の書き方を示しています.
最初の事後条件(3行目)が示しているのは,次のことです.関数 find は実行後,ゼロあるいは,配列Aのいずれかの値を返すということです.見つからなかった時は,ゼロで,見つかった時は,その位置を返すと推測できます(Adaではデフォルトで,配列添字は1から始まります).
2番目の例では,明確に事後条件を定義しています.
いま,配列A中の全ての要素が,検索対象自然数Eと一致しないとき,ゼロを返す(9行目).それ以外では,配列Aの添字範囲内にある位置を返す(10行目).先の例では,推測として書いたことが,2番目の例では明確に事後条件として表現されています.
検証対象として望ましい記述は,2番目ということなります.ちなみに,さきの「全ての要素が」)という書き方は,述語論理における全称限量子を用いた書き方になります.このように,述語論理を用いた記述が可能です.
- 契約ケース(Contract Cases)
複雑な事前条件・事後条件の組を記載したいときの書き方に,契約ケースという書き方があります.
Contract_Cases というアスペクト名を使用します.
図6 契約ケースサンプル
図6では,閾値(オブジェクトThreshold)との大小関係で,入力に対して出力すべき値を規定しています.図5の条件文で記載するときに比べ,より見やすい記述が可能になります.
- ゴーストコード
SPARKには,「ゴースト(ghost)」という概念があり,検証すべき内容を記述するときに,利用することができます.検証のために仕様部で用います.
実際のプログラムには影響を与えず,かつ,コンパイル時に最終的なコードから取り除くこともできます.いろいろ役に立つが,最終コードには残らないということで,この名前が付いているのだろうと思います.ゴーストは,あらゆるエンティティ(オブジェクト,型,サブプログラム,パッケージなど)に対して注釈をつけることが可能になります.
図7 ゴースト定数サンプル
3行目で,ゴースト定数 X_Init を定義しています.”with Ghost” がアスペクトの指定です.6行目の表明文[注]において,Do_Some_Complex_Stuff手続き実行後に,Xの値が,ゴースト定数 X_Init と等しいかをチェックしています.
8行目では,このゴースト定数を,オブジェクトXに代入しています.この文はエラーとなります.あくまでゴーストですから,実行文に用いることはできません.9行目,10行目と同等のエラーメッセージが,コンソール或いはレポートに出力されます.
*注:ここでの表明,Assert文は,一般的なAssert文と同様です.「契約による設計」用というわけではなく,値の確認用に用います.
ゴーストコードを使用できるのは,仕様部に限定されることに注意して下さい.
図8 ゴースト式関数サンプル
ここでは,ゴースト式関数Get_Modelを宣言しています(2行目).式関数というのは, 実装部が単一の式である関数です.実装を含んでいますが,仕様部で用いることができます.
手続き Push において,事前条件では,スタックSの長さが,Max より小さいことを条件としています(5行目).事後条件は,手続き Push が,要素Eをスタックに加えることで,新しいスタックを得ることができるとしています(6行目).ゴースト関数は,前回のゴースト定数と同様に,表明の記述中でのみ用いることができます.
関数 Peek では,I番目の要素の値を返すために,このゴースト関数を用いています(7行目〜8行目).これはエラーとなります.実行文においては,「ゴースト」は用いることができないためです.
この例では,なぜ直接スタックSを扱わずに,ゴースト関数を用意しているのでしょうか.それは,スタックSが非公開(private)型だからです.スタックSの構造の詳細にアクセスすることができません.
ゴースト関数は,このようにやむを得ない場合,或いは,表明を簡潔にするために,用いることができます.
- ループ不変条件
代表的な表明として,これまで示したものに加え,ループ不変条件があります.ループ不変条件は,(1)ループの初回と,(2)各ループで不変条件が成立し続けるかを検査します.場合によって,初回は成立しないが,初回以降に成立する場合,或いは逆のケースも存在します.
図 9 ループ不変条件サンプル
9行目がループ不変条件と呼ばれるものです.この行がない場合,事後条件を正しく判定することができません(5行目).Xの値が更新されており,証明器はどの値に変わったことを,チェックしようとしないからです.ループ不変条件を記載して,初めて,一回のループで,Xの値が1増加することが分かるため,事後条件が正しく判定できるようになります.
■練習
これまでの復習として,2つほど,練習問題を解いてみます.
- 問題1
図 10 問題1
このプログラムでは,2つの整数型のオブジェクト X, Y を交換します.事後条件はどのように書くことができるでしょうか.
事後条件とは,この手続きが実行されたあと,成立して欲しい条件ですから,以下になります.
XとYには,それぞれ手続きに入る前のYとXの値が設定されます.
- 問題2
次は,ループ不変条件を扱います.
図11 問題2
このプログラムは,配列型A_TのオブジェクトAに関して,全ての要素がゼロであることを確認する手続きになります.事後条件にもあるように,配列要素が全てゼロであれば,ブーリアン型オブジェクト Success には,True がセットされます.
一つでも,ゼロ以外の要素が見つかれば,そこで終了して,Successには,Falseがセットされます.
このプログラムのループ不変条件とは何になるでしょうか.ループ不変条件とは,各ループの間に成立しているべき状態になります.
いま,J(番目)まで確認が取れているとします.正しくチェックができていれば,J番目まで全ての要素はゼロのハズです.ここでは,述語論理の全称限量子(for all)を用いて,全てがゼロであると定義しています.プログラムのように見えますが,あくまで,ルール中で変わって欲しくない状態を示しています.
■まとめ
形式検証のためのいろいろな表現がでてきました.使い分けについては,次のように整理ができるかも知れません.
(1) 必要な範囲を持つデータ型を使う
Ada言語は強い型付けの言語という説明を初回にしています.値制約を付けて,副型を宣言することで,使用予定のない値をとったときに,検出することが可能です.これは,表明の記述を必要としません.
(2) 事前条件・事後条件を副プログラム記述の仕様段階で考える
Ada言語は,明確に仕様部とボディ部(実装)を分離する構造を持っています.これは,プログラマが積極的に分離することを意図しています.従って,プログラムが書き終わったあとで,表明を改めて記述するのではなく,どういう副プログラムを作ろうかと仕様を決めた段階で,考えるべきです.表明もまた,仕様の一部です.
もし,記述が複雑になる場合は,契約ケースやゴーストを利用することを考えます.
(3) ループ不変条件は,ループとともに,考える
ループは,便利な記述ですが,間違える危険性も多い場所です.ループ不変条件を考えることで,より安全なループの記述が可能となります.
SPARKは,形式検証における段階的な移行を支援しています.必要に応じて,表明を記述することで,形式検証の適用範囲は広がります.
また,形式検証の実行に当たって,必要なのは,検証レベルを設定すること位です.
もちろん,全てを形式検証できるわけではありません.しかし,形式検証を実施したモジュールでは,テスト工数を減らした上で,より信頼できるプログラムを得ることができるようになります.
(NIL 伊藤昌夫)