警告ゼロと、正しいプログラムの間

架空事例：青葉機材の予約数量を検査する。コードと数値は説明用に作成した。数式では数学的整数を用い、実際の言語の桁あふれ、共有状態、入力型とは区別する。Frama-C、Clang、PITを本事例へ実行したという報告ではない。

誤った料金を、正確に計算する

コンパイルは通った。静的解析の警告もなかった。予約の計算処理は、指定された数量に単価を掛け、金額を返した。

それでも請求は誤っていた。使っていたのは、契約成立時の単価ではなく、現在の商品マスタの単価だった。

型が正しいことと、業務上選ぶべき値を選んでいることは違う。どちらの単価も整数で、どちらを掛けてもプログラムは動く。警告が出ないという観測から、仕様に書いていない業務上の正しさまで導くことはできない。

原教材第12章の静的解析と形式的な条件は、検査ツールの名前を覚える話だけではない。何を入力し、どの性質を調べ、何が分かったと主張するかを区別する話である。1

実行せずに分かることは、文字の形だけではない

静的解析を、字下げや未使用変数の確認だけだと考えると、その範囲を狭く捉えすぎる。コードの経路や値の関係を追うことで、特定の経路でだけ起こる問題を見つける解析もある。

例えば、在庫情報の取得に失敗すると値が得られないのに、その後の処理が必ず数量を参照するなら、成功時しか試さない実行テストが見逃す経路を静的に調べられる可能性がある。一方、どの経路を、どの精度で扱うかは解析方法に依存する。

Clang Static Analyzerの公式説明は、解析量の上限を設けていること、誤検知があり得ること、検出対象として実装された種類の欠陥を探すことを明示している。2 そこで警告がないという結果を得ても、あらゆる業務上の誤りがないという証明にはならない。

逆に、「静的解析は何も証明できない」と言い切るのも誤りである。欠陥を探すツールの結果と、特定の性質について証明義務を立てる形式的な検証を、ひとまとめにしない。

関数へ渡す前に、何を約束するか

保有数量をC、既に確保した数量をR、新たな依頼数量をqとする。単純な予約関数が R'＝R＋q を行うなら、数量超過を防ぐには、実行前にどの条件が必要だろうか。

数学的整数で、0≦R≦C、0＜q≦C−R を仮定する。すると更新後は 0≦R'≦C が成り立つ。予約関数の前提を事前条件、実行後に満たす約束を事後条件として書けば、何を与えれば何を保証するかが見える。1

この式には、入力を検査する処理は含まれていない。外部から q＝−3 が渡らないことを、関数のコメントへ「正の整数」と書くだけで実現できるわけではない。入口で検査するか、検査済みの値しか渡さない呼出し規則を確実に守るかが必要になる。

事前条件は、外の世界への願望ではない。呼出し側が満たすべき契約である。その条件を確認せずに呼び出した結果まで、条件付きの証明が保証したことにはならない。

数学では正しくても、実装の条件が違うことがある

CもRもqも、実装上の整数型に収まるとする。それでも、途中の計算がその型で安全かは別途確認する。数学では制限のない整数として扱った式を、桁数に上限のある演算へ移すとき、丸めや桁あふれの意味が変わる場合がある。

さらに、本事例の証明は、条件を確認してから更新するまでにRが勝手に変わらないことを前提にしている。二つの処理が同じRを読み、それぞれが空き数量を確認した後に予約を確定するなら、各処理が見た事前条件だけでは全体の確保量を守れない。

数量の式が間違っていたのではない。単独の処理に対する式を、共有状態が変わる場面へ説明なく適用してしまったのである。第3巻の同時実行制御と、この章の契約は同じ境界でつながる。何を一つの不可分な操作にするかを、関数の外側でも定める必要がある。

ループの途中にも、変わらない約束を置く

注文明細の数量を合計する処理を考える。配列aの長さをnとし、先頭からi件を処理した合計をsとする。説明用の手順は次のとおりである。

i = 0
s = 0
while i < n:
    s = s + a[i]
    i = i + 1

ループの入口ごとに、0≦i≦n と「sは先頭i件の合計」を保つ。この不変条件は、iやsが変わらないという意味ではない。値が変わっても、値の間にある関係が保たれるという意味である。1

開始時、まだ一件も処理していないためiは0、合計も0で、約束は成立する。一回の処理でa[i]を加えてiを一つ進めれば、次の入口でもsは先頭i件の合計になる。終了時には i≧n と不変条件の i≦n を合わせてi＝nとなり、sは全件の合計だと分かる。

ただし、これは終了したときの結果へ至る説明である。必ず終了することも言うなら、nが有限で処理中に変わらず、各反復で非負整数 n−i が減少することなどを示す。配列の読取りが正常に行えることや、合計が実装の型に収まることも、実際の検証では別の条件になる。

証明できた条件と、書かなかった要求

