Mercurial > hg > Papers > 2018 > ryokka-thesis
changeset 13:b7106f1dcc38
fix slide
| author | ryokka |
|---|---|
| date | Wed, 21 Feb 2018 15:27:37 +0900 |
| parents | 8c205db691d4 |
| children | 5d7eb0f27fb0 |
| files | final_main/chapter2.tex final_main/chapter4.tex final_main/chapter5.tex final_main/main.pdf slide/slide.html slide/slide.md |
| diffstat | 6 files changed, 287 insertions(+), 216 deletions(-) [+] |
line wrap: on
line diff
--- a/final_main/chapter2.tex Wed Feb 21 13:14:18 2018 +0900 +++ b/final_main/chapter2.tex Wed Feb 21 15:27:37 2018 +0900 @@ -182,7 +182,7 @@ る。 CodeGear 、 DataGear にはそれぞれメタレベルとして、 Meta CodeGear 、 Meta DataGear が存在する。 -CbC で実装していると、stub CodeGear の記述が煩雑になることが分かった。 +CbC で実装していくうちに、stub CodeGear の記述が煩雑になることが分かった。 そのため 既存の実装を モジュールとして扱うため Interface という仕組みを導入した。 Interface は DataGear に対して何らかの操作(API)を行う CodeGear とその
--- a/final_main/chapter4.tex Wed Feb 21 13:14:18 2018 +0900 +++ b/final_main/chapter4.tex Wed Feb 21 15:27:37 2018 +0900 @@ -116,8 +116,8 @@ 実際に使われる Stack の操作は StackMethods にある push や popである。この push や pop は SingleLinkedStack で実装されている。 -\lstinputlisting[label=src:agda-single-linked-stack, caption=Agda における Stack -の実装] {src/AgdaSingleLinkedStack.agda.replaced} +% \lstinputlisting[label=src:agda-single-linked-stack, caption=Agda における Stack +% の実装] {src/AgdaSingleLinkedStack.agda.replaced} \lstinputlisting[label=src:agda-interface, caption=Agda における Interface の定義] {src/AgdaInterface.agda.replaced}
--- a/final_main/chapter5.tex Wed Feb 21 13:14:18 2018 +0900 +++ b/final_main/chapter5.tex Wed Feb 21 15:27:37 2018 +0900 @@ -78,16 +78,18 @@ \lstinputlisting[label=src:agda-tree-proof, caption=Tree Interface の証 明]{src/AgdaTreeProof.agda.replaced} -この Tree の証明では、不定状態の redBlackInSomeState 型を作成し、その状態の Tree +この Tree の証明では、不定状態の Tree を redBlackInSomeState で作成し、その状態の Tree に一つ Node を Put し、その Node を Get することができるかを証明しようとしたもの である。 + しかし、この証明は Node を取得する際に Put した Node が存在するか、 Get した -Node が存在するのか、 Get した Node と Put した Node が合同なのか等の様々な補 -題を証明し、全てが成り立つ必要がある。今回この証明では Put した Node と Get した +Node が存在するのか、などの条件や、 Get した Node と Put した Node が合同なのか、 +key の値が等しい場合の eq は合同と同義であるのか等の様々な補題を証明する必要が +あった。今回この証明では Put した Node と Get した Node が合同であることを記述しようとしていたがそれまでの計算が異なるため完全に合 同であることを示すことが困難であった。 -そのため、今後の研究では\ref{hoare-logic} で説明する Hoare Logic を元に証明を +今後の研究では\ref{hoare-logic} で説明する Hoare Logic を元に証明を 行おうと考えている。 \section{Hoare Logic} @@ -109,8 +111,9 @@ このとき、後状態から前状態を推論することができればそのプログラムは部分的に正しい 動きをすることを証明することができる。 + この Hoare Logic の前状態、処理、後状態を CodeGear、 input/output の DataGear が表 -\ref{fig:cbc-hoare} のように表せると考えている。 +\ref{fig:cbc-hoare} のように表せるのではないか考えている。 \begin{figure}[htpb] \begin{center}
--- a/slide/slide.html Wed Feb 21 13:14:18 2018 +0900 +++ b/slide/slide.html Wed Feb 21 15:27:37 2018 +0900 @@ -86,88 +86,67 @@ <!-- === begin markdown block === generated by markdown/1.2.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16] - on 2018-02-21 13:00:30 +0900 with Markdown engine kramdown (1.15.0) + on 2018-02-21 15:26:02 +0900 with Markdown engine kramdown (1.15.0) using options {} --> <!-- _S9SLIDE_ --> -<h2 id="section">ソフトウェアの信頼性の保証</h2> - +<h2 id="section">プログラムの信頼性の保証</h2> <ul> - <li> - <p>動作するプログラムの信頼性を保証したい</p> - </li> - <li> - <p>そのために当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している</p> + <li>動作するプログラムの信頼性を保証したい</li> + <li>プログラムの仕様を検証するには<strong>モデル検査</strong>と<strong>定理証明</strong>の２つの手法がある + <ul> + <li>モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認する</li> + <li>定理証明 はプログラムの性質を論理式で記述しそれが常に正しいことを証明する</li> + </ul> </li> - <li> - <p>処理の単位である CodeGear はメタ計算によって接続され、メタ計算部分を切り替えることで CodeGear に一切の変更なくプログラムの性質を検証することができる</p> - </li> - <li> - <p>本研究では CodeGear 、 DataGear を用いて記述する言語、 Continuation based C (CbC) を用いてプログラムを記述し、それを証明することで信頼性を上げることを目標としている</p> - </li> - <li> - <p>CbC での記述を Agda にマッピングし、その性質の一部を証明した</p> - </li> + <li>また、当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している</li> </ul> +<!-- * 処理の単位である CodeGear はメタ計算によって接続され、メタ計算部分を切り替えることで CodeGear に一切の変更なくプログラムの性質を検証することができる --> + +<!-- * 本研究では CodeGear 、 DataGear を用いて記述する言語、 Continuation based C (CbC) を用いてプログラムを記述し、それを証明することで信頼性を上げることを目標としている --> + +<!-- * CbC での記述を Agda にマッピングし、その性質の一部を証明した --> + </div> <div class='slide '> <!-- _S9SLIDE_ --> <h2 id="codegear--datagear">CodeGear と DataGear</h2> +<ul> + <li>CodeGear とはプログラムを記述する際の処理の単位である。</li> + <li>DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。</li> + <li>CodeGear はメタ計算によって CodeGear へ接続される</li> + <li>接続はメタ計算で行われ、メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる</li> + <li>CodeGear は入力として DataGear を受け取り、 DataGear に変更を加えて次に指定された CodeGear へ継続する</li> +</ul> -<ul> - <li> - <p>CodeGear とはプログラムを記述する際の処理の単位である。</p> - </li> - <li> - <p>DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。</p> - </li> - <li> - <p>CodeGear はメタ計算によって CodeGear へ接続される</p> - </li> - <li> - <p>CodeGear は入力として DataGear を受け取り、 DataGear に変更を加えて次に指定された CodeGear へ継続する。</p> - </li> -</ul> +<div style="text-align: center;"> + <img src="./fig/csds.svg" alt="goto" width="800" /> +</div> </div> <div class='slide '> <!-- _S9SLIDE_ --> <h2 id="continuation-based-c-cbc">Continuation based C (CbC)</h2> - <ul> - <li> - <p>当研究室で開発している言語</p> - </li> - <li> - <p>基本的な構文は C 言語と同じ</p> - </li> - <li> - <p>CodeGear、 DataGear という単位を用いてプログラムを記述する</p> - </li> - <li> - <p>CbC では 通常計算とメタ計算を分離している</p> - </li> - <li> - <p>CodeGear を継続し、 DataGear を変更しながらプログラムが進んでいく</p> - </li> - <li> - <p>CodeGear は関数の定義前に__codeがつき、関数末尾で継続である goto により次の CodeGear が指定される</p> - </li> - <li> - <p>DataGear はレコードで定義する</p> - </li> + <li>当研究室で開発している言語</li> + <li>基本的な構文は C 言語と同じ</li> + <li>CodeGear、 DataGear という単位を用いてプログラムを記述する</li> + <li>CbC では 通常計算とメタ計算を分離している</li> + <li>CodeGear を継続し、 DataGear を変更しながらプログラムが進んでいく</li> + <li>CodeGear は関数の定義前に__codeがつく</li> + <li>関数末尾の goto により次の CodeGear に継続する</li> </ul> -<pre lang="C"><code>__code cs0(int a, int b){ - goto cs1(a+b); +<pre lang="C"><code>__code cg0(int a, int b){ + goto cg1(a+b); } -__code cs1(int c){ - goto cs2(c); +__code cg1(int c){ + goto cg2(c); } </code></pre> @@ -176,12 +155,12 @@ <div class='slide '> <!-- _S9SLIDE_ --> <h2 id="context">Context</h2> - <ul> <li>CodeGear や DataGear をリストとして、 Context と呼ばれる Meta DataGear の中で定義している</li> <li>しかし Context は Meta DataGear のため、通常レベルである CodeGear で直接扱うのは避けたい</li> <li>その為、 stub CodeGear という Meta CodeGear を定義している。</li> - <li>現段階で複雑でない stub CodeGear はスクリプトを使って自動生成している</li> + <li>stub CodeGear は Context を通して必要なデータを取り出し、次の CodeGear に接続する</li> + <li>stub CodeGear は CodeGear 毎に生成される</li> </ul> @@ -189,7 +168,6 @@ <div class='slide '> <!-- _S9SLIDE_ --> <h2 id="interface">Interface</h2> - <ul> <li>CbC で実装していくにつれて stub CodeGear の記述が煩雑になることがわかった</li> <li>そこで Interface というモジュール化の仕組みを導入した</li> @@ -216,15 +194,10 @@ </div> <div class='slide '> <!-- _S9SLIDE_ --> -<h2 id="interface-">Interface の実装</h2> - +<h2 id="interface-1">Interface</h2> <ul> - <li> - <p>Interface を表す DataGear は次のような関数で生成される</p> - </li> - <li> - <p><strong>stack->push</strong> のようにしてコード中で使うことができる</p> - </li> + <li>Interface を表す DataGear は次のような関数で生成される</li> + <li><strong>stack->push</strong> のようにしてコード中で使うことができる</li> </ul> <pre lang="C"><code>Stack* createSingleLinkedStack(struct Context* context) { @@ -243,41 +216,86 @@ <div class='slide '> <!-- _S9SLIDE_ --> <h2 id="agda">Agda</h2> - <ul> - <li> - <p>Agda とは定理証明支援器で、型システムを用いて証明を記述できる。</p> - </li> - <li> - <p>Agda 上で CodeGear、 DataGear の単位と継続を定義した</p> - </li> + <li>Agda とは定理証明支援器で、型システムを用いて証明を記述できる。</li> + <li>Agda では関数の型を明示する必要がある</li> +</ul> + +<pre lang="AGDA"><code>-- Booleanの定義(データの定義例) +data Bool : Set where + true : Bool + false : Bool + +-- Bool値を反転する関数の例 +not : Bool → Bool +not true = false +not false = true + +-- xor(複数の引数を取る例) +xor : Bool → Bool → Bool +xor true true = false +xor false false = false +xor _ _ = true +</code></pre> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h2 id="agda-1">AGDA</h2> +<ul> + <li>Agda 上で CodeGear、 DataGear の単位と継続を定義した</li> + <li>DataGear はレコード型として定義し、 CodeGear は通常の関数。</li> </ul> -<!-- AgdaのInterface の例 --> +<pre lang="AGDA"><code>// CbC +__code cg0(int a, int b){ + goto cg1(a+b); +} + +</code></pre> +<pre><code>-- agda DataGear +record dg0 : Set where + field + a : Int + b : Int + +-- agda CodeGear define +data CodeGear (A B : Set) : Set where + cg : (A -> B) -> CodeGear A B + +-- agda CodeGear example +cg0 : CodeGear dg0 dg1 +cg0 = cg (\d -> goto cg1 (record {c = (dg0.a d) + (dg0.b d)})) +</code></pre> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> +<h2 id="agda-">Agda での証明</h2> +<ul> + <li>型で論理を書き、関数部分で導出</li> +</ul> + +<pre lang="AGDA"><code>ex : 1 + 2 ≡ 3 +ex = refl +</code></pre> </div> <div class='slide '> <!-- _S9SLIDE_ --> <h2 id="agda--interface-">Agda での Interface の定義</h2> - <ul> - <li> - <p>Agda上でも CbC の Interface と同様のものを定義した。</p> - </li> - <li> - <p>定義部分</p> - </li> + <li>Agda上でも CbC の Interface と同様のものを定義した。</li> </ul> <pre lang="AGDA"><code>record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where field push : stackImpl -> a -> (stackImpl -> t) -> t pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t - pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t - get : stackImpl -> (stackImpl -> Maybe a -> t) -> t - get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t - clear : stackImpl -> (stackImpl -> t) -> t + -- 省略 open StackMethods record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where @@ -288,28 +306,49 @@ pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) popStack : (Stack a si -> Maybe a -> t) -> t popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - pop2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t - pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) - getStack : (Stack a si -> Maybe a -> t) -> t - getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - get2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t - get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) - clearStack : (Stack a si -> t) -> t - clearStack next = clear (stackMethods ) (stack ) (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) + -- 省略 +</code></pre> +<ul lang="AGDA"> + <li>インスタンス生成</li> +</ul> +<pre><code>singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a) +singleLinkedStackSpec = record { + push = pushSingleLinkedStack + ; pop = popSingleLinkedStack + -- 省略 + } + +createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a) +createSingleLinkedStack = record { + stack = emptySingleLinkedStack ; + stackMethods = singleLinkedStackSpec + } </code></pre> -<ul> - <li>Interface部分</li> -</ul> +<!-- ## Tree の Interface --> +<!-- ```AGDA --> +<!-- record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where --> +<!-- field --> +<!-- putImpl : treeImpl -> a -> (treeImpl -> t) -> t --> +<!-- getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t --> +<!-- open TreeMethods --> -</div> -<div class='slide '> -<!-- _S9SLIDE_ --> -<h2 id="tree--interface">Tree の Interface</h2> +<!-- record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where --> +<!-- field --> +<!-- tree : treeImpl --> +<!-- treeMethods : TreeMethods {n} {m} {a} {t} treeImpl --> +<!-- putTree : a -> (Tree treeImpl -> t) -> t --> +<!-- putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} )) --> +<!-- getTree : (Tree treeImpl -> Maybe a -> t) -> t --> +<!-- getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d ) --> +<!-- ``` --> -<pre lang="AGDA"><code> -</code></pre> +<!-- * インスタンス生成 --> + +<!-- ```AGDA --> + +<!-- ``` --> </div> @@ -332,33 +371,21 @@ push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl } </code></pre> +<!-- ## Agda での Interface の部分的な証明と課題(Tree の例) --> -</div> -<div class='slide '> -<!-- _S9SLIDE_ --> -<h2 id="agda--interface-tree-">Agda での Interface の部分的な証明と課題(Tree の例)</h2> +<!-- ```AGDA --> -<!-- なんでだめなのかがうまく説明できないかも… --> - -<pre lang="AGDA"><code> -</code></pre> +<!-- ``` --> </div> <div class='slide '> <!-- _S9SLIDE_ --> <h2 id="hoare-logic">Hoare Logic</h2> - <ul> - <li> - <p>Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証するための手法</p> - </li> - <li> - <p>前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) によって変更する</p> - </li> - <li> - <p>この {P} C {Q} でプログラムを部分的に表すことができる</p> - </li> + <li>Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証するための手法</li> + <li>前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) によって変更する</li> + <li>この {P} C {Q} でプログラムを部分的に表すことができるp</li> </ul> <div style="text-align: center;"> @@ -376,7 +403,7 @@ </ul> <div style="text-align: center;"> - <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="600" /> + <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="800" /> </div> @@ -384,20 +411,11 @@ <div class='slide '> <!-- _S9SLIDE_ --> <h2 id="section-1">今後の課題</h2> - <ul> - <li> - <p>本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。</p> - </li> - <li> - <p>これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。</p> - </li> - <li> - <p>また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。</p> - </li> - <li> - <p>今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。</p> - </li> + <li>本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。</li> + <li>これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。</li> + <li>また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。</li> + <li>今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。</li> </ul> <!-- === end markdown block === --> </div>
--- a/slide/slide.md Wed Feb 21 13:14:18 2018 +0900 +++ b/slide/slide.md Wed Feb 21 15:27:37 2018 +0900 @@ -5,66 +5,60 @@ code-engine: coderay -## ソフトウェアの信頼性の保証 - +## プログラムの信頼性の保証 * 動作するプログラムの信頼性を保証したい - -* そのために当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している +* プログラムの仕様を検証するには**モデル検査**と**定理証明**の２つの手法がある + * モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認する + * 定理証明 はプログラムの性質を論理式で記述しそれが常に正しいことを証明する +* また、当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している -* 処理の単位である CodeGear はメタ計算によって接続され、メタ計算部分を切り替えることで CodeGear に一切の変更なくプログラムの性質を検証することができる +<!-- * 処理の単位である CodeGear はメタ計算によって接続され、メタ計算部分を切り替えることで CodeGear に一切の変更なくプログラムの性質を検証することができる --> -* 本研究では CodeGear 、 DataGear を用いて記述する言語、 Continuation based C (CbC) を用いてプログラムを記述し、それを証明することで信頼性を上げることを目標としている +<!-- * 本研究では CodeGear 、 DataGear を用いて記述する言語、 Continuation based C (CbC) を用いてプログラムを記述し、それを証明することで信頼性を上げることを目標としている --> -* CbC での記述を Agda にマッピングし、その性質の一部を証明した +<!-- * CbC での記述を Agda にマッピングし、その性質の一部を証明した --> ## CodeGear と DataGear - * CodeGear とはプログラムを記述する際の処理の単位である。 - * DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。 +* CodeGear はメタ計算によって CodeGear へ接続される +* 接続はメタ計算で行われ、メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる +* CodeGear は入力として DataGear を受け取り、 DataGear に変更を加えて次に指定された CodeGear へ継続する -* CodeGear はメタ計算によって CodeGear へ接続される - -* CodeGear は入力として DataGear を受け取り、 DataGear に変更を加えて次に指定された CodeGear へ継続する。 - +<div style="text-align: center;"> + <img src="./fig/csds.svg" alt="goto" width="800"> +</div> ## Continuation based C (CbC) - * 当研究室で開発している言語 - * 基本的な構文は C 言語と同じ - * CodeGear、 DataGear という単位を用いてプログラムを記述する +* CbC では 通常計算とメタ計算を分離している +* CodeGear を継続し、 DataGear を変更しながらプログラムが進んでいく +* CodeGear は関数の定義前に__codeがつく +* 関数末尾の goto により次の CodeGear に継続する -* CbC では 通常計算とメタ計算を分離している - -* CodeGear を継続し、 DataGear を変更しながらプログラムが進んでいく - -* CodeGear は関数の定義前に__codeがつき、関数末尾で継続である goto により次の CodeGear が指定される - -* DataGear はレコードで定義する ```C -__code cs0(int a, int b){ - goto cs1(a+b); +__code cg0(int a, int b){ + goto cg1(a+b); } -__code cs1(int c){ - goto cs2(c); +__code cg1(int c){ + goto cg2(c); } ``` ## Context - * CodeGear や DataGear をリストとして、 Context と呼ばれる Meta DataGear の中で定義している * しかし Context は Meta DataGear のため、通常レベルである CodeGear で直接扱うのは避けたい * その為、 stub CodeGear という Meta CodeGear を定義している。 -* 現段階で複雑でない stub CodeGear はスクリプトを使って自動生成している +* stub CodeGear は Context を通して必要なデータを取り出し、次の CodeGear に接続する +* stub CodeGear は CodeGear 毎に生成される ## Interface - * CbC で実装していくにつれて stub CodeGear の記述が煩雑になることがわかった * そこで Interface というモジュール化の仕組みを導入した * Interface は CodeGear とそこで扱われている DataGear の集合を抽象的に表現した Meta DataGear として定義されている @@ -86,11 +80,9 @@ } Stack; ``` -## Interface の実装 - +## Interface * Interface を表す DataGear は次のような関数で生成される - -* **stack->push** のようにしてコード中で使うことができる +* **stack->push** のようにしてコード中で使うことができる ```C Stack* createSingleLinkedStack(struct Context* context) { @@ -104,32 +96,73 @@ return stack; ``` +## Agda +* Agda とは定理証明支援器で、型システムを用いて証明を記述できる。 +* Agda では関数の型を明示する必要がある -## Agda +```AGDA +-- Booleanの定義(データの定義例) +data Bool : Set where + true : Bool + false : Bool + +-- Bool値を反転する関数の例 +not : Bool → Bool +not true = false +not false = true + +-- xor(複数の引数を取る例) +xor : Bool → Bool → Bool +xor true true = false +xor false false = false +xor _ _ = true +``` + +## AGDA +* Agda 上で CodeGear、 DataGear の単位と継続を定義した +* DataGear はレコード型として定義し、 CodeGear は通常の関数。 -* Agda とは定理証明支援器で、型システムを用いて証明を記述できる。 +```C +// CbC +__code cg0(int a, int b){ + goto cg1(a+b); +} + +``` +```AGDA +-- agda DataGear +record dg0 : Set where + field + a : Int + b : Int -* Agda 上で CodeGear、 DataGear の単位と継続を定義した +-- agda CodeGear define +data CodeGear (A B : Set) : Set where + cg : (A -> B) -> CodeGear A B + +-- agda CodeGear example +cg0 : CodeGear dg0 dg1 +cg0 = cg (\d -> goto cg1 (record {c = (dg0.a d) + (dg0.b d)})) +``` + +## Agda での証明 +* 型で論理を書き、関数部分で導出 + +```AGDA +ex : 1 + 2 ≡ 3 +ex = refl +``` - -<!-- AgdaのInterface の例 --> - ## Agda での Interface の定義 - * Agda上でも CbC の Interface と同様のものを定義した。 -* 定義部分 - ```AGDA record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where field push : stackImpl -> a -> (stackImpl -> t) -> t pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t - pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t - get : stackImpl -> (stackImpl -> Maybe a -> t) -> t - get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t - clear : stackImpl -> (stackImpl -> t) -> t + -- 省略 open StackMethods record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where @@ -140,23 +173,48 @@ pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) popStack : (Stack a si -> Maybe a -> t) -> t popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - pop2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t - pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) - getStack : (Stack a si -> Maybe a -> t) -> t - getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - get2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t - get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) - clearStack : (Stack a si -> t) -> t - clearStack next = clear (stackMethods ) (stack ) (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) + -- 省略 +``` +* インスタンス生成 +```AGDA +singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a) +singleLinkedStackSpec = record { + push = pushSingleLinkedStack + ; pop = popSingleLinkedStack + -- 省略 + } + +createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a) +createSingleLinkedStack = record { + stack = emptySingleLinkedStack ; + stackMethods = singleLinkedStackSpec + } ``` -* Interface部分 +<!-- ## Tree の Interface --> -## Tree の Interface +<!-- ```AGDA --> +<!-- record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where --> +<!-- field --> +<!-- putImpl : treeImpl -> a -> (treeImpl -> t) -> t --> +<!-- getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t --> +<!-- open TreeMethods --> -```AGDA +<!-- record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where --> +<!-- field --> +<!-- tree : treeImpl --> +<!-- treeMethods : TreeMethods {n} {m} {a} {t} treeImpl --> +<!-- putTree : a -> (Tree treeImpl -> t) -> t --> +<!-- putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} )) --> +<!-- getTree : (Tree treeImpl -> Maybe a -> t) -> t --> +<!-- getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d ) --> +<!-- ``` --> -``` +<!-- * インスタンス生成 --> + +<!-- ```AGDA --> + +<!-- ``` --> ## Agda での Interface を含めた部分的な証明(Stack の例) @@ -176,22 +234,18 @@ push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl } ``` -## Agda での Interface の部分的な証明と課題(Tree の例) +<!-- ## Agda での Interface の部分的な証明と課題(Tree の例) --> -<!-- なんでだめなのかがうまく説明できないかも… --> -```AGDA +<!-- ```AGDA --> -``` +<!-- ``` --> ## Hoare Logic - * Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証するための手法 - * 前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) によって変更する - -* この {P} C {Q} でプログラムを部分的に表すことができる +* この {P} C {Q} でプログラムを部分的に表すことができるp <div style="text-align: center;"> <img src="./fig/hoare.svg" alt="hoare" width="1000"> @@ -203,16 +257,12 @@ * Hoare Logic の状態と処理を CodeGear、 DataGear の単位で考えることができると考えている <div style="text-align: center;"> - <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="600"> + <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="800"> </div> ## 今後の課題 - * 本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。 - * これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。 - * また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。 - * 今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。