Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/cbc-type.tex @ 100:ebe838b83ada

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Self review
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 12 Feb 2017 11:52:20 +0900
parents a891d7551bbf
children 5ad74fb83f72
comparison
equal deleted inserted replaced
99:a891d7551bbf 100:ebe838b83ada
141 実際、DataSegment が Meta DataSegment に拡張できたため、Meta CodeSegment の定義には比較的変更は無い。 141 実際、DataSegment が Meta DataSegment に拡張できたため、Meta CodeSegment の定義には比較的変更は無い。
142 ノーマルレベルの \verb/CodeSegment/ 型に、DataSegment を取って DataSegment を返す、という制約を明示的に付けるだけである(リスト~\ref{src:agda-mcs}) 142 ノーマルレベルの \verb/CodeSegment/ 型に、DataSegment を取って DataSegment を返す、という制約を明示的に付けるだけである(リスト~\ref{src:agda-mcs})
143 143
144 \lstinputlisting[label=src:agda-mcs, caption=Agda における Meta CodeSegment の定義] {src/MetaCodeSegment.agda.replaced} 144 \lstinputlisting[label=src:agda-mcs, caption=Agda における Meta CodeSegment の定義] {src/MetaCodeSegment.agda.replaced}
145 145
146 メタレベルの定義を部分型で行なって分かったことには以下のようなものがある。
147
148 \begin{itemize}
149 \item メタ計算は階層構造化できる
150
151 メタ計算は階層構造を取ることができるため、組み合わせることも可能である。
152
153 \item 継続先が不定の場合は型を一様に扱う必要がある
154
155 メタ計算がノーマルレベルの具体的な型を知ることができるのはコンパイル時のみである。
156 よってメタ計算を定義する時は部分型制約しか記述できない。
157 逆に言えばノーマルレベル計算のみであれば部分型は解決され、レコード型で型付けができる。
158
159 \item \verb/stub/ は部分型付けにおいても必要である
160
161 GearsOS では Meta DataSegment から DataSegment を取り出すための処理として \verb/stub/ が存在していた。
162 これは Meta DataSegment で一様に扱っていた DataSegment に型を戻す処理として、型システムにおいても必要なものである。'
163 また、型システム経由で \verb/stub/ を生成することも可能であると考えられる。
164
165 \end{itemize}
166
146 % }}} 167 % }}}
147 168
148 % {{{ メタレベル計算の実行 169 % {{{ メタレベル計算の実行
149 \section{メタレベル計算の実行} 170 \section{メタレベル計算の実行}
150 \label{section:meta-level-exec} 171 \label{section:meta-level-exec}
196 % {{{ Agda を用いた Continuation based C の証明 217 % {{{ Agda を用いた Continuation based C の証明
197 218
198 \section{Agda を用いた Continuation based C の証明} 219 \section{Agda を用いた Continuation based C の証明}
199 \label{section:cbc-proof} 220 \label{section:cbc-proof}
200 Agda において CbC の CodeSegment と DataSegment を定義することができた。 221 Agda において CbC の CodeSegment と DataSegment を定義することができた。
201 実際の CbC のコードを Agda に変換し、それらの性質を証明していく。 222 実際の CbC のコードを Agda で記述し、それらの性質を証明していく。
202 223
203 ここではGearsOS が持つ DataSegment \verb/SingleLinkedStack/ を証明していく。 224 ここではGearsOS が持つ DataSegment \verb/SingleLinkedStack/ を証明していく。
204 この\verb/SingleLinkedStack/はポインタを利用した片方向リストを用いて実装されている。 225 この\verb/SingleLinkedStack/はポインタを利用した片方向リストを用いて実装されている。
205 226
206 CbC における DataSegment \verb/SingleLinkedStack/ の定義はリスト~\ref{src:cbc-stack}のようになっている。 227 CbC における DataSegment \verb/SingleLinkedStack/ の定義はリスト~\ref{src:cbc-stack}のようになっている。
446 467
447 push-pop を一般化した n-push-pop を証明することができた。 468 push-pop を一般化した n-push-pop を証明することができた。
448 n-push-pop は証明の途中で補題 pop-n-push と push-pop を利用した定理である。 469 n-push-pop は証明の途中で補題 pop-n-push と push-pop を利用した定理である。
449 このように、CbC で記述されたプログラムを Agda 上に記述することで、データ構造の性質を定理として証明することができた。 470 このように、CbC で記述されたプログラムを Agda 上に記述することで、データ構造の性質を定理として証明することができた。
450 これらの証明機構を CbC のコンパイラやランタイム、モデルチェッカなどに組み込むことにより CbC は CbC で記述されたコードを証明することができるようになる。 471 これらの証明機構を CbC のコンパイラやランタイム、モデルチェッカなどに組み込むことにより CbC は CbC で記述されたコードを証明することができるようになる。
451 なお、本論文で取り扱っている Agda のソースコードは視認性の向上のために暗黙的な引数を省略して記述している。 472 なお、本論文で取り扱っている Agda のソースコードは可読性の向上のために暗黙的な引数を省略している。
452 動作する完全なコードは付録に付す。 473 完全なコードは付録に付す。
453 474
454 % }}} 475 % }}}
476