Mercurial > hg > Papers > 2018 > nozomi-master

changeset 94:2bc816f4af27

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 18:58:53 +0900
parents 16dc3337a5a9
children fcab76b8ca58
files paper/agda.tex paper/akasha.tex paper/atton-master.pdf paper/cbc-type.tex paper/type.tex
diffstat 5 files changed, 8 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- 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 文を行なっているようなものである。
--- 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とは異なるために変換が必要である。
Binary file paper/atton-master.pdf has changed
--- 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}
 
--- 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}