Mercurial > hg > Papers > 2018 > ryokka-thesis

changeset 11:9af6c3636ea0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix slide
author ryokka
date Wed, 21 Feb 2018 13:03:19 +0900
parents a01801c32db7
children 8c205db691d4
files final_main/chapter1.tex final_main/chapter5.tex final_main/chapter6.tex final_main/main.pdf final_main/main.tex final_pre/finalPre.tex final_pre/reference.bib final_pre/src/AgdaInterface.agda final_pre/src/AgdaStackSomeState.agda slide/Makefile slide/slide.html slide/slide.md
diffstat 12 files changed, 757 insertions(+), 108 deletions(-) [+]
line wrap: on
line diff
--- a/final_main/chapter1.tex	Tue Feb 20 17:35:52 2018 +0900
+++ b/final_main/chapter1.tex	Wed Feb 21 13:03:19 2018 +0900
@@ -5,18 +5,25 @@
 % 序論の目安としては1枚半ぐらい．
 % 英語発表者は，最終予稿の「はじめに」の英訳などを載せてもいいかも．
 
-%% 想定外の挙動をしてほしくない
 
 
-動作するプログラム(ソフトウェア)は高い信頼性を持つことが望ましい。
+動作するソフトウェアは高い信頼性を持つことが望ましい。
+そのためにはソフトウェアが期待される動作をすることを保証する必要がある。
+期待される動作は仕様と呼ばれ、自然言語や論理によって記述される。
 
-プログラムの信頼性を保証するにはプログラムが期待される仕様を満たすことを検証する手法と、その仕様を直接証明する手法が存在している。
+ソフトウェアの検証手法にはモデル検査と定理証明がある。
+モデル検査とはソフトウェアの全ての状態を数え上げ、その状態について仕様が正し
+いことを確認する。モデル検査器には Spin\cite{spin} や、モデルを状態遷移系で記述
+する NuSMV\cite{nusmv}、C言語/C++ を記号実行する CBMC\cite{cbmc} などが存在する。
 
-そのために当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している。
-
+定理証明では。ソフトウェアが満たすべき仕様を論理式で記述し、その論理式が常に正し
+いことを証明する。定理証明支援器には依存型で証明を行なう Agda\cite{agda} や Coq\cite{coq} などが存在する。
 
-本研究では CbC を用いて Tree、 Stack を実装し、等価な Agda の実装を使ってその仕
-様の一部を証明した。
+当研究室では検証の単位として CodeGear、DataGear という単位を用いてソフトウェアを記述する手法を提案している。
+また、 CodeGear 、 DataGear という単位を用いてプログラミングする言語としてCountinuation based C\cite{kaito:2015}を開発している。Continuation based C (CbC)はC言語と似た構文を持つ言語である。
+
+本論文では Agda で
+使ってその仕様の一部を証明した。
 
 
 %% 動作するプログラムの信頼性を保証したい
--- a/final_main/chapter5.tex	Tue Feb 20 17:35:52 2018 +0900
+++ b/final_main/chapter5.tex	Wed Feb 21 13:03:19 2018 +0900
@@ -94,21 +94,39 @@
 \label{hoare-logic}
 
 Hoare Logic \cite{Hoare1969AnAB} とは Tony Hoare によって提案されたプログラム正
-しさを推論する手法である。P を前状態(PreCondition) 、C を処理(Command) 、 Q を
-後状態(PostCondition) とし、$\{P\} \  C  \ \{Q\}$ のように考えたとき、
-プログラムの処理を「前状態を満たした後、処理を行い状態が後状態に変化する」といっ
-た形で考える事ができる。
+しさを推論する手法である。図\ref{fig:hoare}のように、 P を前状態(Pre Condition)
+、C を処理(Command) 、 Q を後状態(Post Condition) とし、$\{P\} \  C  \ \{Q\}$ のように考えたとき、
+プログラムの処理を「前状態を満たした後、処理を行い状態が後状態に変化する」といった形で考える事ができる。
+
+\begin{figure}[htpb]
+ \begin{center}
+  \scalebox{0.6}[0.6]{\includegraphics{fig/hoare-logic.pdf}}
+ \end{center}
+ \caption{hoare logicの流れ}
+ \label{fig:hoare}
+\end{figure}
+
 
 このとき、後状態から前状態を推論することができればそのプログラムは部分的に正しい
 動きをすることを証明することができる。
+この Hoare Logic の前状態、処理、後状態を CodeGear、 input/output の DataGear が表
+\ref{fig:cbc-hoare} のように表せると考えている。
+
+\begin{figure}[htpb]
+ \begin{center}
+  \scalebox{0.8}[0.8]{\includegraphics{fig/cbc-hoare.pdf}}
+ \end{center}
+ \caption{cbc と hoare logic}
+ \label{fig:cbc-hoare}
+\end{figure}
+
 この状態を当研究室で提案している CodeGear、 DataGear の単位で考えると
