Mercurial > hg > Papers > 2018 > ryokka-sigos
changeset 12:e20725cd6d8a default tip
fix slides
| author | ryokka |
|---|---|
| date | Mon, 21 May 2018 00:29:29 +0900 |
| parents | 7aa41769f1f1 |
| children | |
| files | Slide/sigos.html Slide/sigos.md |
| diffstat | 2 files changed, 63 insertions(+), 44 deletions(-) [+] |
line wrap: on
line diff
--- a/Slide/sigos.html Sun May 20 23:42:24 2018 +0900 +++ b/Slide/sigos.html Mon May 21 00:29:29 2018 +0900 @@ -86,7 +86,7 @@ <!-- === begin markdown block === generated by markdown/1.2.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16] - on 2018-05-20 23:41:15 +0900 with Markdown engine kramdown (1.15.0) + on 2018-05-21 00:29:20 +0900 with Markdown engine kramdown (1.15.0) using options {} --> <!-- <span style="background-color:#ffcc99"> </span> --> @@ -129,17 +129,11 @@ <li>本研究では関数型の <strong>定理証明支援系</strong> の言語 <strong>Agda</strong> を用いて仕様を検証することにした</li> </ul> - -</div> -<div class='slide '> -<!-- _S9SLIDE_ --> -<h2 id="section-2">発表の流れ</h2> -<ul> - <li>CodeGear と DataGear の定義</li> - <li>Agda の説明</li> - <li>Agda での CodeGear、 DataGear の表現</li> - <li>今回行なった証明</li> -</ul> +<!-- ## 発表の流れ --> +<!-- * CodeGear と DataGear の定義 --> +<!-- * Agda の説明 --> +<!-- * Agda での CodeGear、 DataGear の表現 --> +<!-- * 今回行なった証明 --> <!-- ## Hoare Logic --> <!-- * Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証する手法 --> @@ -282,6 +276,7 @@ <div class='slide '> <!-- _S9SLIDE_ --> <h2 id="agda--3">Agda での関数</h2> + <ul> <li>Agda での関数は <strong>関数名 = 関数の実装</strong></li> <li>ここでは <strong>popSingleLinkedStack</strong> の関数を例とする @@ -289,12 +284,13 @@ <li><strong>関数名</strong> と <strong>=</strong> の間に記述されてる stack 、 cg は引数</li> <li>stack の top は Maybe a なので Nothing か Just が返り、2つの場合が存在</li> <li><strong>with</strong> と <strong>|</strong> を使うことで data の場合分けができる</li> + <li>top が next d になったスタックと取れたデータを渡してる</li> </ul> </li> </ul> <pre lang="AGDA"><code>popSingleLinkedStack : SingleLinkedStack a -> - (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t + (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t popSingleLinkedStack stack cg with (top stack) popSingleLinkedStack stack cg | Nothing = cg stack Nothing popSingleLinkedStack stack cg | Just d = cg record { top = (next d) } (Just (datum d)) @@ -310,8 +306,10 @@ <li>例として <strong>pushSingleLinkedStack</strong> の関数部分を扱う</li> </ul> -<pre lang="Agda"><code>pushSingleLinkedStack : {t : Set} {a : Set} -> SingleLinkedStack a -> a -> (Code : SingleLinkedStack a -> t) -> t -pushSingleLinkedStack stack datum next = next record {top = Just (record {datum = datum;next =(top stack)})} +<pre lang="Agda"><code>pushSingleLinkedStack : {t : Set} {a : Set} -> + SingleLinkedStack a -> a -> (Code : SingleLinkedStack a -> t) -> t +pushSingleLinkedStack stack datum next = + next record {top = Just (record {datum = datum ; next =(top stack)})} </code></pre> <ul> @@ -385,7 +383,7 @@ <!-- _S9SLIDE_ --> <h2 id="interface">Interface</h2> <ul> - <li>Interface は GearsOS のモジュール化の仕組み</li> + <li>Interface は GearsOS でのモジュール化の仕組み</li> <li>ある Data Gear と それに対する操作(API) を行う Code Gear の集合を表現</li> <li>Interface を使うとデータ構造への操作を仕様と実装に分けて記述することができる</li> </ul> @@ -419,7 +417,8 @@ <li><strong>createSingleLinkedStack</strong> は中身のない Stack を作る</li> </ul> -<pre lang="AGDA"><code>createSingleLinkedStack : {t : Set} {a : Set} -> Stack {n} {m} a {t} (SingleLinkedStack a) +<pre lang="AGDA"><code>createSingleLinkedStack : {t : Set} {a : Set} -> + Stack {n} {m} a {t} (SingleLinkedStack a) createSingleLinkedStack = record { stack = emptySingleLinkedStack ; stackMethods = singleLinkedStackSpec @@ -430,7 +429,8 @@ <li><strong>singleLinkedStackSpec</strong> は実装側の push、 pop をまとめている</li> </ul> -<pre lang="AGDA"><code>singleLinkedStackSpec : {t : Set} {a : Set} -> StackMethods a {t} (SingleLinkedStack a) +<pre lang="AGDA"><code>singleLinkedStackSpec : {t : Set} {a : Set} -> + StackMethods a {t} (SingleLinkedStack a) singleLinkedStackSpec = record { push = pushSingleLinkedStack ; pop = popSingleLinkedStack @@ -441,7 +441,7 @@ </div> <div class='slide '> <!-- _S9SLIDE_ --> -<h2 id="section-3">証明の概要</h2> +<h2 id="section-2">証明の概要</h2> <ul> <li>今回は <strong>任意の数</strong> を Stack に push し、直後にその Stack に対して pop を行ない、 push したデータと pop して取れたデータが等しくなることを証明する</li> <li>どのような状態の Stack に push し、 pop をしても値が等しくなって欲しい</li> @@ -473,7 +473,8 @@ <li>Agda では不明な部分を <strong>?</strong> と書くことができ、証明部分を ? としている</li> </ul> -<pre lang="AGDA"><code>push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) +<pre lang="AGDA"><code>push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> + pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) push->pop {a} x s = ? </code></pre> @@ -488,7 +489,8 @@ <li>ここでは <strong>\s1 -></strong> がラムダ計算で、受け取った Stack (s) に push を行い、更新された Stack (s1) を次の CodeGear に渡している</li> </ul> -<pre lang="AGDA"><code>push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) +<pre lang="AGDA"><code>pppush->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> + pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) </code></pre> @@ -500,7 +502,8 @@ <li><strong>?</strong> 部分はコンパイルすると <strong>{}n</strong> のように番号が付き、Agda から内部に入る型を示してもらえる</li> </ul> -<pre lang="AGDA"><code>push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) +<pre lang="AGDA"><code>push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> + pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) push->pop {a} x s = { }0 </code></pre> @@ -517,7 +520,8 @@ <li><strong>{ }0</strong> 部分には x≡x1 が入り、これは refl</li> </ul> -<pre lang="AGDA"><code>push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) +<pre lang="AGDA"><code>push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> + pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) push->pop {a} x s = refl </code></pre> @@ -527,14 +531,18 @@ </div> <div class='slide '> <!-- _S9SLIDE_ --> -<h2 id="section-4">まとめと今後の方針</h2> +<h2 id="section-3">まとめと今後の方針</h2> <ul> <li>本研究では CodeGear、DataGear を Agda で定義することができた</li> <li>また Agda で Interface の記述及び Interface を含めた証明を行うことができた</li> <li>これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた</li> - <li>また、CbC での Interface 記述では考えられていなかった細かな記述が明らかになった</li> - <li>RedBlackTree では Stack と異なり一つの操作に複数の CodeGear が入っているため Hoare Logic を使っての証明や、関数を展開しての証明などを行う</li> - <li>SynchronisedQueue の証明では並列処理シミュレーションを Agda で行うことと、動機機構などを含めての証明を行う</li> + <li>また、GearsOS での Interface 記述では考えられていなかった細かな記述が明らかになった</li> + <li>今後は RedBlackTree や SynchronisedQueue の証明を行いたい + <ul> + <li>RedBlackTree では Stack と異なり一つの操作に複数の CodeGear が入っているため、関数を展開しての証明などを行う</li> + <li>SynchronisedQueue の証明では並列処理シミュレーションを Agda で行うことと、動機機構などを含めての証明を行う</li> + </ul> + </li> </ul> <!-- === end markdown block === --> </div>
--- a/Slide/sigos.md Sun May 20 23:42:24 2018 +0900 +++ b/Slide/sigos.md Mon May 21 00:29:29 2018 +0900 @@ -32,11 +32,11 @@ * これは関数型プログラミングに近い形になる * 本研究では関数型の **定理証明支援系** の言語 **Agda** を用いて仕様を検証することにした -## 発表の流れ -* CodeGear と DataGear の定義 -* Agda の説明 -* Agda での CodeGear、 DataGear の表現 -* 今回行なった証明 +<!-- ## 発表の流れ --> +<!-- * CodeGear と DataGear の定義 --> +<!-- * Agda の説明 --> +<!-- * Agda での CodeGear、 DataGear の表現 --> +<!-- * 今回行なった証明 --> <!-- ## Hoare Logic --> <!-- * Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証する手法 --> @@ -134,15 +134,17 @@ ``` ## Agda での関数 + * Agda での関数は **関数名 = 関数の実装** * ここでは **popSingleLinkedStack** の関数を例とする * **関数名** と **=** の間に記述されてる stack 、 cg は引数 * stack の top は Maybe a なので Nothing か Just が返り、2つの場合が存在 * **with** と **\|** を使うことで data の場合分けができる + * top が next d になったスタックと取れたデータを渡してる ```AGDA popSingleLinkedStack : SingleLinkedStack a -> - (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t + (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t popSingleLinkedStack stack cg with (top stack) popSingleLinkedStack stack cg | Nothing = cg stack Nothing popSingleLinkedStack stack cg | Just d = cg record { top = (next d) } (Just (datum d)) @@ -153,8 +155,10 @@ * 例として **pushSingleLinkedStack** の関数部分を扱う ```Agda -pushSingleLinkedStack : {t : Set} {a : Set} -> SingleLinkedStack a -> a -> (Code : SingleLinkedStack a -> t) -> t -pushSingleLinkedStack stack datum next = next record {top = Just (record {datum = datum;next =(top stack)})} +pushSingleLinkedStack : {t : Set} {a : Set} -> + SingleLinkedStack a -> a -> (Code : SingleLinkedStack a -> t) -> t +pushSingleLinkedStack stack datum next = + next record {top = Just (record {datum = datum ; next =(top stack)})} ``` * **record** 後ろの **{}** 内部で **フィールド名 = 値** で列挙 @@ -220,7 +224,8 @@ * **createSingleLinkedStack** は中身のない Stack を作る ```AGDA -createSingleLinkedStack : {t : Set} {a : Set} -> Stack {n} {m} a {t} (SingleLinkedStack a) +createSingleLinkedStack : {t : Set} {a : Set} -> + Stack {n} {m} a {t} (SingleLinkedStack a) createSingleLinkedStack = record { stack = emptySingleLinkedStack ; stackMethods = singleLinkedStackSpec @@ -230,7 +235,8 @@ * **singleLinkedStackSpec** は実装側の push、 pop をまとめている ```AGDA -singleLinkedStackSpec : {t : Set} {a : Set} -> StackMethods a {t} (SingleLinkedStack a) +singleLinkedStackSpec : {t : Set} {a : Set} -> + StackMethods a {t} (SingleLinkedStack a) singleLinkedStackSpec = record { push = pushSingleLinkedStack ; pop = popSingleLinkedStack @@ -257,7 +263,8 @@ * Agda では不明な部分を **?** と書くことができ、証明部分を ? としている ```AGDA -push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) +push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> + pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) push->pop {a} x s = ? ``` @@ -267,14 +274,16 @@ * ここでは **\s1 ->** がラムダ計算で、受け取った Stack (s) に push を行い、更新された Stack (s1) を次の CodeGear に渡している ```AGDA -push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) +pppush->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> + pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) ``` ## Agda での Interface を含めた部分的な証明 * **?** 部分はコンパイルすると **{}n** のように番号が付き、Agda から内部に入る型を示してもらえる ```AGDA -push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) +push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> + pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) push->pop {a} x s = { }0 ``` @@ -287,7 +296,8 @@ * **{ }0** 部分には x≡x1 が入り、これは refl ```AGDA -push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) +push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> + pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 ))) push->pop {a} x s = refl ``` @@ -297,6 +307,7 @@ * 本研究では CodeGear、DataGear を Agda で定義することができた * また Agda で Interface の記述及び Interface を含めた証明を行うことができた * これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた -* また、CbC での Interface 記述では考えられていなかった細かな記述が明らかになった -* RedBlackTree では Stack と異なり一つの操作に複数の CodeGear が入っているため Hoare Logic を使っての証明や、関数を展開しての証明などを行う -* SynchronisedQueue の証明では並列処理シミュレーションを Agda で行うことと、動機機構などを含めての証明を行う +* また、GearsOS での Interface 記述では考えられていなかった細かな記述が明らかになった +* 今後は RedBlackTree や SynchronisedQueue の証明を行いたい + * RedBlackTree では Stack と異なり一つの操作に複数の CodeGear が入っているため、関数を展開しての証明などを行う + * SynchronisedQueue の証明では並列処理シミュレーションを Agda で行うことと、動機機構などを含めての証明を行う