# HG changeset patch # User atton # Date 1486634333 -32400 # Node ID 2bc816f4af27fb55f55fab91be7fbffef648cdd3 # Parent 16dc3337a5a902fc458021002e82c8b2e83350cf Fix diff -r 16dc3337a5a9 -r 2bc816f4af27 paper/agda.tex --- a/paper/agda.tex Thu Feb 09 18:54:18 2017 +0900 +++ b/paper/agda.tex Thu Feb 09 18:58:53 2017 +0900 @@ -45,7 +45,7 @@ 例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書ける。 Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{src:agda-function}のようになる。 -\lstinputlisting[label=src/agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda.replaced} +\lstinputlisting[label=src:agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda.replaced} 引数は変数名で受けることもできるが、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。 diff -r 16dc3337a5a9 -r 2bc816f4af27 paper/akasha.tex --- a/paper/akasha.tex Thu Feb 09 18:54:18 2017 +0900 +++ b/paper/akasha.tex Thu Feb 09 18:58:53 2017 +0900 @@ -203,14 +203,14 @@ \begin{center} \includegraphics[width=300pt]{fig/akashaPut.pdf} \caption{put を利用するプログラムのメタを上書きする} - \label{fig:akahsaPut} + \label{fig:akashaPut} \end{center} \end{figure} \verb/meta/ はリスト\ref{src:rbtree-insert-case-2}の \verb/insertCase2/ のように軽量継続を行なう際に CodeSegment 名と DataSegment を指定するものである。 -検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続である(リスト\ref{src:meta})。 +検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続であった(リスト\ref{src:default-meta})。 -\lstinputlisting[label=src:meta, caption=通常の CodeSegment の軽量継続] {src/meta.c} +\lstinputlisting[label=src:default-meta, caption=通常の CodeSegment の軽量継続] {src/meta.c} これを、検証を行なうように変更することで \verb/insertCase2/ といった赤黒木の実装のコードを修正することなく検証を行なうことができる。 検証を行ないながら軽量継続する \verb/meta/ はリスト\ref{src:akasha-meta}のように定義される。 @@ -227,7 +227,7 @@ % {{{ モデル検査器 CBMC との比較 \section{モデル検査器 CBMC との比較} -akasha の比較対象として、 C言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いて赤黒木を検証した。 +akasha の比較対象として、 C言語の有限モデルチェッカ CBMC\cite{cbmc} を用いて赤黒木を検証した。 CBMC は ANSI-C を記号実行し、仕様の否定となるような実行パターンが無いかを検証するツールである。 比較のために全く同じ赤黒木のソースコードを用いたいが、CbCの構文は厳密にはCとは異なるために変換が必要である。 diff -r 16dc3337a5a9 -r 2bc816f4af27 paper/atton-master.pdf Binary file paper/atton-master.pdf has changed diff -r 16dc3337a5a9 -r 2bc816f4af27 paper/cbc-type.tex --- a/paper/cbc-type.tex Thu Feb 09 18:54:18 2017 +0900 +++ b/paper/cbc-type.tex Thu Feb 09 18:58:53 2017 +0900 @@ -184,8 +184,8 @@ \begin{figure}[htbp] \begin{center} \includegraphics[width=450pt]{fig/meta-hierarchy.pdf} - \caption{fig:meta-hierarchy} - \label{メタの階層構造} + \caption{メタの階層構造} + \label{fig:meta-hierarchy} \end{center} \end{figure} diff -r 16dc3337a5a9 -r 2bc816f4af27 paper/type.tex --- a/paper/type.tex Thu Feb 09 18:54:18 2017 +0900 +++ b/paper/type.tex Thu Feb 09 18:58:53 2017 +0900 @@ -42,7 +42,7 @@ \item 効率性 - そもそも、科学計算機における最初の型システムは Fortran~\ref{Backus:1978:HFI:960118.808380} などにおける整数と実数の算術式の区別だった。 + そもそも、科学計算機における最初の型システムは Fortran~\cite{Backus:1978:HFI:960118.808380} などにおける整数と実数の算術式の区別だった。 型の導入により、ソースからコンパイラがより最適化されたコードを生成できる。 \end{itemize}