Bメソッドの抽象機械の証明責務

Bメソッド Coq

授業でBメソッドに入門してきた。
参考文献:「先端スキル開発特別講義?：形式手法を使ったデータ指向モデリングと検証」の資料
http://honiden-lab.ex.nii.ac.jp/u-tokyo/lecture2009/
BメソッドのツールであるAtelier Bのマニュアル
http://www.atelierb.eu/index-en.php

Bメソッド概要

わかったこと。

  • Bメソッドは、形式的に証明できる形で仕様を記述し、検証する形式手法の一種である。
  • Bメソッドは、操作というインターフェースをもつ抽象機械としてシステムを記述する。
  • 抽象機械は、変数をもち、操作の際の代入(substitution)によってその状態を変える。代入は非決定的でもよい。
  • 各操作には、操作を行うための条件(事前条件)がある。
  • 不変条件(invariant, 抽象機械が常に満たすべき命題)は、集合によって記述する。(2項関係、関数なども集合で表現できる。)
  • 仕様の詳細化(refinement)の機能があり、より抽象的な仕様とより実装(implementation)に近い仕様の関係の整合性が証明される。

証明責務

Bメソッドの(抽象機械の)検証の特徴は、
「抽象機械への操作(operation)を行っても常に不変条件が成り立っている」
という命題が自動的につくられ、
これを示しなさい、と言われる(証明責務, proof obligation)ことである。
それを以て抽象機械の正しさとするため、不変条件をどう書くかが非常に重要である。
Atelier Bはある程度自動で証明をしてくれるが、それで証明できない場合、
対話的に証明を完了させることになる。

抽象機械に対して生成される証明責務は、

  1. 初期状態が不変条件を満たす
  2. 事前条件と不変条件が満たされているとき、操作を行っても不変条件が満たされる

らしい。

理解を深めるため、抽象機械および証明責務をCoqで記述してみた。
ただし変数および代入などはとりあえずVariableで後回しにした。
気が向いたら実装するかも。

Require Import List.
Section B.

Variable (value : Set) (* 値 *)
(state : Set) (* 状態 *)
(substitution : Set) (* 代入文。 stateを変化させる *)
.
Definition stateSet := state -> Prop. (* stateの集合を命題で表現 *)
Variable (substDenote : substitution -> state -> stateSet)
  (* 代入文の効果。非決定的 *)
.
Definition predicate := state -> Prop.  (* stateを使って表現される命題 *)
Variable wp : substitution -> predicate -> predicate
  (* 代入文から最弱事前条件 (weakest precondition) が決まるとする *)
.

Hypothesis wp_ok : forall (subst : substitution) (predic : predicate) (st1 st2 : state),
  substDenote subst st1 st2 ->
    let P := wp subst predic in
    (P st1 -> predic st2) /\ 
      (forall P' : state -> Prop, (P' st1 -> predic st2) -> P st1)
(* wpは最弱事前条件を計算する *)
.

Record Operation : Type := {
  subst : substitution; (* 操作本体 *)
  pre : predicate; (* 事前条件 *)
  returnValue : state -> value (* 戻り値 *)
}.

Definition pred_preserved (predic : predicate)(op : Operation) : Prop :=
  forall st1 st2 : state, predic st1 -> pre op st1 -> 
    (substDenote (subst op) st1 st2) ->
    wp (subst op) predic st2
(* 事前条件が満たされている場合、predicがopによって保存される *)
.

Fixpoint all_list {A} (P : A -> Prop)(xs : list A) :=
  match xs with
    | nil => True
    | x :: xs' => P x /\ all_list P xs'
  end.

Record Machine := {
  initState : stateSet; (* 初期状態。非決定的 *)
  invariant : predicate; (* 不変条件 *)
  ops : list Operation; (* 操作の列 *)
  init_invariant : forall st : state, initState st -> invariant st;
    (* 初期状態は不変条件を満たす *)
  ops_invariant : all_list (pred_preserved invariant) ops
    (* すべての操作で不変条件が保存される *)
}.

End B.

Machineをレコードにし、フィールドinit_invariantと、ops_invariantで
証明責務を表現した。

「最弱事前条件(weakest precondition)」は、
Atelier Bのマニュアルには出てこなかったが
代入によって条件に現れる変数を代入後の式に書き換えることは
ダイクストラの最弱事前条件を計算していることに対応するため、
参考: http://en.wikipedia.org/wiki/Predicate_transformer_semantics
この表現を用いた。(授業では最弱事前条件、で教わった)

wp_okは、このままではwpに何も条件がついていないため、
「wpは最弱事前条件を計算する」という仮説をつけておいた。
しかしこの仮説の型、間違っているかもしれない。

非決定性をstate -> stateSet (= state -> state -> Prop)で表現すると
最弱事前条件が計算できる必要はないなと思った。