ディペンダブル・システムのための形式手法の実践ポータル

このページでは，形式手法の基本的な考え方を説明します．形式手法と分類される様々な手法に共通する考え方として，数理論理学等に基づき，システムの注目する側面を正確に，曖昧さのない形で表現します．これによりシステムへに関する理解を明確にするとともに，システムの満たす性質について科学的・系統的な分析や検証をツールを用いて行います．

形式手法が効くところ

ソフトウェア開発の過程においては，システムや個々のコンポーネント，メソッド等が「何を（どれだけうまく）すべきか」，そしてそれらが「求められているものをどうやって実現するのか」を議論し定めていきます．開発の初期過程では要求仕様という形で前者の「何をするのか」といったことを主に議論し，徐々に「どう実現するのか」を具体化・詳細化していき，最終的なプログラムを得ることとなります．

「何をすべきか」や「どう実現するのか」という情報は，開発の様々な段階（要求，仕様，設計，実装）で様々な抽象度で現れます．ここで，どの種類の情報であれ，

（問題①）開発者が明確に，曖昧さのない形で理解・共有することが重要です．逆に言うと，日本語や明確な意味が定まっていない図による仕様や設計の表現では，誤解や思い込みが発生，後に発覚し，修正・手戻りのコストが大きくなるという問題が典型的です．

（問題②）「正しさ」をできるだけ保証することが重要です．逆に言うと，設計や実装において検出，修正されずに残っていた「誤り」が原因で，アップデートや製品回収，ビジネスへの支障といった大きなコストが発生するという問題が典型的です．

形式手法という言葉は総称であり実際には様々な手法がありますが，共通する原則として「理論に基づいた形できちんと書く（そしてきちんと検証・分析する）」ことにより，これらの問題に対応することを考えています．

なお，問題②に関し，「正しさ」は与えられた基準に対して相対的に決まるものです．ここでの基準としては，「デッドロックしない」のような基本的な性質の他，「変数xの値は常に正である」「踏切が開いている状態で電車が通過することは決してない」といったアプリケーションごとに定まる性質が考えられます．

きちんと書くとは？ ～プログラムは動かすためにきちんと書いている～

上の「問題①」で述べたように，日本語や明確な意味が定まっていない図による表現だけでは，曖昧さが残ってしまいます．もう少し正確には，曖昧さを取り除く努力はできますが，人によるところがありますし，「よし」と言える明確な基準がありません．プログラムのように，

明確な文法と意味論が決まっている言語で記述すれば，人によって解釈が異なることもなく，曖昧さがない形で書いているかチェックすることもできるようになります．（問題①への対応）

なお，プログラミング言語そのものは実際にシステムを動かすために都合のよい書き方を考えているので，もっと抽象的な仕様や設計を記述するには向いていません．

また「問題②」に関しては，日本語や明確な意味が定まっていない図による表現だけでは，ツールにとって「文字列」「座標を含むオブジェクト」でしかないため，文字列や図の編集はできても，「正しさの分析・検証」のようなことはできません．プログラムは明確な文法と意味論が決まっている言語で書かれており，コンピュータはそれに従い動作することができます．同じように，

明確な文法と意味論が決まっている言語で仕様や，設計とその満たすべき性質などを記述すれば，コンピュータはそれに従い分析や検証を行う（支援する）ことができます．（問題②への対応）

なお，プログラミング言語そのものは実際にシステムを動かすために都合のよい書き方を考えているので，仕様や設計を扱うには向いていませんし，複雑なので網羅的な分析や検証には工夫が必要です．ただしプログラムは今でも「きちんと書いている」ものなので，プログラムを対象とした形式検証手法もあります．

このように，どちらの問題においても，形式手法における「「形式（フォーマル・formal）」という部分が効いてきます．また，実際のシステムそのものというよりは，抽象化され不要な詳細を省いた「モデル」の記述や分析・検証を考えています．モデルという概念については以降の解説において改めて述べます．

ここまでの説明を図にしてみると以下のようになります．

数理論理学・・・？

上では「きちんと（書く，分析・検証する）」と書いて形式手法の目指すところを説明しました．この「きちんと」は，具体的には「数理論理学に基づき」ということになります．「数理論理学」というと難しそうですが，実際にはどのようなものか見てみましょう．

ここでは例として，システムの満たすべき性質をきちんと書いてみることを考えてみます．

（例１）「リクエストを送ると，いつか必ず応答が返ってくる」「踏切が閉じていない状態で電車が通過することはない」
これらの性質は，実行の経過に関する条件を表しています．
例えばSPINというツールでは，この前者の性質は下記のように記述できます（LTLという言語）．
     [] (req => <> res)
（どんな状態においても（ [] ），その状態でリクエストが発生している（req）ならば，以後いつか（ <> ）応答が発生している（res）状態に到達する）

（例２）「メソッドsortの引数は空ではない整数型のリストであり，戻り値は入力のリストを小さい順に並び変えたものである」
この性質は，ソートを行うメソッドがどのような状況下で呼ばれるべきで，その実行の結果何が起こるべきかを表しています．
例えばVDMという手法では，この性質の後半部分は下記のように記述できます（VDM-SLやVDM++という言語）．
     forall i, j in set inds list1 & i < j => list1(i) <= list1(j)
（list1 のインデックスの集合からどの２つを抜き出して i ， j としても（forall ... & ... ）， i が j より小さいならば i 番目の要素は j 番目の要素以下である）

これらの例は，システムの満たすべき性質を「明確な文法と意味論が定められた言語」で書いたものです．これの例においては，「集合に含まれている」「・・・ならば＊＊＊」「どの要素であっても・・・」といった記述が用いられています．数理論理学は，このような記述やその意味論を体系化したものです．「aが集合Sに含まれている（a∈S）」「AならばB（A⇒B）」「どんなxに対しても（∀x）」については，高校数学や大学の計算機科学の授業（集合論，命題論理，一階述語論理）で学んだことがある人も多いのではないでしょうか．「どんな状態でも」や「いつか到達する」の方は，実行の経過に関する検証で用いられる時相論理に含まれているもので，あまりなじみがないかもしれません．

上の例では「数理論理学に基づいて記述」しています．これは開発者の仕事になります．もう１つの側面として，「数理論理学に基づいて分析・検証」することも非常に重要です．上で書いたような性質を何となく検証したのでは「誤りの検出漏れ」という問題が解決されないので，科学的に・系統的に，できれば「与えられた範囲を網羅」して検証する必要があります．また，その際には効率化のため，「これは調べればあっちもわかる，だからあっちは調べなくてよい」といったことを（もちろん理論的に）考える必要があります．そういったことを理論に基づき考えるのは誰かというと，基本的には「分析・検証ツールを作る人」になります．ただし一般の開発者としても，ツールの中で起きていることを少し理解すればより分析・検証の意味・意義が明確になりますし，またツールのオプション設定等をより使いこなすことができるでしょう．

このページの先頭へ戻る