関数プログラミングと形式手法の振り返り

本日で春先から受講していたJAISTの授業I217関数プログラミングを終えました。

経緯としてはSET(Software Engineer in Test)界隈で形式手法が取り上げられることがあり、自分の業務守備範囲からそう遠くない領域だったため興味を持ち受講しました。今回学ぶことが多かったので内容と所感をまとめたいと思います。

※ この記事はあくまでも自分の解釈と所感であり、私は形式手法の専門家ではないので詳しい話は参考に記載したリンクを参照ください。

関数プログラミング
CafeOBJ
形式手法
所感
参考

関数プログラミング

今回受講したJAISTの緒方教授の講義。緒方研究室[1]は形式手法に取り組んでいる関係上、講義では最終的に形式手法の触りまで学んだ。形式手法には代数仕様言語CafeOBJを用いますが、授業で触った限りだと副作用を持つような記述はできず、純粋関数型言語のパラダイムに属する印象を持った。

CafeOBJ

Common Lispで書かれた代数仕様言語。Java等のオブジェクト指向言語がソフトウェアを創るためのものであるとすると、CafeOBJは仕様を検証するためのものと捉えられると思う。講義では以下のような代数の基礎的概念を利用した。

ソート

一般的なプログラミング言語における型に似た概念。以下のようにソートに包括関係を持たせて宣言することが可能であり数理論理学でいう集合論的な概念を表現できる点が特徴かなと思う。

[ NzNat < Nat ]

この場合はNzNatはNatに含まれるとなり、非ゼロの自然数が自然数に含まれるという包括関係を表す。

オペレータ

代数学でいうところの演算子を表す。例えば加算であれば以下のように定義する。

op _+_ : Nat Nat -> Nat

ただし演算子といっても算数で扱う加減乗除のようなものに限らず、プログラミング的には入力に対して出力が一意に定まる関数と捉えたほうが適切かもしれない。

変数・等式

変数は一般的なプログラミング言語ではデータの読み書きを行う記憶領域のことだが、代数仕様言語の文脈ではあるソートの集合そのものと捉えられる。等式 eq を用いて自然数の仕様を以下のように表すとわかりやすい。

var M : Nat .
eq 0 + M = M .

数学における方程式と同義であり0 + x = xと考えるとわかりやすい。

形式手法

形式仕様記述言語を用いてソフトウェアの仕様を記述し数理や代数によりそれを検証する手法のこと。形式手法のアプローチには2つあるようで[2]、講義では証明譜(proof score)という定理証明に近い手法を学んだ。

一例として講義で取り扱った階乗を求めるfactorialの検証を示す。

再帰による階乗計算fact1と末尾再帰による階乗計算fact2を定義し、一方を仕様もう一方を実装としたときにfact1=fact2となれば仕様通りに実装されているとみなせるとのこと。PNatはペアノの公理[3]を満たす0を含む自然数。

mod! PNAT1 {
  [PNat]
  op 0 : -> PNat {constr} .
  op s : PNat -> PNat {constr} .
  vars X Y Z : PNat .

  eq (0 = s(Y)) = false .
  eq (s(X) = s(Y)) = (X = Y) .

  -- 
  op _+_ : PNat PNat -> PNat .
  eq 0 + Y = Y .
  eq s(X) + Y = s(X + Y) .

  op _*_ : PNat PNat -> PNat .
  eq 0 * Y = 0 .
  eq s(X) * Y = (X * Y) + Y .

  op fact1 : PNat -> PNat .
  eq fact1(0) = s(0) . -- f1-1
  eq fact1(s(X)) = s(X) * fact1(X) . -- f1-2

  op fact2 : PNat -> PNat .
  op sfact2 : PNat PNat -> PNat .
  eq fact2(X) = sfact2(X,s(0)) . -- f2
  eq sfact2(0,Y) = Y . -- sf2-1
  eq sfact2(s(X),Y) = sfact2(X,s(X) * Y) . -- sf2
}

検証自体は数学的帰納法により行い、本来は定理証明に必要な補題(Lemma)も都度証明する。手順の概要は以下の通り。

自然数0で実装が仕様を満たす red fact1(0) = fact2(0) .
任意の自然数xの場合に実装が仕様を満たすことを仮定する eq fact1(x) = fact2(x) .
x+1=>s(x)の場合に実装が仕様を満たすことを示す red fact1(s(x)) = fact2(s(x)) .

open PNat1 .
  op x : -> PNat .
  -- lemma
  eq Y * sfact2(X,Z) = sfact2(X,Y * Z) 
  -- induction hypothesis
  eq fact1(x) = fact2(x) .
  -- check
  red fact1(0) = fact2(0) .
  red fact1(s(x)) = fact2(s(x)) .
close

所感

業務への適用可能性

形式手法の導入事例[4]から見てわかるように形式手法そのものは大規模で安全性が求められるシステムに適用される事例が多いようだった。実際にプラント、発電所、機械、鉄道、医療機器、家電などを対象とした安全規格であるIEC 61508ではformal methodがhighly recommendedとなっている。[5]

元々はプロダクションコードのテストを行う要領で形式手法を導入することができると考えていたが、むしろ開発者がコーディングを行う前段階で仕様の漏れや不備を発見したりアルゴリズムの妥当性を検証するための技術と見たほうが正しいと感じた。仕様の漏れによる手戻りがクリティカルな問題になりやすいウォーターフォールの上流で効果を発揮すると思う。

自分が身を置いているようなアジャイル開発を基本とするIT業界において形式手法そのものを導入することはしばらくなさそうだなという印象だった。