-PreCondition が CodeGear に入力として与えられる Input DataGear、Command が
-CodeGear、 PostCondition を Output DataGear として当てはめることができると考えて
+Pre Condition が CodeGear に入力として与えられる Input DataGear、Command が
+CodeGear、 Post Condition を Output DataGear として当てはめることができると考えて
 いる。
 
-
-今後の研究では CodeGear、 DataGear、継続の概念を Hoare Logic に当てはめ、
-幾つかの実装を証明していく。
+今後の研究では CodeGear、 DataGear、継続の概念を Hoare Logic に当てはめ Agda に
+当てはめ、幾つかの実装を証明していく。
 
 % Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。
 % 最終的な Stack、Tree の証明は Hoare Logic ベースで行う。
--- a/final_main/chapter6.tex	Tue Feb 20 17:35:52 2018 +0900
+++ b/final_main/chapter6.tex	Wed Feb 21 13:03:19 2018 +0900
@@ -1,10 +1,16 @@
-\chapter{今後の課題}
+\chapter{まとめ}
 
 本研究では CodeGear、 DataGear を用いたプログラミング手法を使い、Agda で
-Interface を用いたプログラムを実装し、検証した。これにより、 CbC で記述した時に
-は細かく分かっていなかった Interface の型が明確になった。
-また、研究の中にに継続を利用することで得られた知見は、今後の研究で大いに役立つと
-考えている。。
+Interface を用いたプログラムを実装し、証明を記述した。
+これにより、 CbC で記述した時には細かく分かっていなかった Interface の型が明確になった。
+また、 Hoare Logic を CodeGear 、 DataGear と対応させることで Hoare Logic ベース
+で証明が進められると考えている。
+今回の研究中に継続を利用することで得られた知見は、今後の研究で大いに役立つと
+考える。
 
-今後の課題は、CodeGear、DataGear をベースにした Hoare Logic を Agda で実装する。
-また、その Hoare Logic を使い、いくつかの証明を実際に記述する。
\ No newline at end of file
+今後の課題としては、CbC 上での RedBlackTree の実装や、 Agda 上での RedBlackTree
+の実装と証明がある。また、 CodeGear、DataGear をベースにした Hoare Logic を Agda で実
+装する。
+Agda 定義した Hoare Logic を使い、いくつかの証明を実際に記述し、書き方を確立するなどが考えられる。
+他にも、タスクスケジューラの実装を Agda に移し、 SynchronizedQueue の同期、非同
+期の検証などが考えられる。
Binary file final_main/main.pdf has changed
--- a/final_main/main.tex	Tue Feb 20 17:35:52 2018 +0900
+++ b/final_main/main.tex	Wed Feb 21 13:03:19 2018 +0900
@@ -113,6 +113,7 @@
 
 % 参考文献
 %% こっちで書きたいよね
+
 \nocite{*}
 \bibliographystyle{junsrt}
 \bibliography{reference}
--- a/final_pre/finalPre.tex	Tue Feb 20 17:35:52 2018 +0900
+++ b/final_pre/finalPre.tex	Wed Feb 21 13:03:19 2018 +0900
@@ -40,12 +40,13 @@
 \renewcommand{\abstractname}{Abstract}
 \begin{document}
 
