Mercurial > hg > Papers > 2019 > ryokka-sigss
changeset 14:b711209123f7
update
author | ryokka |
---|---|
date | Tue, 15 Jan 2019 17:47:18 +0900 |
parents | fde9ee0cc8ae |
children | e285fb83488b |
files | slide/Makefile slide/slide.html slide/slide.md |
diffstat | 3 files changed, 353 insertions(+), 388 deletions(-) [+] |
line wrap: on
line diff
--- a/slide/Makefile Tue Jan 15 16:52:28 2019 +0900 +++ b/slide/Makefile Tue Jan 15 17:47:18 2019 +0900 @@ -3,8 +3,7 @@ .SUFFIXES: .md .html .md.html: - slideshow b $< -t s6cr --h2 - + slideshow b $< -t s6cr --h2; perl -i -pe 's|<span class="line-numbers">\s*<a href="\#n\d+"name="n\d+">\d+</a></span>||gi' slide.html all: $(TARGET).html open $(TARGET).html -a Google\ Chrome clean:
--- a/slide/slide.html Tue Jan 15 16:52:28 2019 +0900 +++ b/slide/slide.html Tue Jan 15 17:47:18 2019 +0900 @@ -172,7 +172,8 @@ <ul> <li>Agda は定理証明支援系の言語</li> <li>依存型を持つ関数型言語</li> - <li>型を明記する必要がある</li> + <li>Curry-Howard の証明支援系</li> + <li>型と値がある</li> <li>Agda の文法については次のスライドから軽く説明する</li> </ul> @@ -182,47 +183,18 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="agda-のデータ型">Agda のデータ型</h2> +<h2 id="agda-での-gears-の記述whileloop">Agda での Gears の記述(whileLoop)</h2> <ul> - <li>データ型は代数的なデータ構造</li> - <li><strong>data</strong> キーワードの後に、<strong>名前 : 型</strong></li> - <li>次の行以降は<strong>コンストラクタ名 : 型</strong></li> - <li>型は<strong>-></strong>または<strong>→</strong>で繋げる - <ul> - <li>例えば、suc の型<strong>Nat → Nat*は</strong>Nat** を受け取り<strong>Nat</strong>を返す型</li> - <li>これにより 3 を suc (suc (suc zero)) のように表せる - <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> data Nat : Set where -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> zero : Nat -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> suc : Nat → Nat -</pre></div> -</div> - </div> - </li> - </ul> - </li> -</ul> - -<!-- - where は宣言した部分に束縛する --> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="agda-のレコード型">Agda のレコード型</h2> -<ul> - <li>C 言語での構造体に近い</li> - <li>複数のデータをまとめる</li> - <li>関数内で構築できる</li> - <li>構築時は<strong>record レコード名 {フィールド名 = 値}</strong></li> - <li>複数ある場合は <strong>record Env {varn = 1 ; varn = 2}</strong>のように <strong>;</strong> を使って列挙 + <li>Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数</li> + <li>CPS の関数は引数として継続を受け取って継続に計算結果を渡す</li> + <li><strong>名前 : 引数 → (Code : fa → t) → t</strong></li> + <li><strong>t</strong> は継続</li> + <li><strong>(Code : fa → t)</strong> は次の継続先</li> + <li>DataGear は Agda での CodeGear に使われる引数 <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> record Env : Set where -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> field -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> varn : Nat -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> vari : Nat + <div class="code"><pre>whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) + → (Code : Env -> t) -> t +whileTest c10 next = next (record {varn = c10 ; vari = 0} ) </pre></div> </div> </div> @@ -235,28 +207,46 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="agda-の関数">Agda の関数</h2> +<h2 id="agda-での-gears-の記述whileloop-1">Agda での Gears の記述(whileLoop)</h2> <ul> - <li>関数にも型が必要(1行目) + <li>関数の動作を条件で変えたいときはパターンマッチを行う</li> + <li>whileLoop は varn が 0 より大きい間ループする <ul> - <li>引き算はは自然数を2つ取って結果の自然数を返す</li> - <li><strong>_</strong> は任意の値、名前で使うと受け取った引数が順番に入る</li> + <li>lt は Nat を2つ受け取って値の大小を比較 +```AGDA +{-# TERMINATING #-} +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</li> </ul> </li> - <li>関数本体は <strong>関数名 = 値</strong></li> - <li>関数ではパターンマッチがかける - <ul> - <li>ここでは関数名に <strong>_</strong> を使っているため<strong>Nat</strong>の定義にから zero かそれ以外でパターンマッチ - <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> _-_ : Nat → Nat → Nat -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> x - zero = x -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> zero - _ = zero -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> (suc x) - (suc y) = x - y +</ul> + +<p>lt : Nat → Nat → Bool</p> +<pre><code> +## Agda での DataGear +- **DataGear** は CodeGear の引数 +- **データ型**と**レコード型**がある +- データ型は一つのデータ +```AGDA +data Nat : Set where + zero : Nat + suc : Nat → Nat +</code></pre> +<ul> + <li>レコード型は複数のデータをまとめる + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre>record Env : Set where +field + varn : Nat + vari : Nat </pre></div> </div> - </div> - </li> - </ul> + </div> </li> </ul> @@ -276,10 +266,10 @@ <ul> <li><strong>refl</strong> は <strong>x == x</strong> の左右の項が等しいことの証明 <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> ∧true : { x : Bool } → x ∧ true ≡ x -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> ∧true {x} with x -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> ∧true {x} | false = refl -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> ∧true {x} | true = refl + <div class="code"><pre>∧true : { x : Bool } → x ∧ true ≡ x +∧true {x} with x +∧true {x} | false = refl +∧true {x} | true = refl </pre></div> </div> </div> @@ -294,6 +284,146 @@ <div class='slide'> <!-- _S9SLIDE_ --> +<h2 id="gears-をベースにした-hoarelogic-と証明全体">Gears をベースにした HoareLogic と証明(全体)</h2> +<ul> + <li>Gears をベースにした while Program で実行できる + <ul> + <li>これは証明も持っている</li> + </ul> + </li> + <li>whileループを任意の回数にするため<strong>c10</strong>は引数</li> + <li>whileTest’ の継続に conversion1、その継続に whileLoop’ が来て最後の継続に vari が c10 と等しい + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre>proofGears : {c10 : Nat } → Set +proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 + (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) +</pre></div> +</div> + </div> + </li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="gears-と-hoarelogic-をベースにした証明whiletest">Gears と HoareLogic をベースにした証明(whileTest)</h2> +<ul> + <li>最初の Command なので PreCondition がない</li> + <li>proof2は Post Condition が成り立つことの証明 + <ul> + <li><strong><em>/\</em></strong> は pi1 と pi2 のフィールドをもつレコード型</li> + <li>2つのものを引数に取り、両方が同時に成り立つことを示す</li> + </ul> + </li> + <li>Gears での PostCondition は <strong>引数 → (Code : fa → PostCondition → t) → t</strong> + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre>whileTest' : {l : Level} {t : Set l} → {c10 : Nat } → + (Code : (env : Env) → + ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t +hileTest' {_} {_} {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} +</pre></div> +</div> + </div> + </li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="gears-と-hoarelogic-をベースにした証明conversion">Gears と HoareLogic をベースにした証明(conversion)</h2> +<ul> + <li>conversion は Condition から LoopInvaliant への変換を行う CodeGear + <ul> + <li>Condition の条件は Loop 内では厳しいのでゆるくする</li> + </ul> + </li> + <li>proof4 は LoopInvaliant の証明</li> + <li>Gears での HoareLogic の完全な記述は <strong>引数 → PreCondition → (Code : fa → PostCondition → t) → t</strong> +```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</li> +</ul> + +<pre><code> + +## Agdaでの証明(≡-Reasoning) +- Agda では証明の項を書き換える構文が用意されている +```AGDA + 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 + ∎ +</code></pre> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="gears-と-hoarelogic-をベースにした証明全体">Gears と HoareLogic をベースにした証明(全体)</h2> +<ul> + <li>最終状態で返ってくる i の値は c10 と一致する</li> + <li>これにより証明が可能 + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre> proofGears : {c10 : Nat } → Set + proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 + (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) +</pre></div> +</div> + </div> + </li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="まとめと今後の課題">まとめと今後の課題</h2> +<ul> + <li>HoareLogic の while を使った例題を作成、証明を行った</li> + <li>Gears を用いた HoareLogic ベースの検証方法を導入した + <ul> + <li>証明が引数として渡される記述のため証明とプログラムを一体化できた</li> + </ul> + </li> + <li>今後の課題 + <ul> + <li>RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで)</li> + </ul> + </li> +</ul> + + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> <h2 id="agda-上での-hoarelogic">Agda 上での HoareLogic</h2> <ul> <li>Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと @@ -328,14 +458,14 @@ <li>n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になるはずである。</li> <li>次のスライドから Agda 上 HoareLogic を実装し、その上でこの whileProgram の検証を行う <div class="language-C highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> n = <span style="color:#00D">10</span>; -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> i = <span style="color:#00D">0</span>; -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> <span style="color:#080;font-weight:bold">while</span> (n><span style="color:#00D">0</span>) -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> { -<span class="line-numbers"><a href="#n6" name="n6">6</a></span> i++; -<span class="line-numbers"><a href="#n7" name="n7">7</a></span> n--; -<span class="line-numbers"><a href="#n8" name="n8">8</a></span> } + <div class="code"><pre> n = <span style="color:#00D">10</span>; + i = <span style="color:#00D">0</span>; + + <span style="color:#080;font-weight:bold">while</span> (n><span style="color:#00D">0</span>) + { + i++; + n--; + } </pre></div> </div> </div> @@ -354,13 +484,13 @@ <li>varn、vari はそれぞれ変数 n、 i</li> <li><strong>Cond</strong> は Pre、Post の Condition で Env を受け取って Bool 値(true か false)を返す <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> record Env : Set where -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> field -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> varn : Nat -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> vari : Nat -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> -<span class="line-numbers"><a href="#n6" name="n6">6</a></span> Cond : Set -<span class="line-numbers"><a href="#n7" name="n7">7</a></span> Cond = (Env → Bool) + <div class="code"><pre> record Env : Set where + field + varn : Nat + vari : Nat + + Cond : Set + Cond = (Env → Bool) </pre></div> </div> </div> @@ -386,14 +516,14 @@ <li>他にも何もしないコマンドやコマンドの停止などのコマンドもある</li> <li><strong>PrimComm</strong> は Env を受け取って Env を返す定義 <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> data Comm : Set where -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> PComm : PrimComm → Comm -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> Seq : Comm → Comm → Comm -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> If : Cond → Comm → Comm → Comm -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> While : Cond → Comm → Comm -<span class="line-numbers"><a href="#n6" name="n6">6</a></span> -<span class="line-numbers"><a href="#n7" name="n7">7</a></span> PrimComm : Set -<span class="line-numbers"><a href="#n8" name="n8">8</a></span> PrimComm = Env → Env + <div class="code"><pre> 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 </pre></div> </div> </div> @@ -416,13 +546,13 @@ <li><strong>$</strong> は <strong>()</strong> の糖衣で行頭から行末までを ( ) で囲う</li> <li>見やすさのため改行しているが 3~7 行は1行 <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> program : ℕ → Comm -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> program c10 = -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> Seq ( PComm (λ env → record env {varn = c10})) -- n = 10; -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> $ Seq ( PComm (λ env → record env {vari = 0})) -- i = 0; -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> $ While (λ env → lt zero (varn env ) ) -- while (n>0) { -<span class="line-numbers"><a href="#n6" name="n6">6</a></span> (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -- i++; -<span class="line-numbers"><a href="#n7" name="n7">7</a></span> $ PComm (λ env → record env {varn = ((varn env) - 1)} )) -- n--; + <div class="code"><pre> 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--; </pre></div> </div> </div> @@ -443,17 +573,17 @@ <ul> <li><strong><em>⇒</em></strong> は pre, post の Condition をとって post の Condition が成り立つときに True を返す <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> data HTProof : Cond → Comm → Cond → Set where -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} → -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> (pr : Axiom bPre pcm bPost) → -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> HTProof bPre (PComm pcm) bPost -<span class="line-numbers"><a href="#n5" name="n5">5</a></span>-- 次のスライドに続く + <div class="code"><pre> data HTProof : Cond → Comm → Cond → Set where + PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} → + (pr : Axiom bPre pcm bPost) → + HTProof bPre (PComm pcm) bPost +-- 次のスライドに続く </pre></div> </div> </div> <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> Axiom : Cond → PrimComm → Cond → Set -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true + <div class="code"><pre> Axiom : Cond → PrimComm → Cond → Set + Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true </pre></div> </div> </div> @@ -473,18 +603,18 @@ <li><strong>SeqRule</strong> は Command を推移させる Seq の保証</li> <li><strong>IfRule</strong> は If の Command が正しく動くことを保証 <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>-- HTProof の続き -<span class="line-numbers"> <a href="#n2" name="n2">2</a></span> SeqRule : {bPre : Cond} → {cm1 : Comm} → {bMid : Cond} → -<span class="line-numbers"> <a href="#n3" name="n3">3</a></span> {cm2 : Comm} → {bPost : Cond} → -<span class="line-numbers"> <a href="#n4" name="n4">4</a></span> HTProof bPre cm1 bMid → -<span class="line-numbers"> <a href="#n5" name="n5">5</a></span> HTProof bMid cm2 bPost → -<span class="line-numbers"> <a href="#n6" name="n6">6</a></span> HTProof bPre (Seq cm1 cm2) bPost -<span class="line-numbers"> <a href="#n7" name="n7">7</a></span> IfRule : {cmThen : Comm} → {cmElse : Comm} → -<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> {bPre : Cond} → {bPost : Cond} → -<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> {b : Cond} → -<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> HTProof (bPre /\ b) cmThen bPost → -<span class="line-numbers"><a href="#n11" name="n11">11</a></span> HTProof (bPre /\ neg b) cmElse bPost → -<span class="line-numbers"><a href="#n12" name="n12">12</a></span> HTProof bPre (If b cmThen cmElse) bPost + <div class="code"><pre>-- 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 </pre></div> </div> </div> @@ -503,22 +633,22 @@ <li>Tautology は Condition と不変条件が等しく成り立つ</li> <li><strong>WhileRule</strong> はループ不変条件が成り立つ間 Comm を繰り返す <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span>-- HTProof の続き -<span class="line-numbers"> <a href="#n2" name="n2">2</a></span> WeakeningRule : {bPre : Cond} → {bPre' : Cond} → {cm : Comm} → -<span class="line-numbers"> <a href="#n3" name="n3">3</a></span> {bPost' : Cond} → {bPost : Cond} → -<span class="line-numbers"> <a href="#n4" name="n4">4</a></span> Tautology bPre bPre' → -<span class="line-numbers"> <a href="#n5" name="n5">5</a></span> HTProof bPre' cm bPost' → -<span class="line-numbers"> <a href="#n6" name="n6">6</a></span> Tautology bPost' bPost → -<span class="line-numbers"> <a href="#n7" name="n7">7</a></span> HTProof bPre cm bPost -<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} → -<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> HTProof (bInv /\ b) cm bInv → -<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> HTProof bInv (While b cm) (bInv /\ neg b) + <div class="code"><pre>-- 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) </pre></div> </div> </div> <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> Tautology : Cond → Cond → Set -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true + <div class="code"><pre> Tautology : Cond → Cond → Set + Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true </pre></div> </div> </div> @@ -538,20 +668,20 @@ <li>Condititon は initCond や termCond のようにそれぞれ定義する必要がある</li> <li>program に近い形で証明を記述できる <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span> proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) -<span class="line-numbers"> <a href="#n2" name="n2">2</a></span> proof1 c10 = -<span class="line-numbers"> <a href="#n3" name="n3">3</a></span> SeqRule {λ e → true} ( PrimRule (init-case {c10} )) -<span class="line-numbers"> <a href="#n4" name="n4">4</a></span> $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) -<span class="line-numbers"> <a href="#n5" name="n5">5</a></span> $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( -<span class="line-numbers"> <a href="#n6" name="n6">6</a></span> WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} -<span class="line-numbers"> <a href="#n7" name="n7">7</a></span> $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) -<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 -<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> -<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> initCond : Cond -<span class="line-numbers"><a href="#n11" name="n11">11</a></span> initCond env = true -<span class="line-numbers"><a href="#n12" name="n12">12</a></span> -<span class="line-numbers"><a href="#n13" name="n13">13</a></span> termCond : {c10 : Nat} → Cond -<span class="line-numbers"><a href="#n14" name="n14">14</a></span> termCond {c10} env = Equal (vari env) c10 + <div class="code"><pre> 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 + + termCond : {c10 : Nat} → Cond + termCond {c10} env = Equal (vari env) c10 </pre></div> </div> </div> @@ -586,22 +716,22 @@ </li> <li><strong>≡-Reasoning</strong> は Agda での等式変形 <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span> lemma1 : {c10 : Nat} → Axiom (stmt1Cond {c10}) -<span class="line-numbers"> <a href="#n2" name="n2">2</a></span> (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) -<span class="line-numbers"> <a href="#n3" name="n3">3</a></span> lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in -<span class="line-numbers"> <a href="#n4" name="n4">4</a></span> begin -<span class="line-numbers"> <a href="#n5" name="n5">5</a></span> (Equal (varn env) c10 ) ∧ true -<span class="line-numbers"> <a href="#n6" name="n6">6</a></span> ≡⟨ ∧true ⟩ -<span class="line-numbers"> <a href="#n7" name="n7">7</a></span> Equal (varn env) c10 -<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> ≡⟨ cond ⟩ -<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> true -<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> ∎ ) -<span class="line-numbers"><a href="#n11" name="n11">11</a></span> -<span class="line-numbers"><a href="#n12" name="n12">12</a></span> stmt1Cond : {c10 : ℕ} → Cond -<span class="line-numbers"><a href="#n13" name="n13">13</a></span> stmt1Cond {c10} env = Equal (varn env) c10 -<span class="line-numbers"><a href="#n14" name="n14">14</a></span> -<span class="line-numbers"><a href="#n15" name="n15">15</a></span> stmt2Cond : {c10 : ℕ} → Cond -<span class="line-numbers"><a href="#n16" name="n16">16</a></span> stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) + <div class="code"><pre> 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 ⟩ + Equal (varn env) c10 + ≡⟨ 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) </pre></div> </div> </div> @@ -617,187 +747,6 @@ </ul> - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="agda-での-gears">Agda での Gears</h2> -<ul> - <li>Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数</li> - <li>CPS の関数は引数として継続を受け取って継続に計算結果を渡す</li> - <li><strong>名前 : 引数 → (Code : fa → t) → t</strong></li> - <li><strong>t</strong> は継続</li> - <li><strong>(Code : fa → t)</strong> は次の継続先</li> - <li>DataGear は Agda での CodeGear に使われる引数 - <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span>_-_ : {t : Set} → Nat → Nat → (Code : Nat → t) → t -<span class="line-numbers"><a href="#n2" name="n2">2</a></span>x - zero = (λ next → next x) -<span class="line-numbers"><a href="#n3" name="n3">3</a></span>zero - _ = (λ next → next zero) -<span class="line-numbers"><a href="#n4" name="n4">4</a></span>(suc x) - (suc y) = (x - y) -</pre></div> -</div> - </div> - </li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-をベースにした-hoarelogic-と証明全体">Gears をベースにした HoareLogic と証明(全体)</h2> -<ul> - <li>Gears をベースにした while Program - <ul> - <li>これは証明でもある</li> - </ul> - </li> - <li>whileループを任意の回数にするため<strong>c10</strong>は引数</li> - <li>whileTest’ の継続に conversion1、その継続に whileLoop’ が来て最後の継続に vari が c10 と等しい - <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> proofGears : {c10 : Nat } → Set -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) -</pre></div> -</div> - </div> - </li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-と-hoarelogic-をベースにした証明whiletest">Gears と HoareLogic をベースにした証明(whileTest)</h2> -<ul> - <li>ここは代入する Command</li> - <li>最初の Command なので PreCondition がない</li> - <li>もとの whileProgram では PComm を2回していたがまとめた</li> - <li>proof2は Post Condition が成り立つことの証明 - <ul> - <li><strong><em>/\</em></strong> は pi1 と pi2 のフィールドをもつレコード型</li> - <li>2つのものを引数に取り、両方が同時に成り立つことを示す</li> - </ul> - </li> - <li>Gears での PostCondition は <strong>引数 → (Code : fa → PostCondition → t) → t</strong> - <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> whileTest' : {l : Level} {t : Set l} → {c10 : Nat } → -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> (Code : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> whileTest' {_} {_} {c10} next = next env proof2 -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> where -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> env : Env -<span class="line-numbers"><a href="#n6" name="n6">6</a></span> env = record {vari = 0 ; varn = c10} -<span class="line-numbers"><a href="#n7" name="n7">7</a></span> proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) <-- PostCondition -<span class="line-numbers"><a href="#n8" name="n8">8</a></span> proof2 = record {pi1 = refl ; pi2 = refl} -</pre></div> -</div> - </div> - </li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-と-hoarelogic-をベースにした証明conversion">Gears と HoareLogic をベースにした証明(conversion)</h2> -<ul> - <li>conversion は Condition から LoopInvaliant への変換を行う CodeGear</li> - <li>proof4 は LoopInvaliant の証明</li> - <li>Gears での HoareLogic の完全な記述は <strong>引数 → PreCondition → (Code : fa → PostCondition → t) → t</strong> - <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"> <a href="#n1" name="n1">1</a></span> conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : Nat } → -<span class="line-numbers"> <a href="#n2" name="n2">2</a></span> ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -<span class="line-numbers"> <a href="#n3" name="n3">3</a></span> → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t -<span class="line-numbers"> <a href="#n4" name="n4">4</a></span> conversion1 env {c10} p1 next = next env proof4 -<span class="line-numbers"> <a href="#n5" name="n5">5</a></span> where -<span class="line-numbers"> <a href="#n6" name="n6">6</a></span> proof4 : varn env + vari env ≡ c10 -<span class="line-numbers"> <a href="#n7" name="n7">7</a></span> proof4 = let open ≡-Reasoning in -<span class="line-numbers"> <a href="#n8" name="n8">8</a></span> begin -<span class="line-numbers"> <a href="#n9" name="n9">9</a></span> varn env + vari env -<span class="line-numbers"><strong><a href="#n10" name="n10">10</a></strong></span> ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ -<span class="line-numbers"><a href="#n11" name="n11">11</a></span> c10 + vari env -<span class="line-numbers"><a href="#n12" name="n12">12</a></span> ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ -<span class="line-numbers"><a href="#n13" name="n13">13</a></span> c10 + 0 -<span class="line-numbers"><a href="#n14" name="n14">14</a></span> ≡⟨ +-sym {c10} {0} ⟩ -<span class="line-numbers"><a href="#n15" name="n15">15</a></span> c10 -<span class="line-numbers"><a href="#n16" name="n16">16</a></span> ∎ -</pre></div> -</div> - </div> - </li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-と-hoarelogic-をベースにした証明whileloop">Gears と HoareLogic をベースにした証明(whileLoop)</h2> -<ul> - <li>whileLoop は loopInvaliant が true の間 WhileLoop を回し続けるCodeGear</li> - <li>この CodeGear は Agda がループが終わることが証明できてないため <strong>{-# TERMINATING #-}</strong> で明示</li> - <li>false になると次の CodeGear へ - <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> {-# TERMINATING #-} -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> whileLoop env next with lt 0 (varn env) -<span class="line-numbers"><a href="#n4" name="n4">4</a></span> whileLoop env next | false = next env -<span class="line-numbers"><a href="#n5" name="n5">5</a></span> whileLoop env next | true = -<span class="line-numbers"><a href="#n6" name="n6">6</a></span> whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next -</pre></div> -</div> - </div> - </li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="gears-と-hoarelogic-をベースにした証明全体">Gears と HoareLogic をベースにした証明(全体)</h2> -<ul> - <li>最終状態で返ってくる i の値は c10 と一致する</li> - <li>これにより証明が可能 - <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre><span class="line-numbers"><a href="#n1" name="n1">1</a></span> proofGears : {c10 : Nat } → Set -<span class="line-numbers"><a href="#n2" name="n2">2</a></span> proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 -<span class="line-numbers"><a href="#n3" name="n3">3</a></span> (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) -</pre></div> -</div> - </div> - </li> -</ul> - - - -</div> - -<div class='slide'> - <!-- _S9SLIDE_ --> -<h2 id="まとめと今後の課題">まとめと今後の課題</h2> -<ul> - <li>HoareLogic の while を使った例題を作成、証明を行った</li> - <li>Gears を用いた HoareLogic ベースの検証方法を導入した - <ul> - <li>証明が引数として渡される記述のため証明とプログラムを一体化できた</li> - </ul> - </li> - <li>今後の課題 - <ul> - <li>RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで)</li> - </ul> - </li> -</ul> - </div>
--- a/slide/slide.md Tue Jan 15 16:52:28 2019 +0900 +++ b/slide/slide.md Tue Jan 15 17:47:18 2019 +0900 @@ -48,22 +48,33 @@ - Agda の文法については次のスライドから軽く説明する ## Agda での Gears の記述(whileLoop) -- Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数 -- CPS の関数は引数として継続を受け取って継続に計算結果を渡す +- Agda での CodeGear は継続渡し (CPS : Continuation Passing Style) で記述された関数 +- 継続渡しの関数は引数として継続を受け取って継続に計算結果を渡す - **名前 : 引数 → (Code : fa → t) → t** - **t** は継続 - **(Code : fa → t)** は次の継続先 - DataGear は Agda での CodeGear に使われる引数 ```AGDA - whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) → (Code : Env -> t) -> t - whileTest c10 next = next (record {varn = c10 ; vari = 0} ) +whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) + → (Code : Env -> t) -> t +whileTest c10 next = next (record {varn = c10 ; vari = 0} ) +``` - {-# TERMINATING #-} - 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 +## Agda での Gears の記述(whileLoop) +- 関数の動作を条件で変えたいときはパターンマッチを行う +- whileLoop は varn が 0 より大きい間ループする + - lt は Nat を2つ受け取って値の大小を比較 +```AGDA +{-# TERMINATING #-} +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 + +lt : Nat → Nat → Bool ``` ## Agda での DataGear @@ -71,18 +82,16 @@ - **データ型**と**レコード型**がある - データ型は一つのデータ ```AGDA - data Nat : Set where - zero : Nat - suc : Nat → Nat +data Nat : Set where + zero : Nat + suc : Nat → Nat ``` - レコード型は複数のデータをまとめる -- 構築時は**record レコード名 {フィールド名 = 値}** -- 複数ある場合は **record Env {varn = 1 ; varn = 2}**のように **;** を使って列挙 ```AGDA - record Env : Set where - field - varn : Nat - vari : Nat +record Env : Set where + field + varn : Nat + vari : Nat ``` ## Agda での証明 @@ -93,65 +102,73 @@ - 下のコードは Bool型の x と true の and を取ったものは x と等しいことの証明 - **refl** は **x == x** の左右の項が等しいことの証明 ```AGDA - ∧true : { x : Bool } → x ∧ true ≡ x - ∧true {x} with x - ∧true {x} | false = refl - ∧true {x} | true = refl +∧true : { x : Bool } → x ∧ true ≡ x +∧true {x} with x +∧true {x} | false = refl +∧true {x} | true = refl ``` ## Gears をベースにした HoareLogic と証明(全体) -- Gears をベースにした while Program - - これは証明でもある +- 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 )))) +proofGears : {c10 : Nat } → Set +proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 + (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) ``` ## Gears と HoareLogic をベースにした証明(whileTest) -- ここは代入する Command - 最初の Command なので PreCondition がない -- もとの whileProgram では PComm を2回していたがまとめた - proof2は Post Condition が成り立つことの証明 - **_/\\_** は pi1 と pi2 のフィールドをもつレコード型 - 2つのものを引数に取り、両方が同時に成り立つことを示す - 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} +whileTest' : {l : Level} {t : Set l} → {c10 : Nat } → + (Code : (env : Env) → + ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t +hileTest' {_} {_} {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 + - Condition の条件は Loop 内では厳しいのでゆるくする - 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 - ∎ +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 + ``` + +## Agdaでの証明(≡-Reasoning) +- Agda では証明の項を書き換える構文が用意されている +```AGDA + 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 をベースにした証明(全体) - 最終状態で返ってくる i の値は c10 と一致する - これにより証明が可能