「正しさ保証済みプログラムの生成」
ここまで「網羅的テストが可能な擬似コード」と「プログラムの強力検査器」の2つの技術を紹介しました。いずれも検査のためのものでした。つまり、設計や実装がある正しさの基準（要求仕様や、実行エラーが起きないことなど）を満たすかどうかを調べる技術でした。
しかし、検査というのは実は後手に回ったアプローチともいえます。究極的には、プログラムの作り方を突き詰めて、プログラムができあがった時点で「適切に作ったので正しい」と断言できればよいのです。例えばそのように作った部品については、単体テストはスキップできることになるでしょう（ある程度の動作確認はするはずですが）。
この「正しさ保証済みプログラムの生成」という話は突拍子もなく聞こえるかもしれませんが、ソフトウェア開発の一つのあるべき姿として追求されており、確立された技術が活用されています。スタート地点としては前述の「チェック付き仕様記述」になります。厳密で機械処理可能な仕様記述を構築し、その検証（不整合がないことの検査）や妥当性確認（要求に合うことの確認）をまずはしっかり行います。つまり、粛々と実装すればよい状況にします。
ここで、この「チェック付き仕様記述」を少し実装に近づけるよう書き換えます。例えば「実行後には、条件を満たすデータの集合が抜き出されている」という記述を、データに対するループ実行において、要素を一つずつ調べて条件に合致するものを記録していくようなアルゴリズムに書き換えます。そして、この書き換えが、前の記述とズレていないことを理論的に保証するような「証明」を行います。これにより、仕様からズレることなく実装に一歩近づくことができます。
このステップを繰り返すことで、仕様を満たし、かつプログラムコードを得るのに十分な詳細情報を持った記述を得ることができます。あとはC言語など、必要なプログラミング言語のコードに翻訳するだけです。
別のやり方と比べてみます。当然ながら、人間が仕様記述を基にプログラムを構築した場合、いろいろな誤りが混入する可能性があります。しかし、仕様記述とプログラムのギャップが大きいので、プログラムが仕様を満たしていることを理論的に保証することは難しくなってしまいます。あるいは、仕様記述からプログラムを生成するようなコード生成器を作ることを考えます。この際、このコード生成器の作り方によっては、仕様を満たすプログラムを得られることが保証できるかもしれません。しかし上述の通り、やはり仕様記述とプログラムのギャップは大きいので、そのようなコード生成器を作るのは不可能ではなくとも難しくなります。加えて、プログラムの設計をすべてコード生成器に委ねてしまうので、実行速度やメモリ使用量などさまざまな点で不満足なプログラムコードになってしまうこともよくあるでしょう。
これらを踏まえ、「正しさ保証済みプログラムの生成」では、より小さなステップで段階的に、設計指針を反映しつつプログラムコードに近づけていき、各ステップでは理論上の保証をしっかり与えられるようにするのです。
【事例】公共交通の自動運転制御での実績
パリの地下鉄や空港シャトルにおける、自動運転制御等の核となるコードは、「正しさ保証済みプログラムの生成」により構築されたことで有名です。この「正しさ保証済みプログラムの生成」を用いた開発は、ニューヨークなど世界何十カ国にもおける鉄道関連のシステムにも使われています。「正しさ保証済みプログラムの生成」による開発プロセスは、従来のものと工数のかけ方が大きく変わります。具体的には最初の部分、厳密で機械処理可能な仕様記述を構築し、その妥当性確認を行う部分に大きな工数をかけます。あとは粛々と正しい実装を行い、単体テストは念のため実施する程度の感覚になります。フロントローディングといった言葉もありますが、つまり、上流の本来重要なこと（システムが行うことを厳密に定義すること）に工数が移っていることになります。
【専門用語での補足】定理証明を用いて仕様記述からコードへ
「正しさ保証済みプログラムの生成」という考え方は、英語の「Correctness-by-Construction」という言葉に基づいたものです。直訳すると、「構築により正しさを得る」といった感じでしょうか。
また、ある程度小さなステップを繰り返して仕様記述からプログラムコードを得るプロセスは、段階的詳細化と呼ばれます。「単体テストは念のため実施する程度で構わない」といえるための肝になるのは「仕様からズレないこと」といった理論的な保証になります。これは、定理証明という手段で行われます。中学以降の数学で扱うような証明のことです。つまり、与えられた定理などを用いて、論理的な一定の手順だけを用いて、結論（正しさの保証）を導くということです。定理証明はもちろんツールにより支援されており、人による誤りが入らないようにします。現在のツールは非常に進化しており、多くの場合に自動で証明手順を探し出すことができます。パリにおける空港シャトルの事例では、97％の証明が人手による補助なく完了したと報告されています。
さらに広がる論理のチカラ
ここまで見てきたように、形式手法と呼ぶことができる技術は多様です。なぜならば、裏に数学（特に数理論理学）があることだけが共通点だからです。プログラムが持つチカラの中には、論理に基づいた判断や制御のチカラ、そして自動化のチカラがあります。それらのチカラをさらに強化して強力な検査を実現したり、仕様や設計の時点でもそれらのチカラを活かしたりするのが形式手法のアプローチです。
もちろん、ICTのシステムは論理的なことだけ考えればよいわけではありません。変化が激しく不確かな実世界と向き合い、正解がないことがらに対してさまざまなステークホルダーと「満足」や「納得」を追求していくといったことがますます重要になっています。だからこそ、論理のチカラで解決できる部分や、より品質を高められる部分について、エンジニアがあいまいな日本語に悩んだり、大量の人手で挑んだり、経験だけで何となくの品質保証を行ったりするのはもったいないと思います。
本記事で紹介したのはある意味古典的で、一般的なアプローチです。形式手法と呼べるようなアプローチとして、新しい取り組みもどんどん出てきています。昨今流行している人工知能を考えてみると、例えば以下の関連技術も形式手法の一環だといえます。
- 実行時の環境変化を踏まえて設計を自動的に行う技術（制御器合成）は、形式手法の重要な領域であり、特に近年盛んに研究が行われています。
- 自動運転において、人工知能に一定範囲内での自由な意思決定を任せても安全なように、その範囲を実行時に随時（厳密な保証付きで）決めていくような手法もあります。
- ディープラーニングによる画像認識において、ある程度画像をひねったりずらしたりしても誤認識が起きないことを網羅的に検査するようなツールも出てきています。
これは一緒に議論した人からの受け売りですが、形式手法を学び、さまざまな技術との対比や協働について議論をしていくと、要求分析やテスティング、ステークホルダーとのコミュニケーション、エンジニアのスキルなど、さまざまな話題がつながっていきます。形式手法は決して、エンジニアの皆さんの日常から離れた特別な世界での話ではありません。もちろん形式手法に限らず、どんな技術であれ組織的に導入する際には大きな困難があります。しかし、本記事で興味を持った技術があれば少し検索してみる、ツールを使ってみるなど、ぜひ形式手法の面白い世界に一歩踏み出してみてください。
トップエスイーについて
「トップエスイー」は、国立情報学研究所で提供している、社会人エンジニア向けのソフトウェア工学に関する教育プログラムです。トップエスイーでは講義や制作課題を通して、最先端の研究成果や現場で得られた知見が蓄積されてきました。その「アウトカム」、つまり成果やそこに至る過程を紹介し、現場のエンジニアの方々に活用していただける記事を連載しています。トップエスイーでは、形式仕様記述に関わる講義が充実しています。集合論や論理学といった数学を学習する講義、VDMやBメソッドなどの具体的な記述方法の講義、さらには実践的な内容の講義などが開講され、形式仕様記述を習得して現場で応用する能力の獲得をサポートしています。