-\title{Agda と継続を用いたプログラムの検証 \\ Verification of program using Agda and continuation}
+\title{Agda と継続を用いたプログラムの検証 \\ Verification of program using Continuation by Agda}
 \author{145750B 氏名 {外間}{政尊} 指導教員 : 河野 真治}
 \date{}
 \twocolumn [
 \maketitle
 \begin{onecolabstract}
+
   % 高い信頼性を持つことは重要である。  
   % 私たちはプログラムの信頼性を高めるためにCodeGear、DataGearという単位でプログラ
   % ムを書くことを提案している。
@@ -56,46 +57,20 @@
   % 変換した。
   % この論文ではそれらに対して幾つかの部分的な証明を試みた。
 
-  Program has high reliability. it is important.
-  we are proposing to write program in units of CodeGear, DataGear for increase
-  the reliability.
-  we are deceloping Continuation based C (CbC) that can use units CodeGear and
-  DataGear.
-  In CbC, the handling of data in existing implementations is complicated.
-  for that purpose, we can provide a interface mechanisms which are packages of
-  CodeGears and DataGears.
-  we made these units and interface available for Agda.
-  Also converted Stack and Tree wrote in CbC to Agda.
-  In this papaer, we tried several proofs on them.
-% 
-% (we are mapping this units to Agda)
-% CbC では CodeGear 、 DataGear という単位でプログラミングできる。
-% ~~
-% Agda で interface を実装
-% interface を含めて証明ができるか
-% codeとcode のあいだをcall ではなくjmpで結ぶことができる(goto)
-%gotoをつかうことによりOSに必須なmeta計算を実現できる
-%メタ計算は例えばメモリ管理スレッド管理CPUやGPUの資源管理そしてData/Code Gear の管理などである
-%metaレベルではcode/data gear は一つの塊として操作される。これをcbcではunion dataとして実装している
-%code gear 間の接続はつぎのcode gearの番号とthread structure に相当するcontextをmeta code gear にgoto する
-%meta code gear で os の 機能であるメモリ管理やスレッド管理を行う。
-%ユーザーレベルではmeta構造を直接見ることはなく、継続を用いた関数型プログラミングに見える
-%metaレベルから見たdata gearをゆーざーれべるのcode gearに接続するにはstub というmeta code gear  を用いる
-%stubとmetaはユーザーレベルcodegear とdatagearから生成することができる
-%本論文ではstub とcontext 管理構造を生成するスクリプトを作成した
-%これによりcode gear とdeta gear をデータを操作するinterface というまとまりにすることができる。
-% CbC gives Code Gear and Data Gear as programing units.
-% A transfer from a Code Gear to another Code Gear is implemented using a CbC's goto statement,
-% which is compiled as a jump instruction in CbC. 
-% CbC's goto statements provides a ways of implementing meta computations.
-% From a view point of meta computation, Data Gear or Code Gear are uniform data units, which are implemented
-% as union Data in CbC. 
-% In the meta level, a transfer from a Code Gear is a goto statement to meta Code Gear with next Code Gear number and 
-% a Context which corresponds thread structure or an environments in a functional programing.
-% From a normal level, meta structures are not visible directly and a Code Gear looks like a function using continuations.
-% A stub Code Gear is used as a bridge between meta level and normal level.
-% we can generate meta Code Gear and stub Code Gear from normal level Code Gear,
-% and provide a interface mechanisms which are packages of Code Gears and Data Gears.
+  
+  % High reliability is important in Program.
+  % we are proposing programing units of CodeGear, DataGear for increase
+  % the reliability.
+  % we are deceloping Continuation based C (CbC) that can use units CodeGear and
+  % DataGear.
+  % In CbC, the handling of data in existing implementations is complicated.
+  % for that purpose, we can provide a interface mechanisms which are packages of
+  % CodeGears and DataGears.
+  % we made these units and interface available for Agda.
+  % In this papaer, we converted Stack and Tree using the interface discribe in
+  % CbC to Agda, and we tried several proofs on them.
+  
+
 \end{onecolabstract}]
 \thispagestyle{fancy}
 
@@ -108,7 +83,9 @@
 
 \section{ソフトウェアの信頼性の保証}
 ソフトウェアの信頼性を保証することは重要である。現在ソフトウェアの信頼性を保証す
-る方法として代表的なものはモデル検査と、定理証明が存在している。
+る方法として代表的なものはモデル検査と、定理証明が存在している。定理証明支援器と
+して有名なものとしては Agda\cite{agda} が存在する。
+
 当研究室では検証しやすいプログラムの単位として、 CodeGear と DataGear という単位
 を用いるプログラミングスタイルを提案している。
 また、 CodeGear 、 DataGear という単位を用いてプログラミングする言語として
@@ -128,8 +105,9 @@
 Interface では、DataGear に対しての操作(API)を CodeGear とその CodeGear で扱われ
 ている DataGearの集合を抽象的に表現した Meta DataGear として定義されている。
 
-本研究では CbCで使われている Interface を 、 Agda 上で定義、実装を行い、
-Interface を含めた Stack と Tree の部分的な証明を行なった。
+本研究では CbCで使われている Interface を含めて証明を行うために、 Agda 上で
+Interface の定義、実装を行なった。
+また Interface を含めた Stack と Tree の部分的な証明を行なった。
 
 \section{Countinuation based C (CbC)}
 Continuation based C (CbC) とは、当研究室で開発されているプログラミング言語である。
@@ -140,9 +118,10 @@
 DataGear は CodeGear が扱うデータの単位であり、処理に必要なデータが全て入っている。次の CodeGear に処理を移す際は、 goto の後に CodeGear 名と DataGear を指定する。
 CbC ではこの継続処理がメタ計算として定義されており、通常計算である CodeGear を変
 更することなく検証や資源管理等の記述を行うことができる。
