プログラミングからはじめる形式仕様
今回は、VDM-SLという形式仕様言語を紹介します。
形式仕様というと、数学が基礎になっているとか、証明が難しそうとかいうイメージを持っている人をよく見かけます。でも実際には、それは使い方次第です。
VDM-SLには以下の二つの顔があります。
- 数学から入る、形式手法のための言語
- プログラミング言語から入る、プロトタイプおよび参照実装のための言語
この記事では、後者の、プログラミング言語から入るVDM-SLを紹介します。
例題：カウンター
カチカチとボタンを押すたびに数字が1ずつ足されていく、ただし9999までいったらカンストしてそれ以上は増えないようなカウンターを、VDM-SLで書いてみます。まずはVDM-SLを使った例をざっくり眺めてみてください。
module Counter
exports all
definitions
values
max_count : nat = 9999
state Count of
count : nat
init s == s = mk_Count(0)
end
operations
inc : () ==> nat
inc() == (if count < max_count then count := count + 1; return count);
reset : () ==> ()
reset() == count := 0
end Counter
このソースではCounterモジュールを定義しています。
Counterモジュール内では、定数max_countと変数count、さらに2つの手続き (VDM-SLでは操作と呼びます)が定義されています。
max_countはカンストの値、つまり9999です。
countが現在のカウンターの値を保持しています。
incは、カンストしていなければカウンターを1増やします。返り値は、最終的なカウンターの値を返します。
resetは単純にカウンターを0に戻します。
プロトタイピングとしてのVDM-SL
え、それのどこが形式仕様なの？どこが数学なの？普通にプログラムじゃん？と思ったあなた、正解です。上述の記述は、あくまでプロトタイプ実装としてのカウンターです。これを実際に書いて動かしてみることで、次に実装としてどんな内部状態を持ち、どんなAPIを提供するプログラムを書く必要があるのかを確認することができます。例えば、カンスト値は設定可能なのか、それともハードコードしてしまって良いのかを、実際に動かしてみることで確認します。一方で、実行効率は考えません。あくまでどのような動作が期待されているのかを確認するためのプロトタイプです。
カウンターの例はとても単純なので、普通に実装用のプログラミング現後でも十分にプロトタイピングすることができるでしょう。これがもっと複雑になった時、まずは実行効率を度外視してプロトタイピングすることに集中できる言語として、VDM-SLを使う効果が発揮されます。
参照実装としてのVDM-SL
プロトタイプを作成して、本番用の実装を書く時、どの部分が「決められたこと」で、どの部分が「今回たまたまこういう実装をした」ものなのか、混乱してしまうことがあります。プロトタイプ時には実行効率は度外視して書いたために、本番用の実装では改めるべき部分というのもあるでしょう。つまり、プロトタイプには以下の2種類の記述がごちゃ混ぜになっています。
- こういう動作をすべきだという「決まった部分」
- プロトタイプではこういう処理にしたけど、本番実装ではその言語に合った書き方をしたい「仮の部分」
本番実装のためには、上記2種類の記述を区別した上で動作するような参照実装が役に立ちます。
VDM-SLでは、守るべき規範をアサーション（表明）として記述します。
そう、ユニットテストで書く、あのアサーションです。
前述のカウンターにアサーションを加えると、以下のようになります。
module Counter
exports all
definitions
values
max_count : nat = 9999
state Count of
count : nat
inv mk_Count(c) == c <= max_count -- 状態に対するアサーション
init s == s = mk_Count(0)
end
operations
inc : () ==> nat
inc() == (if count < max_count then count := count + 1; return count)
post
(count = count~ + 1 or (count~ = max_count and count = max_count))
and RESULT = count; -- inc操作に対するアサーション
reset : () ==> ()
reset() == count := 0
post count = 0; -- reset操作に対するアサーション
end Counter
アサーションとして加えた部分に、-- で始まるコメントを付けました。
状態に対するアサーションでは、変数countが常に守るべき規範を記述しています。
つまり、カウンターが内部に保持するカウンター値は常に9999以下でなければならないことを示しています。
inc操作に対するアサーションでは、inc操作が変数countに対して最終的にどう変化させるかを記述しています。アサーション内では、count変数について、inc操作を実行する直前の値をcount~、直後の値をcountとして参照しています。規範として、「カウンターの値(count)は、元の値(count~)に1を加えたものか、あるいは、元の値がカンストしていて新しい値もカンストしているかの、どちらか」と定義しています。この規範さえ守れば、どのような処理過程を経ていても、どのようなアルゴリズムでも構いません。例えば、以下のような定義でも規範を守ることができます。
inc() == if count = max_count then return max_count else (count := count + 1; return count)
reset操作に対するアサーションも同様に、この規範さえ守れば実際の処理は変更して構いません。実際にはcount := 0以外にあまり良い方法は思いつきませんが。
プログラマの、プログラマによる、プログラマのためのVDM-SL
カウンターをわざわざVDM-SLで記述してからプログラミング言語で再実装することに意味はあるでしょうか？カウンターの例は簡単なのであまりありがたみは感じないと思います。プロトタイピング言語あるいは参照実装言語としてのVDM-SLの特徴として、高機能な言語機能はあまりなく、とても基本的な構文要素しか持ちません。例えば制御構造は、cases文、for文、while文などです。型クラスや型推論のような高度な型機能も持ちません。とても基本的で素直な、手続き型言語です。つまり、まっすぐ、単純に記述をします。そこに、アサーションとして規範を加える事で、参照実装として実装者に伝えるべきことを伝えることができます。
言ってみれば、VDM-SLはいわゆる上流技術者向けではありません。むしろ、プログラマの、プログラマによる、プログラマのための仕様を、プログラマの道具とプログラマの流儀で記述するための言語です。VDM-SLはプログラムとして実行することができます。プログラムとして実行することができるのだから、プログラムとして書くこともできます。ならば、プログラマにとって友達のはずです。
VDM-SLは友達、怖くないよ！