VSTTE 2012 Software Verification Competition
VSTTEという国際会議の開催した「ソフトウェア検証大会」
に挑戦していました。48時間で5問の仕様と実装が提示されて、その正しさ、つまり停止性や、配列の範囲外アクセスをしないこと、仕様を満たしていることなどを、なんでも自由なツールを使っていいから検証してみよう！というコンテストです。
というわけで、Coq でやってみて、力尽きました。難しいですね！コードだけ貼り付けておきます（提出はしてない）。
Problem 1
とある bool のソートアルゴリズム。
- Coq で書けたので停止性は示されているはず
- 配列は範囲内であることが証明されている整数でしかアクセスできない依存型なのでアクセスも安全なはず
- 返値が sorted であることも証明付きの依存型なので大丈夫なはず
- 元のpermutationであることは示せてない
Require Import ZArith Omega Zwf. Require Import List Bool. Require Import Program Relations Wellfounded. Open Scope Z_scope. (** * Definition of arrays of size [n] with element type [t]. * They are indexed by 0 <= i < n and returns t. *) Definition index (n: Z) := {i | 0<=i /\ i<n}. Definition array (n: {n|n>=0}) (t: Type) := forall (i: index (`n)), t. Axiom proof_irrelevance : forall n t (a:array n t) i j, `i = `j -> a i = a j. (** * Definition of swap. *) Program Definition swap {n} {t} (a: array n t) (i j: index n) := fun (k: index n) => if Z_eq_dec k i then a j else if Z_eq_dec k j then a i else a k. (** * Definition of sortedness *) Program Definition sorted {n} (a: array n bool) := forall i j, a i=false /\ a j=true -> i<j. (** * The main loop. * * The algorithm in the problem statement is implemented. * Four invariants are hand-annotated and proven. *) Local Obligation Tactic := (program_simpl; unfold Zwf; try omega). Program Fixpoint loop {n} (a: array n bool) (i j: Z) (* Loop invariants. *) (inv1: 0<=i /\ i<=n) (inv2: j<n) (inv3: forall (k: index n), k<i -> a k=false) (inv4: forall (k: index n), k>j -> a k=true) (* Termination measure: j-i is decreasing. *) {measure (j - i) (Zwf 0)} (* Return type assures sortedness *) : {a: array n bool | sorted a} := if Z_le_dec i j then if bool_dec (a i) false then loop a (i+1) j _ _ _ _ (* 4: inv3 *) else if bool_dec (a j) true then loop a i (j-1) _ _ _ _ (* 11: inv4 *) else loop (swap a i j) (i+1) (j-1) _ _ _ _ (*17,18: inv3,4*) else a. (* 20: sorted *) (* Discharging proof obligations. *) Obligation 4. assert (X: `k=i \/ `k<i) by omega; destruct X; [rewrite <-H0|]; eauto using proof_irrelevance. Qed. Obligation 11. assert (X: `k=j \/ `k>j) by omega; destruct X; [rewrite <-H1|]; eauto using proof_irrelevance. Qed. Obligation 17. unfold swap. destruct Z_eq_dec. (* k=i *) rewrite <-(not_true_is_false _ H1). eauto using proof_irrelevance. simpl in n0. destruct Z_eq_dec. (* k=j *) assert (`k <> j) by omega. contradiction. (* other *) apply inv3; omega. Qed. Obligation 18. unfold swap. destruct Z_eq_dec. (* k=i *) simpl in e. rewrite <-(not_false_is_true _ H0). assert (i = j) by omega. eauto using proof_irrelevance. destruct Z_eq_dec. (* k=j *) rewrite <-(not_false_is_true _ H0). eauto using proof_irrelevance. (* other *) simpl in n1. apply inv4; omega. Qed. Obligation 20. unfold sorted; intros i0 j0 [Hi Hj]. assert (~(`i0 >= i) /\ ~(i > `j0)). split. intro. assert (`i0 > j) by omega. rewrite (inv4 i0 H4) in Hi. auto using diff_true_false. intro. assert (`j0 < i) by omega. rewrite (inv3 j0 H4) in Hj. auto using diff_true_false. omega. Qed. (* Entry point *) Program Fixpoint two_way_sort {n} (a: array n bool) : {a: array n bool | sorted a} := loop a 0 (n-1) _ _ _ _. Obligation 3. destruct k; simpl in H; apply False_ind; omega. Qed. Obligation 4. destruct k; simpl in H; apply False_ind; omega. Qed.
Problem 4
リストから、規則に従ってツリーを作る。
- Coq で書けたので停止性は示されているはず
- 健全性や完全性は示せてない
Require Import Arith Omega. Require Import List. Require Import Program Relations Wellfounded. Local Obligation Tactic := (program_simpl; simpl in *; try omega). (** * Definition of trees and lists *) Inductive tree := | Leaf : tree | Node : tree -> tree -> tree. Definition list := List.list nat. (** * The implementation. * * Immutable list is used. So, the build_rec function returns * the list left after the procedure as well as the tree. * Also, failure is reprensented by the option type. *) Program Fixpoint build_rec (d: nat) (s: list) (* Termination measure: lexicographic order on (|s|, h-d) *) {measure (match s with nil => existT _ 0 0 | cons h _ => existT _ (length s) (h - d) end) (lexprod nat _ lt (fun _ => lt))} (* 5 *) (* Return type with a post condition on length decreasing *) : option (tree * {t: list | length t < length s}) := (* The algorithm written in the problem statement. *) match s with | nil => None | cons h t => if lt_dec h d then None else if eq_nat_dec h d then Some (Leaf, t) (* 1 *) else match build_rec (d+1) s with (* 2 *) | None => None | Some (l, s) => match build_rec (d+1) s with (* 3 *) | None => None | Some (r, s) => Some (Node l r, s) (* 4 *) end end end. (** Discharge proof obligations. * 1,4 : Returned list gets shorter (auto). * 2,3 : Argument is decreasing. * 5 : Wellfoundedness of the termination measure. *) Obligation 2. right; omega. (* h-d is decreasing. *) Qed. Obligation 3. destruct s0; left; simpl in *; omega. (* |s| decreases. *) Qed. Obligation 5. auto using measure_wf, wf_lexprod, lt_wf. Defined. Definition build (s: list) : option tree := match build_rec 0 s with | Some (t, exist nil _) => Some t | _ => None end. (** * Test cases (run in OCaml). *) Definition test1_in := [1;3;3;2]. Definition test1_out := Some (Node Leaf (Node (Node Leaf Leaf) Leaf)). Definition test2_in := [1;3;2;2]. Definition test2_out := @None tree. Extraction "extracted.ml" build test1_in test1_out test2_in test2_out.
test.ml
#use "extracted.ml" let _ = assert (build test1_in = test1_out); assert (build test2_in = test2_out); print_endline "[TEST PASSED]"