-例として CbC の簡単な例(ソースコード\ref{src:goto})と、流れ\ref{fig:code_simple}を示す。
+例として CbC の簡単な例をソースコード\ref{src:goto}に、流れを図\ref{fig:code_simple}示す。
 
 \lstinputlisting[label=src:goto, caption=CbCコードの例]{./src/goto.cbc}
+
 \begin{figure}[htpb]
  \begin{center}
    \scalebox{0.7}[0.7]{\includegraphics{fig/codesegment.pdf}}
@@ -156,6 +135,30 @@
 流れ\ref{fig:code_simple}は cs0 から cs1 へ継続した後、 cs0 には戻らずに次の継
 続に指定された CodeGear へ継続する。
 
+\section{Agda}
+Agda とは定理証明支援器であり依存型を関数プログラミング言語である。
+依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述することができる。
+CbC を Agda に変換する場合 DataGear はレコード型、 CodeGear は Agda での通常関数
+として定義できる。
+ソースコード\ref{src:goto} で示した CbC の簡単な例を Agda に変換したものをソースコー
+ド\ref{src:agda-css}に示す。
+
+\lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義]
+{src/CodeSegments.agda}
+
+Agda のコードで関数を定義するときは関数名、型を記述した後に関数本体を指定する。
+関数の型では → または \verb/->/ を使い定義し、関数本体は関数名の後に$=$をつけて
+記述する。
+DataGear はレコード型で表記できるため Agda 上で DataGear を定義することが可能で
+ある。
+ % 定義をする際は record キーワードのあとにレコード名、
+% 型、 where の後に field キーワードを入れ、フィールド名 : 型名 と列挙する。レコー
+% ドを構築する際は record キーワードの後に {} 内部に fileName = value の形で列挙
+% していく。複数の値を列挙する際は ; で区切る。
+% Agda での DataGear の定義の例を以下のソースコード\ref{src:agda-ds}示す
+% \lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda}
+このように CbC のコードを Agda に変換し、証明を行う。
+
 \section{CbC における Interface の定義}
 CbC で実装していくにつれ、stub CodeGear の記述が煩雑になった。
 そのため 既存の実装を モジュールとして扱うため Interface を導入した。
@@ -172,28 +175,6 @@
 このように Interface 記述をすることで CbC で通常記述する必要がある一定の部分を省略し呼び出
 しが容易になる。
 
-\section{Agda}
-Agda\cite{agda} とは定理証明支援器であり依存型を関数プログラミング言語である。
-依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述することができる。
-CbC を Agda に変換する場合 DataGear はレコード型、 CodeGear は Agda での通常関数
-として定義できる。
-前項で示した CbC の簡単な例を Agda に変換する。(ソースコード\ref{src:agda-css})
-
-\lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義]
-{src/CodeSegments.agda}
-
-Agda のコードで関数を定義するときは関数名、型を記述した後に関数本体を指定する。
-関数の型では → または \verb/->/ を使い定義し、関数本体は関数名の後に$=$をつけて
-記述する。
-DataGear はレコード型で表記できるため Agda 上で DataGear を定義することが可能で
-ある。
- % 定義をする際は record キーワードのあとにレコード名、
-% 型、 where の後に field キーワードを入れ、フィールド名 : 型名 と列挙する。レコー
-% ドを構築する際は record キーワードの後に {} 内部に fileName = value の形で列挙
-% していく。複数の値を列挙する際は ; で区切る。
-% Agda での DataGear の定義の例を以下のソースコード\ref{src:agda-ds}示す
-% \lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda}
-このように CbC のコードを Agda に変換し、証明を行う。
 
 \section{Agda における Interface の定義、実装}
 Agda でも CbC と同様に Interface の定義、実装した。
@@ -218,14 +199,16 @@
 に入れた値と一致する」という性質を証明した。
 
 まず始めに不定状態の Stack をソースコード~\ref{src:agda-in-some-state}
-で定義した。 stackInSomeState が不定状態の Stack である。
- ソースコード~\ref{src:agda-in-some-state}の証明ではこのstackInSomeState に対し
- て、 push を2回行い、 pop2 をして取れたデータは push したデータと同じものになる
- ことの証明している。
+で定義した。 stackInSomeState は不定状態の Stack を定義する関数である。
+ソースコード~\ref{src:agda-proof}の証明ではこの stackInSomeState に対し
+て、 push を2回行い、 pop2 をして取れたデータは push したデータと同じものになる
+ことの証明している。
 
- \lstinputlisting[label=src:agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda}
+ \lstinputlisting[label=src:agda-in-some-state, caption=不定なStackの定義]{src/AgdaStackSomeState.agda}
+
+ \lstinputlisting[label=src:agda-proof, caption=push$->$push$->$pop2 の証明]{src/AgdaProof.agda}
  
