コラム

Column

ご挨拶

そのプログラム、正しく書けている?「形式検証」入門:第一回

AdaCore コラム

これから数回にわたり形式検証に関連するコラムを連載で掲載します。
今回は、弊社が代理店をしているAdaCoreのパートナー企業であるニルソフトウェアの代表者、伊藤様に作成いただきました。

第一回 なぜAda言語か

「形式検証(formal verification)」とはなんでしょうか.最初の「形式」は何らかの数学的モデルに基づいていることを表しています.「検証」は,元になる仕様があり,実現(例えばプログラム)が,仕様に適合しているかを確認することを指します.「形式」と「検証」の両者を合わせると,“数学的なモデルを用いて,作られたプログラムが,仕様と合っているかを確認する”という意味になります.検証における代表的なテストは,形式検証には含まれません.

もちろん,全てのプログラムが,形式検証できるわけではありません.数学的に書けない仕様があります(例えば,ユーザインターフェイスの使い勝手が典型的です).しかし,一部でも形式検証できるならば,意味があります.労働集約的なテストに対して,多少ともテストの割合を減らすことができれば,実務的には,きわめて有効な方法です.かつ,形式検証した箇所では,テストケースのモレということを心配する必要がありません.

さて,「仕様が正しく書ければ」というのがポイントになります.正しく書くのは難しく,解こうとする問題毎に,用いる数学的モデルが適している場所があります.

今回ご紹介するのは,最も一般的な方法で,かつ記述しやすい方法です.Ada言語由来のSPARK言語と,ツールを用いる方法になります.

第一回目は,Ada言語をご紹介します[注].次の順番で説明を予定しています.

 (1)なぜAda言語か(今回)
 (2)形式検証の世界
 (3)SPARKの紹介

なお,短いスペースで,Ada言語を紹介することはできず,今回は,学ぼうとするときに知っておいた方が良い点を中心に,説明します.
*注: Ada言語に馴染みのない方が多いと想像しています.ただ,類似のものをご存じかもしれません.ハードウェア記述言語であるVHDLは,Ada言語をベースとしています.いま,自動車技術会で進められているモデルベース開発では,VHDL-AMS[1]を利用しています.米国では,アーキテクチャ記述言語として,やはりAda言語由来のAADLの仕様化が行われています.
また,商用データベースに用いられているPL/SQLは,Adaを利用した開発プロジェクトへ参加した経験から,作られたと云われています.

Ada言語の歴史

簡単にAda言語の歴史を振り返ります.

プログラム言語の開発では,個人がアイデアをもとに開始する場合もあれば,言語を必要とする組織が始める場合もあります.Ada 言語は後者です.従って,組織が始めた場合に生じがちな特性があります(例えば,言語仕様が大きい).

スタートは,米国の国防総省が,搭載用のプログラム言語を統一化したいという望みから始まっています.フランスのチームが応募し(採用され),幾つかドラフトが作られました.最終のドラフトは鉄の人(Steelman)[2]と呼ばれ,今でも読めます.

1983年に,仕様が定まり(MIL規格およびANSI規格),Adaという名前を与えられます.Adaは,最初のプログラマと云われている Ada Lovelace (1815-52) に因んで名付けられました.詩人であり作家(「海賊」は素晴らしい)のバイロン卿の一人娘です. Ada 関連のサイトには,必ずといって良いほど彼女の肖像があります.本人にはまったく想像できなかったことでしょう.

1987年にISO規格となり,1995年に最初の改訂が行われます.その後,2005年・2012年にも改訂が行われ,Ada 2012[3] と呼ばれるものが最新になります.

歴史を振り返った時に,2つの注目すべき点があります.

一つ目は,どの環境でも同じ動作をすることを目指していたということです.そのため,タスク機構といった本来はOS側で用意される機能も言語レベルで定義されています.また,以前には,ACVC (Ada Compiler Validation Capability) という検定制度がありました.環境とコンパイラのセットに対して,検定を行います.そのテストに通って,初めて Ada コンパイラと名乗ることができました.これも,常に同じふるまいを保証したいということから来ています.

Ada は,単なるプログラミング言語以上のことを目指したと,というのが2点目です.