Frama-CのWPは、ACSLで記述した契約について、最弱事前条件計算に基づく証明義務を作り、自動証明器などを使って検証する仕組みである。3 一部の入力を実行して成功した結果とは、対象にする範囲が違う。

それでも、書かなかった業務要求が自動的に証明されるわけではない。数量の合計が正しいことを示しても、取消し済みの明細を除外する必要が契約から落ちていれば、その業務上の欠落は残る。正しい契約を、適切なモデルと前提で表すことが重要になる。

また、証明義務を生成できたことと、必要な義務がすべて証明されたことも違う。未解決の条件を残したまま、ツールが最後まで動いたから証明済みと扱ってはいけない。使った前提、対象版、未解決の性質を、結果と一緒に読む。

本章の短い式は、人が関係を追うための作例である。Frama-Cでの機械証明を納品したわけではない。数学的な説明、有限範囲の例の確認、実際のプログラムに対する形式検証を分ける。

アサーションは、外部入力を安全にする魔法ではない

実行中に「確保量は保有量以下」をアサーションで検査すれば、設計上は起こらないはずの状態を顕在化させられる。だが、制約違反を検出した時点で、外部への通知や別DBの更新が済んでいるかもしれない。検出と、整合性を回復する処理は同じではない。

アサーションが無効になるかどうかも言語や実行設定に依存する。したがって、不正な外部入力に対する正式な拒否処理を、無条件にアサーションへ置き換えない。入力契約を検査して業務エラーを返す処理と、内部の前提違反を検出する処理は目的が異なる。1

青葉機材の数量超過は、顧客が正当に起こし得る入力である。システム障害として突然終了するより、「残り数量を超えるため確定できない」と扱う方が、本事例の業務に合っている。何を想定外とするかは、コードを書いた人の驚きではなく、仕様と境界から決める。

テストが、わざと間違えた実装を通してしまう

数量1〜20を許す検査を、意図的に1〜19へ変えたとする。数量1、5、19、21の試験だけなら、元の実装と変更後の実装は同じ結果になる。20を与える試験があれば、違いが見える。

ミューテーションテストは、実装に小さな変異を加え、既存テストがそれを検出できるかを調べる。PITの公式説明も、変異体を使ったときにテストが失敗することと、検出されず生き残ることを区別している。4 これは製品の欠陥数を直接数える方法ではなく、ある種類の変更に対してテストが敏感かを調べる方法である。

生き残った変異体は、そのまま「実在する欠陥一件」ではない。テストが不足している場合のほか、対象領域では元の実装と同じ振る舞いをする場合もある。さらに、PITではタイムアウトや実行エラー、対象行が実行されなかった結果も区別される。測定に失敗した結果を、通常の成功や等価性と混ぜない。4

既存テストが20の誤りを捕まえるようにしても、単価の時点が誤っている問題は残り得る。一つの検査が強くなったことを、すべての要求に対する保証へ広げない。

知識を答案へ戻す

午前Ⅱ。 静的解析、動的テスト、形式的な検証は、扱う対象と根拠が異なる。不変条件は変数が不変という意味ではない。アサーションによる検出と、入力検査や回復処理を区別する。

午後Ⅰ。 条件を確認する時点と更新する時点、想定した入力領域、途中で変化する共有状態を追う。どの約束が破られているかを本文の条件から特定する。

午後Ⅱ。 なぜその検証方法を選び、どの要求に対して、何を確認できたかを説明する。警告ゼロ、網羅率、証明結果の意味を分け、未確認の環境や業務条件を確認済みとしない。

立ち止まって考える：合計関数の正しさを証明すれば、請求金額も正しいか

合計の対象、単価の参照時点、割引、取消しの扱いが業務要件に合うかは別である。加算が正しくても、誤った項目や値を入力すれば、業務上は誤る。関数の契約と、その契約を使う業務上の妥当性の両方を確認する。

出典と照合範囲

[1] コンプリートテキスト第6・11・12章、IPA「SAシラバス Ver.5.2」6-2、9-2、11-5、11-7：事前条件・事後条件・不変条件、検証方法、テストの限界を出発点とした。予約の不等式とループの説明は独自に導出した。Pythonの数学的整数で、保有量0〜50の有効な予約、長さ0〜6・要素0〜2の配列、境界20の変異例を確認した。有限範囲の確認は一般的な機械証明や実機での試験ではない。公式シラバス

[2] Clang Static Analyzer, Important Points to Consider：解析量の制限、誤検知、検出する欠陥の種類について、公開説明を参照した。本文の料金誤りを同ツールで検出・実験したとはしていない。公式説明

[3] Frama-C, WP — Overview：ACSL契約、最弱事前条件計算、証明器との関係を参照した。WPの全機能や実装詳細を解説するものではなく、本章の例に対するツール実行も行っていない。公式概要

[4] PIT, Basic Concepts：変異体、等価な変異、Killed・Survived・No coverage・実行エラー等の区別を参照した。数量の例はPITによるJavaバイトコード変異ではなく、比較条件を変えた独自の小例である。公式説明