-stackInSomeState 型の s が抽象的な Stack で、そこに x 、 y の２つのデー
+stackInSomeState は引数として s を取っていて、不定な Stack そこに x 、 y の２つのデー
 タを push している。また、 pop2 で取れたデータは y1 、 x1 となっていて両方が
 Just で返ってくるかつ、 x と x1 、 y と y1 がそれぞれ合同であることが仮定として
 型に書いた。関数本体で返る値は$ x \equiv x1 と y \equiv y1$で両方共に成り立つ為、
@@ -239,8 +222,8 @@
 また、 CbC で記述した時には細かく分かっていなかった Interface の型が明確に
 なった。
 今後の課題としては、Tree 側では証明が複雑化し、うまく証明できていないことと、
- Hoare Logic 用いての証明を行えるように、CodeGear、DataGear をベースにした Hoare
- Logic を Agda 上で定義し、実際に証明を行うことなどが挙げられる。
+Hoare Logic 用いての証明を行えるように、CodeGear、DataGear をベースにした Hoare
+Logic を Agda 上で定義し、実際に証明を行うことなどが挙げられる。
 
 \nocite{*}
 \bibliographystyle{junsrt}
--- a/final_pre/reference.bib	Tue Feb 20 17:35:52 2018 +0900
+++ b/final_pre/reference.bib	Wed Feb 21 13:03:19 2018 +0900
@@ -22,12 +22,12 @@
 @misc{agda,
     title = {The Agda wiki},
     howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}},