高い信頼性を持つソフトウェアを作るためには,プログラム以前に,仕様や設計をきちんと記述する必要があるというのは,一般的な理解と思います.Ada の仕様策定でも意識されていました.例えば,基本要素であるパッケージでは,仕様部とボディ部が分離しています.ボディ部の作成に先立ち,仕様部を作成し評価することになります.その上で,実装段階において,ボディ部を作ります.仕様部との整合性を機械的にコンパイラが確認する.即ち,仕様部には,単にパッケージを説明する以上の役割を与えられています.

また,APSE (Ada Programming Support Environment) [4] があります.APSE は,その名が示したとおり,当時目指していた Ada のプログラム開発環境です.現在でも,開発支援環境は,大きなテーマの一つですが,当時としては珍しかったと思います.Ada に対して,形式検証機能をツールとして自然な形で利用できる SPARK は,その伝統の中で生まれていると思います.

Ada言語の最初の一歩

ここでは,Ada言語を初めて学ぶときに,知っていると良いことを幾つか記載しておきます.Ada言語のほんの一部ですが,最初に知っておくと良いことを選んでみました.

なお,これから,学習を進めるために良いページがあります.日本Ada協会のコミュニティサイト(https://ada.jp/)を見て下さい.次のページ(https://ada.jp/?page_id=12)は,学習するときに役立つリンクを示しています.最初にある学習プラットフォームは,WEB上だけで,学習が可能です.また実装系は,非商用向けに,FLOSS(Free/Libre and Open Source Software)として提供されています(AdaCore社の次のページです.https://www.adacore.com/community).

特徴1. 強い型付けの言語です

型付けというコトバは,聞き慣れないでしょうし,他の言語では余り用いられません.変数が取り得る値を,型として規定するという意味になります.

ここで,Initial が変数です.Character は文字を表す基本型です.ここでは,範囲制約が付くことにより,Character range ‘A’ .. ‘C’ で副型(subtype)を構成します.

繰り返しこの副型を使用する場合,明示的に宣言することができます.これが,先の「変数の取り得る値を型として規定する」ということになります.

これにより,変数宣言[注]は,次のように書くことができます.
*注:正確には,オブジェクト宣言といいます.オブジェクトというとき,変数と定数の両方を指します.古い教科書で,オブジェクトに算体という訳語を与えられているときがあります.

いま,変数Initial に,文字’D’ を代入しようとすると,副型が保証している範囲制約を越えることになり,コンパイルエラーが出ます.

型付けにより,変数の取り得る値に制約を加えることができ,共通のものについては,「型」とすることができます.誤って,異なる型同士の演算が書かれていれば,静的にコンパイラが見つけます.常に型を意識してプログラミングする必要がある言語というのが,「強い型付け」言語の特徴になります.

2. 構造:パッケージが基本単位です

次に,Adaでプログラムを作成するときの,基本的な構造について説明します.

基本単位は,「パッケージ(Package)」になります.パッケージは,(パッケージの)仕様部とボディ部に分かれます.副プログラムには,手続き(procedure)と関数(function)の2種類があります.仕様部では,そのパッケージで用いる型や,副プログラムを宣言します.ボディ部では,副プログラムの実体を定義します(図1参照).

*図 1 仕様部とボディ部からなるパッケージの構造(手続きは,パッケージを利用します.このとき,パッケージ内には,手続きや関数などの副プログラムが通常含まれます.)

例を見てみます.いま,パッケージ Buffer を考えます.この Buffer の仕様部では,バッファーに値を設定する Load 手続きを考えます.

引数内にあるin 或いは out は,引数モードを示す標識です.B は手続きの出力(out)で,S は,入力(in)になります.他には,in out モードがあります.値が更新される入力変数ということを示します(この情報は,SPARKにおけるフロー解析で利用します).

次に,型 Buffer をレコード型(他言語では,構造体と呼ばれることがあります)として宣言します.レコード型の要素として格納用の文字列(Data),開始番号(Start)と終了番号(Finish)を持っています.

ボディ部では,この手続きを実装します.

入力された文字列の最初の位置を1に(ちなみに,Adaでは配列添字のデフォルト値は1になります),最後の位置(Finish)を,その長さに設定します.Dataは,配列で,入力された文字列を格納します.

いま,仕様において,Dataは,80文字としていました(レコード型の定義を見て下さい).もし,それよりも長い文字列が来ると困りますので,事前条件として定義してみます.

ここで,pre で始まる部分が,事前条件の定義になります.入力文字列の長さはMAX(80)を越えない.これは,Loadを呼び出す側の責務になります.仕様部にあるこの事前条件に,手続きを呼び出す人は従わなければなりません.利用する上での,いわば「契約」になります.実際に,MAX を越える文字列を入力してみると,SYSTEM.ASSERTIONS.ASSERT_FAILURE例外が送出されます.

同じコードをSPARKとみなせば[注],実行時エラーではなく,検証時に,「precondition might fail (事前条件が,成立しない可能性がある)と出力されます.つまり,実際にプログラムを動かすことなく,事前条件が成立しない可能性があることを教えてくれます.これが,形式検証になります.
*注:Adaコードを変更する必要はありません.SPARKとして,証明器にかければ良いだけです.

ここに重要なことがあります.事前条件を記述することで,この検査ができます.何もかかないで,間違いを見つけてくれるわけではありません[注].何が正しいかを示さない限り,間違っているとは誰にも云えません.
*注:ゼロ割の可能性検出は別です.常に,ゼロ割りは誤りなので,記述することなく検査します.この他にも敢えて表明を書かなくとも検査される項目があります.

この事前条件記述は,契約型プログラムにおいて表明(Assertion)と呼ばれます.表明には他に,事後条件があります.SPARKでは,更に,ループ不変条件や述語論理に基づく記述が可能です.これらは,何が正しいかを,我々が示すための道具立てになります.

形式検証には,後に説明するSPARKの処理系と検証器が必要です.しかし,SPARKはAda言語のサブセットであり(逆ではありません),まずは今回ご紹介したAdaで,何が成立していれば良いかを,示すよう習慣づけることが重要になります.

最後に

今回の記事のために,Adaの仕様策定に携わったB. Brosgol博士(AdaCore社)から,みなさまへのAda言語の紹介を頂きました.

Ada is a modern programming language that is especially suitable for applications demanding reliability, safety, and/or security.  Sound software engineering principles form the basis for the language’s design, as illustrated in Ada’s support for object-oriented programming, generic templates, an expressive and efficient concurrency model that is well suited for real-time embedded systems, and contract-based programming features that make explicit a code module’s assumptions and guarantees. These benefits, coupled with the language’s extensive compile-time and run-time checks, make Ada an ideal choice for both new programmers and experienced software professionals. With Ada, you develop good habits from the start.

[Ada言語は,近代的プログラム言語の一つです.特に,信頼性・安全性・セキュリティが求められるアプリケーションに適しています.確固としたソフトウェア工学の原則があります.オブジェクト指向プログラム,汎用(体)テンプレート,(リアルタイム組み込みシステムに適合した)表現力豊かで,効率の良い並列モデル.そして,コードモジュールの仮定・保証を明示的に表現する契約型プログラムです.こういったメリットと,広範囲に渡るコンパイル時や実行時の検査と相まって,Ada言語は,プログラマになろうとする人や経験豊かなプログラマにとって,理想的な選択となります.Ada言語によって,学習の最初から,(プログラミングにおける)良い習慣を身につけることができるようになります.]

この文章には,Ada言語の全てがコンパクトに示されています.今回は,Ada言語を学び始めるための導入的なご紹介です.昔とは違って,オンラインで学習する手段はたくさんあります.日本Ada協会の先に紹介したページをぜひのぞいて学んでみて下さい.

次回は,形式検証についてもう少し詳細に,ご説明したいと思います.

(NIL 伊藤昌夫)

[1] 国際標準記述によるモデル開発・流通検討委員会編著,「自動車システムのモデルベース開発」,自動車技術会,2017.
[2] http://www.adahome.com/History/Steelman/intro.htm
[3] John Barnes. Programming in Ada 2012. Cambridge University Press, New York, NY, USA, 2014.(Adaに関する教科書です.900ページを越えています.)
[4] P. A. Oberndorf, “The Common Ada Programming Support Environment (APSE) Interface Set (CAIS)” in IEEE Transactions on Software Engineering, vol. 14, no. 6, pp. 742-748, June 1988.

メールマガジン

「ご登録いただいた内容は、弊社の掲げる「個人情報保護方針」に沿って管理し、本件に関するお問い合わせ、お申込み等いただいた内容への対応のために利用する場合がございます。なお、お客様の同意なく目的外の利用や第三者への開示、提供を行うことはございません。」

CONTACT

まずはお気軽に
お問い合わせください!

PAGE TOP