Mercurial > hg > Papers > 2019 > ryokka-sigss
changeset 17:61117df82f51 default tip
fix
| author | ryokka |
|---|---|
| date | Wed, 16 Jan 2019 12:42:49 +0900 |
| parents | 07e1ccdfd844 |
| children | |
| files | Paper/tecrep.pdf ryokka-sigss.mm slide/Makefile slide/slide.html slide/slide.md |
| diffstat | 5 files changed, 155 insertions(+), 75 deletions(-) [+] |
line wrap: on
line diff
--- a/ryokka-sigss.mm Wed Jan 16 03:19:15 2019 +0900 +++ b/ryokka-sigss.mm Wed Jan 16 12:42:49 2019 +0900 @@ -1,8 +1,8 @@ <map version="1.1.0"> <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> <node CREATED="1542710800707" ID="ID_311099003" MODIFIED="1542710817736" TEXT="HoareLogic を用いた CbC の検証"> -<node CREATED="1542710937504" FOLDED="true" ID="ID_569346512" MODIFIED="1547296650006" POSITION="right" TEXT="目次"> -<node CREATED="1542710833654" ID="ID_422945004" MODIFIED="1542710848431" TEXT="研究目的"> +<node CREATED="1542710937504" ID="ID_569346512" MODIFIED="1547470706865" POSITION="right" TEXT="目次"> +<node CREATED="1542710833654" FOLDED="true" ID="ID_422945004" MODIFIED="1547470956607" TEXT="研究目的"> <node CREATED="1542712135796" ID="ID_1556598404" MODIFIED="1542712159908" TEXT="動作するプログラムは高い信頼性を持っていてほしい"/> <node CREATED="1542712161341" ID="ID_1089776093" MODIFIED="1542712318458" TEXT="そのため当研究室では CodeGear, DataGear という単位を用いて記述する手法を提案している"/> <node CREATED="1542712325826" ID="ID_1328437172" MODIFIED="1542713353200" TEXT="処理の単位である CodeGear を継続してプログラミングをする"/> @@ -10,7 +10,7 @@ <node CREATED="1544602583680" ID="ID_1768414893" MODIFIED="1544604155058" TEXT="継続渡しの記述と HoareLogic は相性良く記述ができるのではないかと考えている"/> <node CREATED="1544604130156" ID="ID_1466381113" MODIFIED="1544604233204" TEXT="本研究では Agda 上で 継続渡し記述と Hoare Logic を用いて SingleLinkedQueue に対して検証を行った(行いたい)"/> </node> -<node CREATED="1542710849360" ID="ID_1011962353" MODIFIED="1542710855151" TEXT="研究概要"> +<node CREATED="1542710849360" FOLDED="true" ID="ID_1011962353" MODIFIED="1547470963972" TEXT="研究概要"> <node CREATED="1544604865596" ID="ID_778442777" MODIFIED="1544605176196" TEXT="継続渡し記述をした Agda で、Hoare Logic を組み合わせての証明を行う"/> <node CREATED="1544604886373" ID="ID_742333345" MODIFIED="1544605273294" TEXT="通常は関数ごとの検証が厳しそう"> <node CREATED="1544605273841" ID="ID_1047842205" MODIFIED="1544605304755" TEXT="HoareLogic ベースだとそれぞれの関数ごとに検証ができそう"> @@ -24,7 +24,7 @@ <node CREATED="1544605471951" ID="ID_1170775991" MODIFIED="1544605484612" TEXT="ぱるすさんの修論あたりから拾ってくる"/> </node> </node> -<node CREATED="1542710861598" ID="ID_1569648968" MODIFIED="1544603739021" TEXT="Agda"> +<node CREATED="1542710861598" ID="ID_1569648968" MODIFIED="1547470946011" TEXT="Agda"> <node CREATED="1544603740555" ID="ID_1970865370" MODIFIED="1544603746306" TEXT="Agda について"> <node CREATED="1544604331911" ID="ID_1316542521" MODIFIED="1544604340263" TEXT="Agda とは?"/> <node CREATED="1544604340903" ID="ID_1025874674" MODIFIED="1544604470238" TEXT="Agda のデータ、文法記述"/> @@ -49,7 +49,7 @@ </node> </node> </node> -<node CREATED="1542710864438" ID="ID_1474492130" MODIFIED="1542710910000" TEXT="HoareLogic"> +<node CREATED="1542710864438" ID="ID_1474492130" MODIFIED="1547470948229" TEXT="HoareLogic"> <node CREATED="1544952943134" ID="ID_10179037" MODIFIED="1544952949971" TEXT="While Program"> <node CREATED="1544952991409" ID="ID_596599032" MODIFIED="1544952997567" TEXT="Skip"/> <node CREATED="1544952998071" ID="ID_1502092759" MODIFIED="1544953002143" TEXT="Abort"/>
--- a/slide/Makefile Wed Jan 16 03:19:15 2019 +0900 +++ b/slide/Makefile Wed Jan 16 12:42:49 2019 +0900 @@ -3,9 +3,9 @@ .SUFFIXES: .md .html .md.html: - 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 + slideshow b $< -t s6cr --h2; all: $(TARGET).html - open $(TARGET).html -a Google\ Chrome + open $(TARGET).html -a Google\ Chrome; clean: rm -f *.html
--- a/slide/slide.html Wed Jan 16 03:19:15 2019 +0900 +++ b/slide/slide.html Wed Jan 16 12:42:49 2019 +0900 @@ -78,7 +78,7 @@ <td> <div align="left"> 外間政尊 , 河野真治 - 琉球大学 : 並列信頼研究室 + - 琉球大学 : 並列信頼研究室 <hr style="color:#ffcc00;background-color:#ffcc00;text-align:left;border:none;width:100%;height:0.2em;"> </div> </td> @@ -102,7 +102,7 @@ <li>事前条件(Pre Condition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(Post Condition)を満たす</li> </ul> </li> - <li>OS の検証などで使われているが、実装の記述の他に関数型の記述が必要となる</li> + <li>OS の検証などで使われているが、実装の記述の他に実装に対応する証明が必要となる</li> <li>HoareLogic の単位である代入や、WhileLoop に対応する分解が煩雑</li> </ul> @@ -119,7 +119,7 @@ <li>この単位を用いて信頼性の高い OS として GearsOS を開発している</li> <li>Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する</li> <li>CodeGear は CbC により、C と同等の速度で実行可能かつ Agda の継続記述にもなっている</li> - <li>変換を必要とせずに HoareLogic による証明をメタ計算として記述できる</li> + <li>証明への変換を必要とせずに HoareLogic による証明をメタ計算として記述できるようになった</li> </ul> @@ -131,7 +131,7 @@ <h2 id="gears-について">Gears について</h2> <ul> <li><strong>Gears</strong> は当研究室で提案しているプログラム記述手法</li> - <li>計算の単位を <strong>CodeGear</strong> 、データの単位を <strong>DataGear</strong></li> + <li>処理の単位を <strong>CodeGear</strong> 、データの単位を <strong>DataGear</strong></li> <li>CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す</li> <li>Output の DataGear は次の CodeGear の Input として接続される <!-- [fig1](file://./fig/cgdg.pdf) --></li> @@ -158,8 +158,8 @@ <li>データ型は一つのデータ <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> <div class="code"><pre>data Nat : Set where -zero : Nat -suc : Nat → Nat + zero : Nat + suc : Nat → Nat </pre></div> </div> </div> @@ -167,9 +167,9 @@ <li>レコード型は複数のデータをまとめる <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> <div class="code"><pre>record Env : Set where -field - varn : Nat - vari : Nat + field + varn : Nat + vari : Nat </pre></div> </div> </div> @@ -187,14 +187,14 @@ <li>Agda での CodeGear は継続渡し (CPS : Continuation Passing Style) で記述された関数</li> <li><strong>{}</strong> は暗黙的(推論される)</li> <li>継続渡しの関数は引数として継続を受け取って継続に計算結果を渡す</li> - <li>CodeGear の型は<strong>名前 : 引数 → (Code : fa → t) → t</strong></li> + <li>CodeGear の型は<strong>引数 → (Code : fa → t) → t</strong></li> <li><strong>t</strong> は継続(最終的に返すもの)</li> <li><strong>(Code : fa → t)</strong> は次の継続先 <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> <div class="code"><pre>whileTest : {t : Set} → (c10 : Nat) - → (Code : Env → t) → t + → (Code : Env → t) → t whileTest c10 next = next (record {varn = c10 - ; vari = 0} ) + ; vari = 0} ) </pre></div> </div> </div> @@ -242,10 +242,12 @@ <!-- _S9SLIDE_ --> <h2 id="agda-での証明">Agda での証明</h2> <ul> - <li>証明の見た目関数と同じ</li> - <li>関数との違いは<strong>型が証明すべき論理式</strong>で<strong>関数自体がそれを満たす導出</strong></li> - <li><strong>refl</strong> は <strong>x == x</strong> で左右の項が等しいことの証明</li> - <li>変換で使っている <strong>cong</strong> は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明</li> + <li>関数との違いは<strong>型が証明すべき論理式</strong>で<strong>関数自体がそれを満たす導出</strong> + <ul> + <li><strong>refl</strong> は <strong>x == x</strong> で左右の項が等しいことの証明</li> + <li><strong>cong</strong> は 関数と x ≡ y 受け取って、x ≡ y の両辺に関数を適応しても等しいことが変わらないことの証明</li> + </ul> + </li> <li><strong>+zero</strong> は任意の自然数の右から zero を足しても元の数と等しいことの証明 <ul> <li><strong>y = zero</strong> のときは <strong>zero ≡ zero</strong> のため refl</li> @@ -334,8 +336,8 @@ <li>証明の例で使用した<strong>+zero</strong>は<strong>y + zero ≡ y</strong></li> <li>これを使いたいが今回は<strong>y + zero ≡ y</strong></li> <li>Agda の StandartLibrary にある sym を用いて <strong>+zero</strong> を <strong>y + zero ≡ y</strong> として適応することで証明ができる -```AGDA -– +zero : { y : Nat } → y + zero ≡ y + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre>-- +zero : { y : Nat } → y + zero ≡ y +-sym {zero} {suc y} = let open ≡-Reasoning in begin zero + suc y @@ -343,29 +345,43 @@ suc y ≡⟨ sym +zero ⟩ suc y + zero - ∎</li> + ∎ +sym : Symmetric {A = A} _≡_ +sym refl = refl +</pre></div> +</div> + </div> + </li> </ul> -<p>sym : Symmetric {A = A} <em>≡</em> -sym refl = refl</p> -<pre><code> -## HoareLogicをベースとした Gears での検証手法 -- 今回 HoareLogic で証明する例の疑似コードを用意した -- このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす -- n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になるはずである。 -```C - n = 10; - i = 0; -</code></pre> -<div class="language-c highlighter-coderay"><div class="CodeRay"> - <div class="code"><pre> <span style="color:#080;font-weight:bold">while</span> (n><span style="color:#00D">0</span>) - { - i++; - n--; - } + + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="hoarelogicをベースとした-gears-での検証手法">HoareLogicをベースとした Gears での検証手法</h2> +<ul> + <li>今回 HoareLogic で証明する次のようなコードを検証した</li> + <li>このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす</li> + <li>n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になるはずである。 + <div class="language-C highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre> n = <span style="color:#00D">10</span>; + i = <span style="color:#00D">0</span>; </pre></div> </div> + </div> + <div class="language-c highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre> <span style="color:#080;font-weight:bold">while</span> (n><span style="color:#00D">0</span>) + { + i++; + n--; + } +</pre></div> </div> + </div> + </li> +</ul> @@ -441,14 +457,14 @@ <li>proof2は Post Condition が成り立つことの証明 <ul> <li><strong><em>/\</em></strong> は pi1 と pi2 のフィールドをもつレコード型</li> - <li>２つのものを引数に取り、両方が同時に成り立つことを表している</li> + <li>これは２つのものを引数に取り、両方が同時に成り立つことを表している</li> <li><strong>refl</strong> は <strong>x == x</strong> で左右の項が等しいことの証明</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 : {t : Set} → (c10 : Nat) → (Code : Env → t) → t -whileTest' : {l : Level} {t : Set l} → {c10 : Nat } → +whileTest' : {t : Set} → {c10 : Nat } → (Code : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t whileTest' {_} {_} {c10} next = next env proof2 @@ -479,7 +495,7 @@ <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>conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : Nat } → + <div class="code"><pre>conversion1 : {t : Set} → (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 @@ -552,7 +568,7 @@ <h2 id="gears-と-hoarelogic-をベースにした証明全体">Gears と HoareLogic をベースにした証明(全体)</h2> <ul> <li>最終状態で返ってくる i の値は c10 と一致する</li> - <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 @@ -589,12 +605,53 @@ <div class='slide'> <!-- _S9SLIDE_ --> -<h2 id="発表終了">発表終了</h2> +<h2 id="agda-上での-hoarelogic-記述">Agda 上での HoareLogic 記述</h2> <ul> - <li>ご清聴ありがとうございました。</li> + <li>Agda で構築した HoareLogic での whileProgram と Gears での whileProgram を見た目で比較</li> + <li>この他に証明にコマンド、コマンドの証明の定義を記述する必要がある + <div class="language-AGDA highlighter-coderay"><div class="CodeRay"> + <div class="code"><pre>-- HoareLogic でのwhileProgram +program : ℕ → Comm +program c10 = + Seq ( PComm (λ env → record env {varn = c10})) + $ 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)} )) +-- コマンドの証明部分 +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 +</pre></div> +</div> + </div> + </li> </ul> + +</div> + +<div class='slide'> + <!-- _S9SLIDE_ --> +<h2 id="gears-での-hoarelogic-記述">Gears での HoareLogic 記述</h2> +<ul> + <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>
--- a/slide/slide.md Wed Jan 16 03:19:15 2019 +0900 +++ b/slide/slide.md Wed Jan 16 12:42:49 2019 +0900 @@ -1,6 +1,6 @@ title: GearsOS の Hoare Logic を用いた検証 author: 外間政尊 , 河野真治 -profile: 琉球大学 : 並列信頼研究室 +profile: - 琉球大学 : 並列信頼研究室 lang: Japanese <!-- 発表20分、質疑応答5分 --> @@ -10,7 +10,7 @@ - 信頼性を上げるために仕様を検証する必要 - 仕様検証の手法として Floyd-Hoare Logic (以下 HoareLogic) がある - 事前条件(Pre Condition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(Post Condition)を満たす -- OS の検証などで使われているが、実装の記述の他に関数型の記述が必要となる +- OS の検証などで使われているが、実装の記述の他に実装に対応する証明が必要となる - HoareLogic の単位である代入や、WhileLoop に対応する分解が煩雑 ## GearsOS によるメタ計算としての HoareLogic の導入 @@ -19,12 +19,12 @@ - この単位を用いて信頼性の高い OS として GearsOS を開発している - Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する - CodeGear は CbC により、C と同等の速度で実行可能かつ Agda の継続記述にもなっている -- 変換を必要とせずに HoareLogic による証明をメタ計算として記述できる +- 証明への変換を必要とせずに HoareLogic による証明をメタ計算として記述できるようになった ## Gears について - **Gears** は当研究室で提案しているプログラム記述手法 -- 計算の単位を **CodeGear** 、データの単位を **DataGear** +- 処理の単位を **CodeGear** 、データの単位を **DataGear** - CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す - Output の DataGear は次の CodeGear の Input として接続される <!-- [fig1](file://./fig/cgdg.pdf) --> @@ -34,37 +34,35 @@ <!-- {} --> <!-- <p style="text-align:center;"><img src="./pic/cgdg.svg" alt="" width="30%" height="30%"/></p> --> - ## Agda での DataGear - **DataGear** は CodeGear でつかわれる引数 - **データ型**と**レコード型**がある - データ型は一つのデータ ```AGDA data Nat : Set where - zero : Nat - suc : Nat → Nat + zero : Nat + suc : Nat → Nat ``` - レコード型は複数のデータをまとめる ```AGDA record Env : Set where - field - varn : Nat - vari : Nat + field + varn : Nat + vari : Nat ``` - ## Agda での Gears の記述(whileTest) - Agda での CodeGear は継続渡し (CPS : Continuation Passing Style) で記述された関数 - **{}** は暗黙的(推論される) - 継続渡しの関数は引数として継続を受け取って継続に計算結果を渡す -- CodeGear の型は**名前 : 引数 → (Code : fa → t) → t** +- CodeGear の型は**引数 → (Code : fa → t) → t** - **t** は継続(最終的に返すもの) - **(Code : fa → t)** は次の継続先 ```AGDA whileTest : {t : Set} → (c10 : Nat) - → (Code : Env → t) → t + → (Code : Env → t) → t whileTest c10 next = next (record {varn = c10 - ; vari = 0} ) + ; vari = 0} ) ``` ## Agda での Gears の記述(whileLoop) @@ -88,10 +86,9 @@ ``` ## Agda での証明 -- 証明の見た目関数と同じ - 関数との違いは**型が証明すべき論理式**で**関数自体がそれを満たす導出** -- **refl** は **x == x** で左右の項が等しいことの証明 -- 変換で使っている **cong** は 関数と x ≡ y 受け取って両辺に関数を適応しても等しいことが変わらないことの証明 + - **refl** は **x == x** で左右の項が等しいことの証明 + - **cong** は 関数と x ≡ y 受け取って、x ≡ y の両辺に関数を適応しても等しいことが変わらないことの証明 - **+zero** は任意の自然数の右から zero を足しても元の数と等しいことの証明 - **y = zero** のときは **zero ≡ zero** のため refl - **y = suc y** のときは cong を使い y の数を減らして再帰的に**+zero**を行っている @@ -154,13 +151,12 @@ ≡⟨ sym +zero ⟩ suc y + zero ∎ - sym : Symmetric {A = A} _≡_ sym refl = refl ``` ## HoareLogicをベースとした Gears での検証手法 -- 今回 HoareLogic で証明する例の疑似コードを用意した +- 今回 HoareLogic で証明する次のようなコードを検証した - このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす - n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になるはずである。 ```C @@ -209,12 +205,12 @@ - 最初の Command なので PreCondition がない - proof2は Post Condition が成り立つことの証明 - **_/\\_** は pi1 と pi2 のフィールドをもつレコード型 - - ２つのものを引数に取り、両方が同時に成り立つことを表している + - これは２つのものを引数に取り、両方が同時に成り立つことを表している - **refl** は **x == x** で左右の項が等しいことの証明 - Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t** ```AGDA -- whileTest : {t : Set} → (c10 : Nat) → (Code : Env → t) → t -whileTest' : {l : Level} {t : Set l} → {c10 : Nat } → +whileTest' : {t : Set} → {c10 : Nat } → (Code : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t whileTest' {_} {_} {c10} next = next env proof2 @@ -231,7 +227,7 @@ - proof4 は LoopInvaliant の証明 - Gears での HoareLogic の完全な記述は **引数 → PreCondition → (Code : fa → PostCondition → t) → t** ```AGDA -conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : Nat } → +conversion1 : {t : Set} → (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 @@ -260,7 +256,7 @@ c10 ∎ -- +-sym : { x y : Nat } → x + y ≡ y + x -``` +``` ## Gears と HoareLogic をベースにした証明(whileLoop) - whileLoop も whileTest と同様に PreCondition が CodeGear に入りそれに対する証明が記述されている @@ -271,7 +267,7 @@ ## Gears と HoareLogic をベースにした証明(全体) - 最終状態で返ってくる i の値は c10 と一致する -- これにより証明が可能 +- これにより証明が完了 ```AGDA proofGears : {c10 : Nat } → Set proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 @@ -284,6 +280,33 @@ - 今後の課題 - RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで) -## 発表終了 -- ご清聴ありがとうございました。 +## Agda 上での HoareLogic 記述 +- Agda で構築した HoareLogic での whileProgram と Gears での whileProgram を見た目で比較 +- この他に証明にコマンド、コマンドの証明の定義を記述する必要がある +```AGDA +-- HoareLogic でのwhileProgram +program : ℕ → Comm +program c10 = + Seq ( PComm (λ env → record env {varn = c10})) + $ 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)} )) +-- コマンドの証明部分 +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 +``` +## Gears での HoareLogic 記述 +- +```AGDA + proofGears : {c10 : Nat } → Set + proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 + (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) +```