-    note = {Accessed: 2017/10/24(Tue)}
+    note = {Accessed: 2018/2/20(Tue)}
 }
 
 
 @misc{agda-documentation,
-    title = {Welcome to Agda’s documentation! — Agda 2.6.0 documentation},
-    howpublished = {\url{http://agda.readthedocs.io/en/latest/index.html}},
-    note = {Accessed: 2017/10/24(Tue)}
+    title = {Welcome to Agda’s documentation! — Agda 2.5.3 documentation},
+    howpublished = {\url{http://agda.readthedocs.io/en/v2.5.3/index.html}},
+    note = {Accessed: 2018/2/20(Tue)}
 }
\ No newline at end of file
--- a/final_pre/src/AgdaInterface.agda	Tue Feb 20 17:35:52 2018 +0900
+++ b/final_pre/src/AgdaInterface.agda	Wed Feb 21 13:03:19 2018 +0900
@@ -2,5 +2,5 @@
   field
     stack : si
     stackMethods : StackMethods {n} {m} a {t} si
-  pushStack :  a -> (Stack a si -> t) -> t
-  pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
+    pushStack :  a -> (Stack a si -> t) -> t
+    pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
--- a/final_pre/src/AgdaStackSomeState.agda	Tue Feb 20 17:35:52 2018 +0900
+++ b/final_pre/src/AgdaStackSomeState.agda	Wed Feb 21 13:03:19 2018 +0900
@@ -1,6 +1,2 @@
 stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
 stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
-
-push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
-pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slide/Makefile	Wed Feb 21 13:03:19 2018 +0900
@@ -0,0 +1,12 @@
+TARGET = slide
+
+.SUFFIXES: .md .html
+
+.md.html:
+	slideshow b $< -t s6cr --h2
+
+all: $(TARGET).html
+	open $(TARGET).html
+
+clean: 
+	rm -f *.html
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slide/slide.html	Wed Feb 21 13:03:19 2018 +0900
@@ -0,0 +1,408 @@
+<!DOCTYPE html>
+<html>
+<head>
+   <meta http-equiv="content-type" content="text/html;charset=utf-8">
+   <title>「Agda による継続を用いたプログラムの検証」</title>
+
+<meta name="generator" content="Slide Show (S9) v2.5.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin16]">
+<meta name="author"    content="外間 政尊" >
+
+<!-- style sheet links -->
+<link rel="stylesheet" href="s6/themes/projection.css"   media="screen,projection">
+<link rel="stylesheet" href="s6/themes/screen.css"       media="screen">
+<link rel="stylesheet" href="s6/themes/print.css"        media="print">
+<link rel="stylesheet" href="s6/themes/blank.css"        media="screen,projection">
+
+<!-- JS -->
+<script src="s6/js/jquery-1.11.3.min.js"></script>
+<script src="s6/js/jquery.slideshow.js"></script>
+<script src="s6/js/jquery.slideshow.counter.js"></script>
+<script src="s6/js/jquery.slideshow.controls.js"></script>
+<script src="s6/js/jquery.slideshow.footer.js"></script>
+<script src="s6/js/jquery.slideshow.autoplay.js"></script>
+
+<!-- prettify -->
+<link rel="stylesheet" href="scripts/prettify.css">
+<script src="scripts/prettify.js"></script>
+
+<script>
+  $(document).ready( function() {
+    Slideshow.init();
+
+    $('code').each(function(_, el) {
+      if (!el.classList.contains('noprettyprint')) {
+        el.classList.add('prettyprint');
+      }
+    });
+    prettyPrint();
+  } );
+
+  
+</script>
+
+<!-- Better Browser Banner for Microsoft Internet Explorer (IE) -->
+<!--[if IE]>
+<script src="s6/js/jquery.microsoft.js"></script>
+<![endif]-->
+
+
+
+</head>
+<body>
+
+<div class="layout">
+  <div id="header"></div>
+  <div id="footer">
+    <div align="right">
+      <img src="s6/images/logo.svg" width="200px">
+    </div>
+  </div>
+</div>
+
+<div class="presentation">
+
+  <div class='slide cover'>
+    <table width="90%" height="90%" border="0" align="center">
+      <tr>
+        <td>
+          <div align="center">
+            <h1><font color="#808db5">「Agda による継続を用いたプログラムの検証」</font></h1>
+          </div>
+        </td>
+      </tr>
+      <tr>
+        <td>
+          <div align="left">
+            外間 政尊
+            @並列信頼研
+            <hr style="color:#ffcc00;background-color:#ffcc00;text-align:left;border:none;width:100%;height:0.2em;">
+          </div>
+        </td>
+      </tr>
+    </table>
+  </div>
+
+<div class='slide '>
+<!-- === 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)
+                  using options {}
+  -->
+
+<!-- _S9SLIDE_ -->
+<h2 id="section">ソフトウェアの信頼性の保証</h2>
+
+<ul>
+  <li>
+    <p>動作するプログラムの信頼性を保証したい</p>
+  </li>
+  <li>
+    <p>そのために当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している</p>
+  </li>
+  <li>
+    <p>処理の単位である CodeGear はメタ計算によって接続され、メタ計算部分を切り替えることで CodeGear に一切の変更なくプログラムの性質を検証することができる</p>
+  </li>
+  <li>
+    <p>本研究では CodeGear 、 DataGear を用いて記述する言語、 Continuation based C (CbC) を用いてプログラムを記述し、それを証明することで信頼性を上げることを目標としている</p>
+  </li>
+  <li>
+    <p>CbC での記述を Agda にマッピングし、その性質の一部を証明した</p>
+  </li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="codegear--datagear">CodeGear と DataGear</h2>
+
+<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>
+<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>
+</ul>
+
+<pre lang="C"><code>__code cs0(int a, int b){
+  goto cs1(a+b);
+}
+
+__code cs1(int c){
+  goto cs2(c);
+}
+</code></pre>
+
+
+</div>
+<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>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="interface">Interface</h2>
+
+<ul>
+  <li>CbC で実装していくにつれて stub CodeGear の記述が煩雑になることがわかった</li>
+  <li>そこで Interface というモジュール化の仕組みを導入した</li>
+  <li>Interface は CodeGear とそこで扱われている DataGear の集合を抽象的に表現した Meta DataGear として定義されている</li>
+  <li><strong>__code next(…)</strong> は継続を表していて <strong>…</strong>部分は後続の引数に相当する</li>
+</ul>
+
+<pre lang="C"><code>typedef struct Stack&lt;Type, Impl&gt;{
+        // DataGear
+        union Data* stack;
+        union Data* data;
+        union Data* data1;
+
+        // CodeGear
+        __code whenEmpty(...);
+        __code clear(Impl* stack,__code next(...));
+        __code push(Impl* stack,Type* data, __code next(...));
+        // 省略
+        __code next(...);
+} Stack;
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="interface-">Interface の実装</h2>
+
+<ul>
+  <li>
+    <p>Interface を表す DataGear は次のような関数で生成される</p>
+  </li>
+  <li>
+    <p><strong>stack-&gt;push</strong> のようにしてコード中で使うことができる</p>
+  </li>
+</ul>
+
+<pre lang="C"><code>Stack* createSingleLinkedStack(struct Context* context) {
+    struct Stack* stack = new Stack();
+    struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack();
+    stack-&gt;stack = (union Data*)singleLinkedStack;
+    singleLinkedStack-&gt;top = NULL;
+    stack-&gt;push = C_pushSingleLinkedStack;
+    stack-&gt;pop  = C_popSingleLinkedStack;
+    // 省略
+    return stack;
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda">Agda</h2>
+
+<ul>
+  <li>
+    <p>Agda とは定理証明支援器で、型システムを用いて証明を記述できる。</p>
+  </li>
+  <li>
+    <p>Agda 上で CodeGear、 DataGear の単位と継続を定義した</p>
+  </li>
+</ul>
+
+<!-- AgdaのInterface の例 -->
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--interface-">Agda での Interface の定義</h2>
+
+<ul>
+  <li>
+    <p>Agda上でも CbC の Interface と同様のものを定義した。</p>
+  </li>
+  <li>
+    <p>定義部分</p>
+  </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 -&gt; a -&gt; (stackImpl -&gt; t) -&gt; t
+    pop  : stackImpl -&gt; (stackImpl -&gt; Maybe a -&gt; t) -&gt; t
+    pop2 : stackImpl -&gt; (stackImpl -&gt; Maybe a -&gt; Maybe a -&gt; t) -&gt; t
+    get  : stackImpl -&gt; (stackImpl -&gt; Maybe a -&gt; t) -&gt; t
+    get2 : stackImpl -&gt; (stackImpl -&gt; Maybe a -&gt; Maybe a -&gt; t) -&gt; t
+    clear : stackImpl -&gt; (stackImpl -&gt; t) -&gt; t 
+open StackMethods
+
+record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
+  field
+    stack : si
+    stackMethods : StackMethods {n} {m} a {t} si
+  pushStack :  a -&gt; (Stack a si -&gt; t) -&gt; t
+  pushStack d next = push (stackMethods ) (stack ) d (\s1 -&gt; next (record {stack = s1 ; stackMethods = stackMethods } ))
+  popStack : (Stack a si -&gt; Maybe a  -&gt; t) -&gt; t
+  popStack next = pop (stackMethods ) (stack ) (\s1 d1 -&gt; next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
+  pop2Stack :  (Stack a si -&gt; Maybe a -&gt; Maybe a -&gt; t) -&gt; t
+  pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -&gt; next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
+  getStack :  (Stack a si -&gt; Maybe a  -&gt; t) -&gt; t
+  getStack next = get (stackMethods ) (stack ) (\s1 d1 -&gt; next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
+  get2Stack :  (Stack a si -&gt; Maybe a -&gt; Maybe a -&gt; t) -&gt; t
+  get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -&gt; next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
+  clearStack : (Stack a si -&gt; t) -&gt; t
+  clearStack next = clear (stackMethods ) (stack ) (\s1 -&gt; next (record {stack = s1 ; stackMethods = stackMethods } ))
+</code></pre>
+
+<ul>
+  <li>Interface部分</li>
+</ul>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="tree--interface">Tree の Interface</h2>
+
+<pre lang="AGDA"><code>
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--interface-stack-">Agda での Interface を含めた部分的な証明(Stack の例)</h2>
+
+<ul>
+  <li>不定な Stack を作成し、そこに push し、直後に pop した値が push した値と等しいことを示している</li>
+</ul>
+
+<pre lang="AGDA"><code>stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -&gt; Stack {l} {m} D {t}  ( SingleLinkedStack  D )
+stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
+
+</code></pre>
+
+<p lang="AGDA">実際の証明</p>
+<pre><code>push-&gt;push-&gt;pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -&gt;
+    pushStack ( stackInSomeState s )  x ( \s1 -&gt; pushStack s1 y ( \s2 -&gt; pop2Stack s2 ( \s3 y1 x1 -&gt; (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push-&gt;push-&gt;pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="agda--interface-tree-">Agda での Interface の部分的な証明と課題(Tree の例)</h2>
+
+<!-- なんでだめなのかがうまく説明できないかも… -->
+
+<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>
+</ul>
+
+<div style="text-align: center;">
+    <img src="./fig/hoare.svg" alt="hoare" width="1000" />
+</div>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="hoare-logic--cbc">Hoare Logic と CbC</h2>
+
+<ul>
+  <li>Hoare Logic の状態と処理を CodeGear、 DataGear の単位で考えることができると考えている</li>
+</ul>
+
+<div style="text-align: center;">
+    <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="600" />
+</div>
+
+
+</div>
+<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>
+</ul>
+<!-- === end markdown block === -->
+</div>
+
+
+</div><!-- presentation -->
+</body>
+</html>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slide/slide.md	Wed Feb 21 13:03:19 2018 +0900
@@ -0,0 +1,218 @@
+title: 「Agda による継続を用いたプログラムの検証」
+author: 外間 政尊
+profile: @並列信頼研
+lang: Japanese
+code-engine: coderay
+
+
+## ソフトウェアの信頼性の保証
+
+* 動作するプログラムの信頼性を保証したい
+
+* そのために当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している
+
+* 処理の単位である CodeGear はメタ計算によって接続され、メタ計算部分を切り替えることで CodeGear に一切の変更なくプログラムの性質を検証することができる
+
+* 本研究では CodeGear 、 DataGear を用いて記述する言語、 Continuation based C (CbC) を用いてプログラムを記述し、それを証明することで信頼性を上げることを目標としている
+
+* CbC での記述を Agda にマッピングし、その性質の一部を証明した
+
+
+## CodeGear と DataGear
+
+* CodeGear とはプログラムを記述する際の処理の単位である。
+
+* DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。
+
+* CodeGear はメタ計算によって CodeGear へ接続される
+
+* CodeGear は入力として DataGear を受け取り、 DataGear に変更を加えて次に指定された CodeGear へ継続する。
+
+
+## Continuation based C (CbC)
+
+* 当研究室で開発している言語
+
+* 基本的な構文は C 言語と同じ
+
+* CodeGear、 DataGear という単位を用いてプログラムを記述する
+
+* CbC では 通常計算とメタ計算を分離している
+
+* CodeGear を継続し、 DataGear を変更しながらプログラムが進んでいく
+
+* CodeGear は関数の定義前に__codeがつき、関数末尾で継続である goto により次の CodeGear が指定される
+
+* DataGear はレコードで定義する
+
+```C
+__code cs0(int a, int b){
+  goto cs1(a+b);
+}
+
+__code cs1(int c){
+  goto cs2(c);
+}
+```
+
+
+## Context
+
+* CodeGear や DataGear をリストとして、 Context と呼ばれる Meta DataGear の中で定義している
+* しかし Context は Meta DataGear のため、通常レベルである CodeGear で直接扱うのは避けたい
+* その為、 stub CodeGear という Meta CodeGear を定義している。
+* 現段階で複雑でない stub CodeGear はスクリプトを使って自動生成している
+
+## Interface
+
+* CbC で実装していくにつれて stub CodeGear の記述が煩雑になることがわかった
+* そこで Interface というモジュール化の仕組みを導入した
+* Interface は CodeGear とそこで扱われている DataGear の集合を抽象的に表現した Meta DataGear として定義されている
+* **__code next(...)** は継続を表していて **...**部分は後続の引数に相当する
+
+```C
+typedef struct Stack<Type, Impl>{
+        // DataGear
+        union Data* stack;
+        union Data* data;
+        union Data* data1;
+
+        // CodeGear
+        __code whenEmpty(...);
+        __code clear(Impl* stack,__code next(...));
+        __code push(Impl* stack,Type* data, __code next(...));
+        // 省略
+        __code next(...);
+} Stack;
+```
+
+## Interface の実装
+
+* Interface を表す DataGear は次のような関数で生成される
+
+*  **stack->push** のようにしてコード中で使うことができる
+
+```C
+Stack* createSingleLinkedStack(struct Context* context) {
+    struct Stack* stack = new Stack();
+    struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack();
+    stack->stack = (union Data*)singleLinkedStack;
+    singleLinkedStack->top = NULL;
+    stack->push = C_pushSingleLinkedStack;
+    stack->pop  = C_popSingleLinkedStack;
+    // 省略
+    return stack;
+```
+
+
+## Agda
+
+* Agda とは定理証明支援器で、型システムを用いて証明を記述できる。
+
+* Agda 上で CodeGear、 DataGear の単位と継続を定義した
+
+
+
+<!-- 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
+  field
+    stack : si
+    stackMethods : StackMethods {n} {m} a {t} si
+  pushStack :  a -> (Stack a si -> t) -> t
+  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 } ))
+```
+
+* Interface部分
+
+## Tree の Interface
+
+```AGDA
+
+```
+
+## Agda での Interface を含めた部分的な証明(Stack の例)
+
+* 不定な Stack を作成し、そこに push し、直後に pop した値が push した値と等しいことを示している
+
+
+```AGDA
+stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
+stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
+
+```
+
+実際の証明
+```AGDA
+push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
+    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
+```
+
+## Agda での Interface の部分的な証明と課題(Tree の例)
+
+<!-- なんでだめなのかがうまく説明できないかも… -->
+
+```AGDA
+
+```
+
+
+## Hoare Logic
+
+* Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証するための手法
+
+* 前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) によって変更する
+
+* この {P} C {Q} でプログラムを部分的に表すことができる
+
+<div style="text-align: center;">
+    <img src="./fig/hoare.svg" alt="hoare" width="1000">
+</div>
+
+
+## Hoare Logic と CbC
+
+* Hoare Logic の状態と処理を CodeGear、 DataGear の単位で考えることができると考えている
+
+<div style="text-align: center;">
+    <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="600">
+</div>
+
+
+## 今後の課題
+
+* 本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。
+
+* これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。
+
+* また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。
+
+* 今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。