1 data Comm : Set where -2 Skip : Comm -3 Abort : Comm -4 PComm : PrimComm -> Comm -5 Seq : Comm -> Comm -> Comm -6 If : Cond -> Comm -> Comm -> Comm -7 While : Cond -> Comm -> Comm +
1 _-_ : ℕ → ℕ → ℕ -2 x - zero = x -3 zero - _ = zero -4 (suc x) - (suc y) = x - y +
1 program : Comm -2 program = -3 Seq ( PComm (λ env → record env {varn = 10})) -4 $ Seq ( PComm (λ env → record env {vari = 0})) -5 $ While (λ env → lt zero (varn env ) ) -6 (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -7 $ PComm (λ env → record env {varn = ((varn env) - 1)} )) +1-- HTProof の続き + 2 SeqRule : {bPre : Cond} → {cm1 : Comm} → {bMid : Cond} → + 3 {cm2 : Comm} → {bPost : Cond} → + 4 HTProof bPre cm1 bMid → + 5 HTProof bMid cm2 bPost → + 6 HTProof bPre (Seq cm1 cm2) bPost + 7 IfRule : {cmThen : Comm} → {cmElse : Comm} → + 8 {bPre : Cond} → {bPost : Cond} → + 9 {b : Cond} → +10 HTProof (bPre /\ b) cmThen bPost → +11 HTProof (bPre /\ neg b) cmElse bPost → +12 HTProof bPre (If b cmThen cmElse) bPost
1-- HTProof の続き - 2 WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} -> - 3 {bPost' : Cond} -> {bPost : Cond} -> - 4 Tautology bPre bPre' -> - 5 HTProof bPre' cm bPost' -> - 6 Tautology bPost' bPost -> - 7 HTProof bPre cm bPost - 8 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> - 9 HTProof (bInv /\ b) cm bInv -> -10 HTProof bInv (While b cm) (bInv /\ neg b) + 2 WeakeningRule : {bPre : Cond} → {bPre' : Cond} → {cm : Comm} → + 3 {bPost' : Cond} → {bPost : Cond} → + 4 Tautology bPre bPre' → + 5 HTProof bPre' cm bPost' → + 6 Tautology bPost' bPost → + 7 HTProof bPre cm bPost + 8 WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} → + 9 HTProof (bInv /\ b) cm bInv → +10 HTProof bInv (While b cm) (bInv /\ neg b)
1proof1 : HTProof initCond program termCond - 2proof1 = - 3 SeqRule {λ e → true} ( PrimRule empty-case ) - 4 $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 ) - 5 $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 ( - 6 WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10} +1 proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) + 2 proof1 c10 = + 3 SeqRule {λ e → true} ( PrimRule (init-case {c10} )) + 4 $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) + 5 $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( + 6 WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} 7 $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) - 8 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 + 8 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 9 -10initCond : Cond -11initCond env = true +10 initCond : Cond +11 initCond env = true 12 -13termCond : {c10 : ℕ} → Cond -14termCond {c10} env = Equal (vari env) c10 +13 termCond : {c10 : Nat} → Cond +14 termCond {c10} env = Equal (vari env) c10
- - - - - -
-1 lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) - 2 lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in - 3 begin - 4 (Equal (varn env) c10 ) ∧ true - 5 ≡⟨ ∧true ⟩ - 6 Equal (varn env) c10 - 7 ≡⟨ cond ⟩ - 8 true - 9 ∎ ) +1 lemma1 : {c10 : Nat} → Axiom (stmt1Cond {c10}) + 2 (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) + 3 lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + 4 begin + 5 (Equal (varn env) c10 ) ∧ true + 6 ≡⟨ ∧true ⟩ + 7 Equal (varn env) c10 + 8 ≡⟨ cond ⟩ + 9 true +10 ∎ ) +11 +12 stmt1Cond : {c10 : ℕ} → Cond +13 stmt1Cond {c10} env = Equal (varn env) c10 +14 +15 stmt2Cond : {c10 : ℕ} → Cond +16 stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
1 {-# TERMINATING #-} -2 whileLoop : {l : Level} {t : Set l} -> Env -> (Code : Env -> t) -> t +2 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t 3 whileLoop env next with lt 0 (varn env) 4 whileLoop env next | false = next env 5 whileLoop env next | true = @@ -652,11 +763,12 @@-Gears と HoareLogic をベースにした証明
+Gears と HoareLogic をベースにした証明(全体)
-
- ここでは +
- 最終状態で返ってくる i の値は c10 と一致する
+- これにより証明が可能
--1 proofGears : {c10 : ℕ } → Set +@@ -665,27 +777,26 @@ -1 proofGears : {c10 : Nat } → Set 2 proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 3 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 ))))<–! -[論文目次] -まえがき
+ -現状
- -Agda
- -GearsOS
+CodeGear DataGear
- -Gears と Agda
- -Agda での HoareLogic
- -Gears ベースの HoareLogic
- -まとめと課題
- -–>
+ diff -r 17b7605a5deb -r e8fe28afe61e slide/slide.md --- a/slide/slide.md Sun Jan 13 23:42:16 2019 +0900 +++ b/slide/slide.md Tue Jan 15 15:56:33 2019 +0900 @@ -1,4 +1,4 @@ -title: GearsOS の Hoare triple を用いた検証 +title: GearsOS の Hoare Logic を用いた検証 author: Masataka Hokama profile: 琉球大学 : 並列信頼研究室 lang: Japanese @@ -9,17 +9,17 @@ - OS やアプリケーションなどの信頼性は重要な課題 - 信頼性を上げるために仕様を検証する必要 - 仕様検証の手法として Floyd-Hoare Logic (以下 HoareLogic) がある - - 事前条件(PreCondition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(PostCondition)を満たす -- 既存の言語ではあまり利用されていない(python の pyrefine ってコードチェッカーくらい...?) + - 事前条件(Pre Condition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(Post Condition)を満たす +- 既存の言語ではあまり利用されていない ## 背景 - 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案 - CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む -- Gear 間の接続処理はメタ計算として定義 - - メタ計算部分に検証を埋め込むことで通常処理に手を加えずに検証 -- 本研究では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する + + +- この単位を用いて信頼性の高い OS として GearsOS を開発している +- 本発表では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する -## Gears について - **Gears** は当研究室で提案しているプログラム記述手法 @@ -29,19 +29,18 @@ - CodeGear の接続処理は通常の計算とは異なるメタ計算として定義 - メタ計算で信頼性の検証を行う - +
-
+ ## CbC について - Gears の単位でプログラミングできる言語として当研究室で開発している **CbC** (Continuation based C) が存在 - - これは C からループ制御構造と関数呼び出しを取り除き継続を導入したもの - - 環境を継続に含めない -- 現在の CbC ではメタ計算での検証 + - これは C からループ制御構造と関数呼び出しを取り除き、代わりに継続を導入したもの +- 現在の CbC でもメタ計算での検証は可能 - 将来的には証明も扱えるようにしたいが現段階では未実装 - そのため Gears の単位を定理証明支援系の言語である **Agda** で記述し、 Agda で証明している -## Agda +## Agda とは - Agda は定理証明支援系の言語 - 依存型を持つ関数型言語 - 型を明記する必要がある @@ -49,19 +48,15 @@ ## Agda のデータ型 - データ型は代数的なデータ構造 -- **data** キーワードの後に、**名前 : 型**、 where 句 +- **data** キーワードの後に、**名前 : 型** - 次の行以降は**コンストラクタ名 : 型** - 型は**->**または**→**で繋げる -- 例えば、型**PrimComm −> Comm**は**PrimComm** を受け取り**Comm**を返す型 -- 再帰的な定義も可能 + - 例えば、suc の型**Nat → Nat*は**Nat** を受け取り**Nat**を返す型 + - これにより 3 を suc (suc (suc zero)) のように表せる ```AGDA - data Comm : Set where - Skip : Comm - Abort : Comm - PComm : PrimComm −> Comm - Seq : Comm −> Comm −> Comm - If : Cond −> Comm −> Comm −> Comm - While : Cond −> Comm −> Comm + data Nat : Set where + zero : Nat + suc : Nat → Nat ``` @@ -70,201 +65,197 @@ - C 言語での構造体に近い - 複数のデータをまとめる - 関数内で構築できる -- 構築時は**レコード名 {フィールド名 = 値}** -- 複数ある場合は **{フィールド1 = 1 ; フィールド2 = 2}**のように **;** を使って列挙 - - (varn,vari の型 **ℕ** は Agda 上の 自然数、 データ型で zero : ℕ と succ : ℕ -> ℕ で定義されてる) +- 構築時は**record レコード名 {フィールド名 = 値}** +- 複数ある場合は **record Env {varn = 1 ; varn = 2}**のように **;** を使って列挙 ```AGDA - record Env : Set where - field - varn : ℕ - vari : ℕ + record Env : Set where + field + varn : Nat + vari : Nat ``` ## Agda の関数 -- 関数にも型が必要 -- 関数は **関数名 = 値** +- 関数にも型が必要(1行目) + - 引き算はは自然数を２つ取って結果の自然数を返す + - **_** は任意の値、名前で使うと受け取った引数が順番に入る +- 関数本体は **関数名 = 値** - 関数ではパターンマッチがかける -- **_** は任意の引数 + - ここでは関数名に **_** を使っているため**Nat**の定義にから zero かそれ以外でパターンマッチ ```AGDA - _-_ : ℕ → ℕ → ℕ - x - zero = x - zero - _ = zero - (suc x) - (suc y) = x - y + _-_ : Nat → Nat → Nat + x - zero = x + zero - _ = zero + (suc x) - (suc y) = x - y ``` ## Agda での証明 -- 関数の型に論理式 +- 関数の型に証明すべき論理式 - 関数自体にそれを満たす導出 - 完成した関数は証明 - **{}** は暗黙的(推論される) -- 下のコードは自然数に 0 を足したとき値が変わらないことの証明 +- 下のコードは Bool型の x と true の and を取ったものは x と等しいことの証明 + - **refl** は **x == x** の左右の項が等しいことの証明 ```AGDA - +zero : { y : ℕ } → y + zero ≡ y - +zero {zero} = refl - +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) + ∧true : { x : Bool } → x ∧ true ≡ x + ∧true {x} with x + ∧true {x} | false = refl + ∧true {x} | true = refl ``` ## Agda 上での HoareLogic -* 現在 Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと +* Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと それを Agda2 に書き写したものが存在している。 -* 今回はAgda2側の HoareLogic で使うコマンド定義の一部と、コマンドの証明に使うルールを借りて説明を行う。 - - -## Agda での HoareLogic の理解 -* HoareLogic を用いて次のようなプログラム(while Program)を検証した。 -```C - n = 10; - i = 0; +* 今回はAgda2側の HoareLogic で使うコマンド定義の一部と、コマンドの証明に使うルールを借りて Agda2上で HoareLogic を構築する - while (n>0) - { - i++; - n--; - } -``` -* このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす -* n==0のとき停止するため、終了時の変数の結果はi==10、n==0 になるはずである。 - -## HoareLogic +## HoareLogic とは * Floyd-Hoare Logic (以下HoareLogic)は部分的な正当性を検証する * プログラムは事前条件(Pre Condition)、事後条件(Post Condition)を持ち、条件がコマンドで更新され、事後条件になる * 事前、事後条件には変数や論理式、コマンドには代入や、繰り返し、条件分岐などがある。 -* コマンドが正しく成り立つことを保証することで、このコマンドを用いて記述されたプログラムの部分的な正しさを検証する +* コマンドが正しく成り立つことを保証することで、このコマンドを用いて記述されたプログラムの部分的な正しさを検証できる +## HoareLogic の理解 +- HoareLogic 例として疑似コードを用意した +- このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす +- n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になるはずである。 +- 次のスライドから Agda 上 HoareLogic を実装し、その上でこの whileProgram の検証を行う +```C + n = 10; + i = 0; -## Agda 上での HoareLogic(コマンド定義) -* Env は while Program の変数である var n, i -* **PrimComm** は代入時に使用される -* **Cond** は Condition で Env を受け取って Boolean の値を返す + while (n>0) + { + i++; + n--; + } +``` + +## Agda 上での HoareLogic(条件、変数の定義) +- **Env** は while Program で必要な変数をまとめたもの + - varn、vari はそれぞれ変数 n、 i +- **Cond** は Pre、Post の Condition で Env を受け取って Bool 値(true か false)を返す ```AGDA - record Env : Set where - field - varn : ℕ - vari : ℕ + record Env : Set where + field + varn : Nat + vari : Nat - PrimComm : Set - PrimComm = Env → Env - - Cond : Set - Cond = (Env → Bool) + Cond : Set + Cond = (Env → Bool) ``` ## Agda 上での HoareLogic(コマンド定義) -* **Comm** は Agda のデータ型で定義した HoareLogic の Command - * **Skip** は何も変更しない - * **PComm** は変数を代入する - * **Seq** は Command を実行して次の Command に移す - * **If** は Cond と2つの Comm を受け取り Cond の状態により実行する Comm を変える - * **while** は Cond と Comm を受け取り Cond の中身が真である間 Comm を繰り返す +* **Comm** は Agda のデータ型で定義した HoareLogic のコマンド + * **PComm** は変数を代入のコマンド + * **Seq** はコマンドの推移、 Command を実行して次の Command に移す + * **If** は条件分岐のコマンド + * **while** は繰り返しのコマンド +* 他にも何もしないコマンドやコマンドの停止などのコマンドもある +- **PrimComm** は Env を受け取って Env を返す定義 ```AGDA - data Comm : Set where - Skip : Comm - Abort : Comm - PComm : PrimComm -> Comm - Seq : Comm -> Comm -> Comm - If : Cond -> Comm -> Comm -> Comm - While : Cond -> Comm -> Comm + data Comm : Set where + PComm : PrimComm → Comm + Seq : Comm → Comm → Comm + If : Cond → Comm → Comm → Comm + While : Cond → Comm → Comm + + PrimComm : Set + PrimComm = Env → Env ``` ## Agda 上での HoareLogic(実際のプログラムの記述) -* Command を使って while Program を記述した。 +* 先程定義したコマンドを使って while Program を記述した + - 任意の自然数を引数に取る形になっているが**c10 == 10**ということにする * **$** は **()** の糖衣で行頭から行末までを ( ) で囲う - * 見やすさのため改行しているため 3~7 行はまとまっている -* Seq は Comm を2つ取って次の Comm に移行する +* 見やすさのため改行しているが 3~7 行は1行 ```AGDA - program : Comm - program = - Seq ( PComm (λ env → record env {varn = 10})) - $ Seq ( PComm (λ env → record env {vari = 0})) - $ While (λ env → lt zero (varn env ) ) - (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) - $ PComm (λ env → record env {varn = ((varn env) - 1)} )) + program : ℕ → Comm + program c10 = + Seq ( PComm (λ env → record env {varn = c10})) -- n = 10; + $ Seq ( PComm (λ env → record env {vari = 0})) -- i = 0; + $ While (λ env → lt zero (varn env ) ) -- while (n>0) { + (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -- i++; + $ PComm (λ env → record env {varn = ((varn env) - 1)} )) -- n--; ``` - -## Agda 上での HoareLogicの理解 -* 規則は HTProof にまとめられてる +## Agda 上での HoareLogic(コマンドの保証)1/3 +* 保証の規則は HTProof にまとめられてる * **PrimRule** は **PComm** で行う代入を保証する * 3行目の pr の型 Axiom は PreCondition に PrimComm が適用されると PostCondition になることの記述 - * **_⇒_** は pre, post の Condition をとって post の Condition が成り立つときに True を返す関数 -* SkipRule は PreCondition を変更しないことの保証 -* AbortRule は プログラムが停止するときのルール + * **_⇒_** は pre, post の Condition をとって post の Condition が成り立つときに True を返す ```AGDA - data HTProof : Cond -> Comm -> Cond -> Set where - PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} -> - (pr : Axiom bPre pcm bPost) -> - HTProof bPre (PComm pcm) bPost - SkipRule : (b : Cond) -> HTProof b Skip b - AbortRule : (bPre : Cond) -> (bPost : Cond) -> - HTProof bPre Abort bPost + data HTProof : Cond → Comm → Cond → Set where + PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} → + (pr : Axiom bPre pcm bPost) → + HTProof bPre (PComm pcm) bPost -- 次のスライドに続く ``` ```AGDA - Axiom : Cond -> PrimComm -> Cond -> Set - Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true + Axiom : Cond → PrimComm → Cond → Set + Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true ``` -## Agda 上での HoareLogicの理解 +## Agda 上での HoareLogic(コマンド保証)2/3 * **SeqRule** は Command を推移させる Seq の保証 * **IfRule** は If の Command が正しく動くことを保証 ```AGDA -- HTProof の続き - SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} -> - {cm2 : Comm} -> {bPost : Cond} -> - HTProof bPre cm1 bMid -> - HTProof bMid cm2 bPost -> - HTProof bPre (Seq cm1 cm2) bPost - IfRule : {cmThen : Comm} -> {cmElse : Comm} -> - {bPre : Cond} -> {bPost : Cond} -> - {b : Cond} -> - HTProof (bPre /\ b) cmThen bPost -> - HTProof (bPre /\ neg b) cmElse bPost -> - HTProof bPre (If b cmThen cmElse) bPost + SeqRule : {bPre : Cond} → {cm1 : Comm} → {bMid : Cond} → + {cm2 : Comm} → {bPost : Cond} → + HTProof bPre cm1 bMid → + HTProof bMid cm2 bPost → + HTProof bPre (Seq cm1 cm2) bPost + IfRule : {cmThen : Comm} → {cmElse : Comm} → + {bPre : Cond} → {bPost : Cond} → + {b : Cond} → + HTProof (bPre /\ b) cmThen bPost → + HTProof (bPre /\ neg b) cmElse bPost → + HTProof bPre (If b cmThen cmElse) bPost ``` -## Agda 上での HoareLogicの理解 +## Agda 上での HoareLogic(コマンド保証)3/3 * **WeakeningRule** は通常の Condition からループ不変条件(Loop Invaliant)に変換 * Tautology は Condition と不変条件が等しく成り立つ * **WhileRule** はループ不変条件が成り立つ間 Comm を繰り返す ```AGDA -- HTProof の続き - WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} -> - {bPost' : Cond} -> {bPost : Cond} -> - Tautology bPre bPre' -> - HTProof bPre' cm bPost' -> - Tautology bPost' bPost -> - HTProof bPre cm bPost - WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> - HTProof (bInv /\ b) cm bInv -> - HTProof bInv (While b cm) (bInv /\ neg b) + WeakeningRule : {bPre : Cond} → {bPre' : Cond} → {cm : Comm} → + {bPost' : Cond} → {bPost : Cond} → + Tautology bPre bPre' → + HTProof bPre' cm bPost' → + Tautology bPost' bPost → + HTProof bPre cm bPost + WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} → + HTProof (bInv /\ b) cm bInv → + HTProof bInv (While b cm) (bInv /\ neg b) ``` ```AGDA - Tautology : Cond -> Cond -> Set - Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true + Tautology : Cond → Cond → Set + Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true ``` + ## Agda 上での HoareLogic(証明) -* **proof1** は while Program の証明 -* HTProof に 初期状態とコマンドで書かれた **program** と終了状態を渡す -* lemma1~5は rule それぞれの証明 -* +- **proof1** は while Program の証明 +- HTProof に 初期状態と先程コマンドで記述した whileProgram である **program** と終了状態を渡す +- Condititon は initCond や termCond のようにそれぞれ定義する必要がある +- program に近い形で証明を記述できる ```AGDA - proof1 : HTProof initCond program termCond - proof1 = - SeqRule {λ e → true} ( PrimRule empty-case ) - $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 ) - $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 ( - WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10} - $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) - $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 + proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) + proof1 c10 = + SeqRule {λ e → true} ( PrimRule (init-case {c10} )) + $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) + $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( + WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} + $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 - initCond : Cond - initCond env = true + initCond : Cond + initCond env = true - termCond : {c10 : ℕ} → Cond - termCond {c10} env = Equal (vari env) c10 + termCond : {c10 : Nat} → Cond + termCond {c10} env = Equal (vari env) c10 ``` - + @@ -273,12 +264,19 @@ -## 証明の一部 -- 基本的な証明方法は Condtition を変化させて次の Condition が成り立つように変形する -- impl⇒ +## 証明の一部(lemma1) +- PComm の証明である lemma1 だけ解説 +- lemma1 は n に 10 を代入したあと、 i に 0 を代入するところ +- 証明することは**事前条件の n ≡ 10 が成り立つか** +- PreCondition が成り立つとき、Command を実行するとPostConditionが成り立つ + - Axiom は x ⇒ y ≡ true が成り立てば良かった + - **_⇒_** は事後条件が成り立つかどうか + - impl⇒ は x ≡ true → y ≡ true の関数(Command)を受け取って x ⇒ y ≡ true を返す関数 +- **≡-Reasoning** は Agda での等式変形 ```AGDA - lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) - lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + lemma1 : {c10 : Nat} → Axiom (stmt1Cond {c10}) + (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) + lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in begin (Equal (varn env) c10 ) ∧ true ≡⟨ ∧true ⟩ @@ -286,52 +284,112 @@ ≡⟨ cond ⟩ true ∎ ) + + stmt1Cond : {c10 : ℕ} → Cond + stmt1Cond {c10} env = Equal (varn env) c10 + + stmt2Cond : {c10 : ℕ} → Cond + stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) ``` - + - + - + ## Agda での Gears - Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数 - CPS の関数は引数として継続を受け取って継続に計算結果を渡す -- **名前 : 引数 -> (Code : fa -> t) -> t** +- **名前 : 引数 → (Code : fa → t) → t** - **t** は継続 -- **(Code : fa -> t)** は次の継続先 +- **(Code : fa → t)** は次の継続先 - DataGear は Agda での CodeGear に使われる引数 ```AGDA -_g-_ : {t : Set} → ℕ → ℕ → (Code : ℕ → t) → t -x g- zero next = next x -zero g- _ = next zero -(suc x) g- (suc y) = next (x g- y) +_-_ : {t : Set} → Nat → Nat → (Code : Nat → t) → t +x - zero = (λ next → next x) +zero - _ = (λ next → next zero) +(suc x) - (suc y) = (x - y) +``` + +## Gears をベースにした HoareLogic と証明(全体) +- Gears をベースにした while Program + - これは証明でもある +- whileループを任意の回数にするため**c10**は引数 +- whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が c10 と等しい +```AGDA + proofGears : {c10 : Nat } → Set + proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 + (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) ``` -## Gears をベースにした HoareLogic -* 次に Gears をベースにした while Program をみる。 -* このプログラムは自然数と継続先を受け取って t を返す +## Gears と HoareLogic をベースにした証明(whileTest) +- ここは代入する Command +- 最初の Command なので PreCondition がない +- もとの whileProgram では PComm を2回していたがまとめた +- proof2は Post Condition が成り立つことの証明 + - **_/\\_** は pi1 と pi2 のフィールドをもつレコード型 + - ２つのものを引数に取り、両方が同時に成り立つことを示す +- Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t** +```AGDA + whileTest' : {l : Level} {t : Set l} → {c10 : Nat } → + (Code : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t + whileTest' {_} {_} {c10} next = next env proof2 + where + env : Env + env = record {vari = 0 ; varn = c10} + proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) <-- PostCondition + proof2 = record {pi1 = refl ; pi2 = refl} +``` + +## Gears と HoareLogic をベースにした証明(conversion) +- conversion は Condition から LoopInvaliant への変換を行う CodeGear +- proof4 は LoopInvaliant の証明 +- Gears での HoareLogic の完全な記述は **引数 → PreCondition → (Code : fa → PostCondition → t) → t** +```AGDA + conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : Nat } → + ((vari env) ≡ 0) /\ ((varn env) ≡ c10) + → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t + conversion1 env {c10} p1 next = next env proof4 + where + proof4 : varn env + vari env ≡ c10 + proof4 = let open ≡-Reasoning in + begin + varn env + vari env + ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ + c10 + vari env + ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ + c10 + 0 + ≡⟨ +-sym {c10} {0} ⟩ + c10 + ∎ +``` + +## Gears と HoareLogic をベースにした証明(whileLoop) +- whileLoop は loopInvaliant が true の間 WhileLoop を回し続けるCodeGear +- この CodeGear は Agda がループが終わることが証明できてないため **{-# TERMINATING #-}** で明示 +- false になると次の CodeGear へ ```AGDA {-# TERMINATING #-} - whileLoop : {l : Level} {t : Set l} -> Env -> (Code : Env -> t) -> t + whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t whileLoop env next with lt 0 (varn env) whileLoop env next | false = next env whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next ``` -## Gears と HoareLogic をベースにした証明 -* ここでは +## Gears と HoareLogic をベースにした証明(全体) +- 最終状態で返ってくる i の値は c10 と一致する +- これにより証明が可能 ```AGDA - proofGears : {c10 : ℕ } → Set + proofGears : {c10 : Nat } → Set proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) ``` - ## まとめと今後の課題 - HoareLogic の while を使った例題を作成、証明を行った - Gears を用いた HoareLogic ベースの検証方法を導入した