形式的仕様記述の適用事例を通して得た仕様記述のコツ

これはFormal Method Advent Calendar 2016の25日目の記事です。

今年6月、国立情報学研究所で「恊働ロボットCOROの開発における形式的仕様の適用事例」というタイトルで形式手法の適用事例について発表しました。資料はこちらです。

http://www.slideshare.net/liferobotics/coro-63631016/1

開発対象となるシステムの仕様を形式的に記述するということは自分にとっても初の挑戦であったので、実際に適用してわかったことがたくさんありました。発表資料でのいくつか書いていますが、本記事では仕様の書き方で自分が発見したことに焦点をあてて説明します。

不変条件はなるべく明記した方がよい

発表資料でも触れていますが、仕様を理解する上で不変条件はとても重要な役割を果たします。今回、自分たちが採用した仕様は状態遷移モデルをもとにしているため、振る舞いはイベントに対する遷移として記述します。状態遷移モデルに変数を導入することで、変数がないプリミティブなモデルから見たら複数ある遷移をひとつの遷移として書くことができます。しかし、その場合各変数が遷移後にどのような状態になっているかを明記しなければなりません。これを事後条件で記述します。たとえば、
あるボタンが押されたら、別のボタンがDisableになって操作不能になるとしましょう。このとき、ボタンのEnable/Disable状態を表す変数をブール型の変数で表すとすると、遷移の事後条件には以下のような記述が必要です。

button_enabled' = False;

ここで、button_enabled がブール型の変数で、Falseは偽を表すブール型の値です。button_enabled' のように変数に ' がついている場合は事後の変数を表します。=は等号であり、代入演算子ではありません。この場合は、事前の状態に関係になく False になりますが、一般的には事後条件は事前の状態との関係で表されます。たとえば、ボタンのEnable/Disableが切り替わるような操作があった場合は以下のように書きます。

button_enabled' = not button_enabled;

ここで、not はブールの否定演算子です。このように変数を導入することで本来は各変数がとりうる値ごとに状態として記述する必要があるものが、変数を含むより大きな状態に着目して仕様を記述することができます。自分たちの場合は、GUIアプリケーションの画面を大きな状態として捉えて、その画面内の振る舞いを記述するのに変数をつかって記述しました。

さて、このように各遷移を書いていくと、どの遷移の事後条件でも成り立つものを見つけることができます。それをもっとよく考えてみると実は大きな状態にいる間（自分たちの例では画面）ずっと成り立つ条件を見つけることができます。それが（その状態での）不変条件です。不変条件はその名の通り変わらない条件で、さまざまなものを対象にすることができます。たとえば、システムが動いている間すべての状態（自分たちの例でいうとすべての画面）で成り立つ不変条件はシステムの不変条件です。また、不変条件はなにも仕様だけの話ではなく、プログラムのループが実行している間成り立つ条件もありこれをループの不変条件と呼びます。われわれがつくるシステム（プログラム）は動くことに価値があるのですが、不変条件はその中で変わらない条件を表します。ちょっと不思議ですが、この不変条件が仕様の理解にとっても役に立つのです。

というのは、実はさきほど述べた各遷移をよく見て不変条件を見つけるというのは稀で、むしろ各遷移で成り立つルールがあってそれに違反しないように各遷移の事後条件を書くことの方が多いからです。で、このルールが不変条件そのものです。仕様を決めるときに、各遷移の詳細を決める前に方針のようなものを決めることがあります。たとえば、ロボットが動いている時はボタンをDisableにして操作不能にしよう、とかです。こういう方針を不変条件で書いておくことは非常に大切です。なぜなら、不変条件を書かないとロボットを動かし始める遷移の事後条件をすべて見てどういう条件が成り立つか発見しないといけないからです。仕様を理解する上で最初に合意されるこういった方針やルールは非常に役に立つものです。これを不変条件として表します。

robot_state = State_Moving => button_enabled = False;

この不変条件が陽に記述されないと、どういうルールがあるのか読み解くのに苦労します。

共通の振る舞いは一箇所で記述が済むように何らかの支援があると良い（だろう）

もうひとつは、これだ！とまだ解が出たわけではないのですが、書くうえで非常に苦労したことから得たことです。上で述べたように今回各画面を大きな状態として捉えて遷移を記述しました。しかし中には全画面で共通の振る舞いというものがあります。今回は、これを何も工夫せず各画面で書くようにしました。しかし、これはあまり良い選択ではありませんでした。

一つ目の理由は、単純に記述がめんどくさいということです。共通のものは一箇所の記述で済ませたいというのがプログラマの心理としては当然です。修正するときの手間はエディタの機能で頑張ってもらうとしても面倒なことはかわりません。

二つ目の理由は読む方も大変だということです。各画面にちらばって書いてあると不変条件と同じように全部を見ないと共通だと言えないので、本当に同じ振る舞いか？というのを確認するのが大変になります。ここでも例をあげて説明しましょう。たとえば、どの画面にいてもあるHWボタンを押したらロボットが停止する、というような仕様を書くとしましょう。このとき、全画面で以下のような事後条件をもつ遷移を記述しないといけません。

robot_state' = State_Stop;

しかし、画面がいくつもある場合、全画面のそのイベントの遷移を見て、すべてが上記の記述ならば確かにいつでも停止状態にするということがわかります。もし、ひとつの画面でも

robot_state' = robot_state;

というように、ロボットの状態が変わらないと書いてあった場合は、その画面だけは異なる振る舞いになります。これが意図したものなのか、実は記述ミスなのかは補足がないと確信がもてないでしょう。

最初に仕様記述の文法を考えたときに一つ目の理由は頭にはありましたが（逆に二番目は気づいてなかった）、それでも各画面で書くように決めた理由はあります。それは、あまり仕様に構造を持ち込みたくないと考えていたからです。各状態で書くものを一箇所の記述にすむようにするということは、それが各画面で書いたものと等価である記法を考えないといけません。オブジェクト指向でいうところの継承のようなモデルを採用する案は頭にはありましたが、あまり複雑にして記法に溺れても、と思い、まずはフラットに書こうと決めました。しかし、結果的にはあまり良い選択ではなかったようです。ただ、支援なしではどういうところが大変かというがわかったという意味では良かったと思います。

以上、今回は実践から得たふたつのことを書きました。ほかにもいくつかあるのですが、長くなったので今日はこのへんで。もしかしたら、来年のJaSST Tokyo 2017での発表でもう少し詳しくお話しできるかもしれません。興味がある方はぜひご参加ください。

http://jasst.jp/symposium/jasst17tokyo/details.html#D3

では、メリークリスマス