Mercurial > hg > Papers > 2018 > suruga-thesis
changeset 3:8faea9c319ed
add thesis
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/Makefile Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,90 @@ +# target and root file name +TARGET = main + +# class files +CLASS_FILE = + +# figure pass +FIG_DIR = ./fig + +# ebb or extractbb +EBB = extractbb + +# dependent document files +TEX_FILES = \ + bibliography.tex \ + chapter*.tex \ + thanks.tex \ + +# dependent image files +SVG_FILES = + +# use bibtex or not (yes|no) +BIBTEX_ENABLED = no + +# commands to compile document +LATEX = platex +BIBTEX = pbibtex +DVIPDF = dvipdfmx +DVIPS = dvips + +# generated files +DVI_FILE = $(TARGET).dvi +PDF_FILE = $(TARGET).pdf +PS_FILE = $(TARGET).ps +TEX_FILES += $(TARGET).tex +EPS_FILES = $(SVG_FILES:%.svg=%.eps) +AUX_FILES = $(TEX_FILES:%.tex=%.aux) +GENERATED_FILE = \ + $(EPS_FILES) \ + $(DVI_FILE) \ + $(PDF_FILE) \ + $(AUX_FILES) \ + $(TARGET).log \ + $(TARGET).toc \ + $(TARGET).bbl \ + $(TARGET).blg \ + $(TARGET).lof \ + $(TARGET).lol \ + texput.log + +.DEFAULT_GOAL = pdf + +.PHONY : pdf +pdf : $(PDF_FILE) + open $(TARGET).pdf +$(PDF_FILE) : $(DVI_FILE) $(TEX_FILES) $(EPS_FILES) $(CLASS_FILE) + $(DVIPDF) $(TARGET) + +.PHONY : ps +ps : $(PS_FILE) +$(PS_FILE) : $(DVI_FILE) $(TEX_FILES) $(EPS_FILES) $(CLASS_FILE) + $(DVIPS) $(TARGET) + +.PHONY : dvi +dvi : $(DVI_FILE) +$(DVI_FILE) : $(TEX_FILES) $(EPS_FILES) $(CLASS_FILE) + $(LATEX) -halt-on-error $(TARGET) +ifeq ($(BIBTEX_ENABLED),yes) + $(BIBTEX) $(TARGET) +endif + $(LATEX) -halt-on-error $(TARGET) + $(LATEX) -halt-on-error $(TARGET) + +%.eps : %.svg + inkscape --export-area-drawing --without-gui --file="$<" --export-eps="$@" + +.PHONY : clean +clean: + rm -f $(GENERATED_FILE) + +.PHONY : help +help: + @echo "make dvi" + @echo " Make DVI file from tex documents." + @echo "make pdf" + @echo " Make PDF file from DVI file." + @echo "make ps" + @echo " Make PS file from DVI file." + @echo "make clean" + @echo " Remove all generated files."
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/bibliography.tex Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,30 @@ +% 参考文献 +\def\line{−\hspace*{-.7zw}−} + +\begin{thebibliography}{99} +%\bibitem{*}内の * は各自わかりやすい名前などをつけて、 +%論文中には \cite{*} のように使用する。 +%これをベースに書き換えた方が楽かも。 +%書籍、論文、URLによって若干書き方が異なる。 +%URLを載せる人は参考にした年月日を最後に記入すること。 + + \bibitem{1} + 杉本 優 : 分散フレームワーク Alice上の Meta Computation と応用, + \bibitem{2} + 大城 信康 : 分散 Database Jungle に関する研究, + \bibitem{3} + 金川 竜己 : 非破壊的木構造データベース Jungle とその評価 + \bibitem{4} + 大城 信康, 杉本 優, 河野真治 : Data Segment の分散データベースへの応用, 日本ソフトウェア科学会(2013). + +% \bibitem{gears} +% {伊波立樹, 東恩納琢偉, 河野真治}: Code Gear、Data Gear に基づく OS のプロトタイプ +% , 情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS) (2016). + +% \bibitem{llvm} +% The LLVM Compiler Infrastructure. \\\verb|http://llvm.org| + +% \bibitem{llvm_ir} +% LLVM Language Reference Manual. \\\verb|http://llvm.org/docs/LangRef.html| + +\end{thebibliography}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/chapter1.tex Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,36 @@ + \chapter{はじめに} +\label{chap:introduction} +\pagenumbering{arabic} + +% 序論の目安としては1枚半ぐらい． +\section{研究背景} +天気予報やニュース、エンタメや生活に必要なありとあらゆる情報は、インターネット上で手軽に閲覧できるようになり、また、SNSにより情報の発信も気軽にできるようになった。 +その利便性から、パソコンやスマートフォン、タブレット端末等のメディアがますます普及し、Webサービスの利用者は増大する一方で、サーバ側への負荷は増加している。 +Webサービスの負荷を減らすために、データベースには処理能力の高さ、すなわちスケーラビリティがますます求められてきている。 +データベースの処理能力を向上させるために、スケールアウトとスケールアップの方法が考えられる。 +スケールアップとは、ハードウェア的に高性能なマシンを用意することでシステムの処理能力を上げることを指す。スケールアウトとは、汎用的なマシンを複数用意し、処理を分散させることでシステムの処理能力を上げることを指す。 +単純に処理能力を上げる方法として、スケールアップは有効であるが、高性能のマシンには限界がある。コストはもちろん、そのマシン単体では処理できない程負荷がかかる可能性がある。 +それに対して、スケールアウトは、処理が重くなるたびに汎用的なマシンを順次追加していくことで性能を上げるため、ハードウェア的に高性能なマシンを用意せずにすみ、また柔軟な対応を取ることができる。よって、データベースの性能を向上させる方法として、このスケールアウトが求められている。 +本研究で扱うスケーラビリティとはスケールアウトのことを指す。 + +分散データシステムは、データの整合性 (一貫性)、常にアクセスが可能であること (可用性)、データを分散させやすいかどうか (分割耐性)、この 3 つを同時に保証するこ とは出来ない。これは CAP 定理と呼ばれる。 +一貫性と可用性を重視しているのが、現在最も使われているデータベースであるRelational Database(RDB)である。そのため、データを分割し、複数のノードにデータを分散させることが難しく、結果スケールアウトが困難になってしまうという問題がある。分断耐性を必要とする場合は、NoSQLデータベースを選択する。 + + 当研究室では、これらの問題を解決した、煩雑なデータ設計が必要ないスケーラビリ ティのあるデータベースを目指して、非破壊的木構造データベース Jungle を開発している。JungleはNoSQLを元に開発されているため、分断耐性を持っている。また、Jungle は、全体の整合性ではなく、木ごとに閉じた局所的な整合性を保証している。 整合性のある木同士をマージすることで新しい整合性のある木をす繰り出すことも 可能であるため、データの伝搬も容易である。Jungle は、これまでの開発によって木構造を格納する機能をもっている。 + +\section{研究目的} +Jungleは現在、JavaとHaskellによりそれぞれの言語で開発されている。 +本研究で扱うのはJava版である。 + + +これまでに行われた分散環境上でのJungleの性能を検証する実験では、huskellで書かれたjungleの方が、javaで書かれたjungleよりも、読み込みで 3.25 倍, 書き込みで 3.78 倍の性能が確認できた。 + +huskellは、モダンな型システムを持ち, 型推論と 型安全により、信頼性に重きを置いてプログラミングを行う関数型言語である。 +対して、Javaはコンパイラ型言語であり、構文に関してはCやC\#の影響を受けており、プログラムの処理に関してはHuskellよりもパフォーマンスが高い言語であるといえる。 +よって、javaで書かれたjungleが、huskellで書かれたjungleより性能が遅くなってしまった原因として、性能測定時に使用するテストプログラムのフロントエンドにWebサーバーJettyが使用されていたことが考えられる。 + +本研究では、新たにWebサーバーを取り除いた測定用プログラムを用いて、純粋なjava版Jungleの性能を測定する方法を提案する。 + +%\section{論文の構成} + +%\section{Introduction}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/chapter2.tex Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,46 @@ +\chapter{分散版jungleデータベース} +Jungleは、スケーラビリティのあるデータベースの開発を目指して当研究室で開発されている分散データベースである。 +現在JavaとHaskellによりそれぞれの言語で開発されており、本研究で扱うのはJava版である。 +本章では、分散データベースJungleの構造と分散部分について触れる。 +\section{Jungleデータベースの構造} +Jungleは、当研究室で開発を行っている木構造の分散データベースで、Javaを用いて実装されている。一般的なウェブサイトの構造は大体が木構造であるため、データ構造として木構造を採用している。 + +Jungleは名前付きの複数の木の集合からなり、木は複数のノードの集合でできている。ノードは自身の子のリストと属性名、属性値を持ち、データベースのレコードに相応する。通常のレコードと異なるのは、ノードに子供となる複数のノードが付くところである。 + +通常のRDBと異なり、Jungleは木構造をそのまま読み込むことができる。例えば、XMLやJsonで記述された構造を、データベースを設計することなく読み込むことが可能である。 + +また、この木を、そのままデータベースとして使用することも可能である。しかし、木の変更の手間は木の構造に依存する。特に非破壊木構造を採用しているJungleでは、木構造の変更の手間はO(1)からO(n)となりえる。つまり、アプリケーションに合わせて木を設計しない限り、十分な性能を出すことはできない。逆に、正しい木の設計を行えば高速な処理が可能である。 + +Jungleはデータの変更を非破壊で行なっており、編集ごとのデータをバージョンとしてTreeOperationLogに残している。Jungleの分散ノード間の通信は木の変更のTreeOperationLogを交換することによって、分散データベースを構成するよう設計されている。 + +\section{分散機構} +Jungleの分散機構は、木構造、すなわちツリー型を想定したネットワークトポロジーを形成し、サーバー同士を接続することで通信を行なっている。 +リング型(図\ref{fig:ring} ）やメッシュ型(図\ref{fig:mesh} ）のトポロジーでは、データの編集結果を他のサーバーノードに流す際に、流したデータが自分自身に返ってくることでループが発生してしまう可能性がある。 +ツリー型であれば、閉路がない状態でサーバーノード同士を繋げることができる為、編集履歴の結果を他のサーバーノードに流すだけですみ、結果ループを防ぐことができる(図\ref{fig:tree}）。 + +\begin{figure}[H] + \centering + \includegraphics[width=100mm]{pic/ring.pdf} + \caption{ring型のトポロジー} + \label{fig:ring} +\end{figure} + +\begin{figure}[H] + \centering + \includegraphics[width=100mm]{pic/mesh.pdf} + \caption{メッシュ型のトポロジー} + \label{fig:mesh} +\end{figure} + +\begin{figure}[H] + \centering + \includegraphics[width=100mm]{pic/tree.pdf} + \caption{ツリー型のトポロジー} + \label{fig:tree} +\end{figure} + +ネットワークトポロジーは、当研究室で開発している並列分散フレームワークであるAliceが提供する、TopologyManagerという機能を用いて構成されている。 + +また、データ分散の為には、どのデータをネットワークに流すのか決めなければならない。そこで、TreeOperationLogを使用する。前セクションでも述べたが、TreeOperationLogには、どのNodeにどのような操作をしたのかという、データ編集の履歴情報が入っている。 +このTreeOperationLogをAliceを用いて他のサーバーノードに送り、データの編集をしてもらうことで、同じデータをもつことが可能になる。 +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/chapter3.tex Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,94 @@ +\chapter{評価実験} +本研究は、Jungleの分散環境上での性能を正しく評価するための実験を行う。 +本章では実験の概要について述べる。 +まず、本研究の目的について述べ、 +次に、分散フレームワーク Aliceによる、本研究の分散機構を構成する方法について述べる。 +次に、木構造上に立ち上げたJungleを制御するジョブスケジューラーであるTORQUEについて述べる。 +最後に、本実験の測定用プログラムについて述べる。 +\section{実験目的} +これまでの分散環境上でのJungleの性能を測定する実験で使われたテストプログラムは、フロントエンドにJettyというWebサーバーが使われていた。 +しかし、この測定方法では、Webサーバーが仲介した測定結果となってしまい、純粋なJungleの性能を測定できないという問題がある。 +そこで、Webサーバーを取り除き、純粋なJungleの性能を測定するテストプログラムを作成する。 + +テストプログラムは、木構造における子ノードに、データを複数書き込む機能を提供する。 +末端の複数の子ノードにデータをそれぞれ書き込み、最終的にrootノードへデータをmergeしていく(図\ref{fig:logupdatetest} ）。 + +測定範囲は、 +\begin{itemize} + \item 末端ノードからrootノードへデータが到達する時間 + \item 末端Jungleからrootノードを介して別の末端ノードへデータが到達する時間 +\end{itemize} +の２点を計測する予定である。 +\begin{figure}[H] + \centering + \includegraphics[width=100mm]{pic/logupdatetest.pdf} + \caption{テストプログラムによるJungleの性能測定} + \label{fig:logupdatetest} +\end{figure} + +\newpage + + +\section{分散フレームワーク Alice による分散環境の構築} +本研究では、分散環境上でのJungleの性能を確認する為、VM32台分のサーバーノードを用意し、それぞれでJungleを起動することで、Jungle間で通信をする環境をつくる。 +Jungleを起動したサーバーノード間の通信部分を、当研究室で開発している並列分散フレームワークAlice[1]にて再現する。 + +Aliceには、ネットワークのトポロジーを構成するTopologyManager[2]という機能が備わっている。TopologyManagerに参加表明をしたサーバーノードに順番に、接続先のサーバーノードのIPアドレス、ポート番号、接続名を送り、受け取ったサーバーノードはそれらに従って接続する。 +今回、TopologyManagerはJungleをのせたVM32台分のサーバーノードを、木構造を形成するように采配する（図\ref{fig:topologymanager} ）。 + +トポロジー構成後、Jungle間の通信でのデータ形式にはTreeOperationLogを利用する。TreeOperationLogには、ノードの編集の履歴などの情報が入っている。TreeOperationLogをAliceによって他のJungleへ送ることで、送信元のJungleと同じ編集を行う。こうして、Jungle間でのデータの同期を可能にしている。 +\begin{figure}[H] + \centering + \includegraphics[width=70mm]{pic/topologymanager.pdf} + \caption{AliceによるJungleの木構造トポロジーの形成} + \label{fig:topologymanager} +\end{figure} + +\newpage +\section{TORQUE Resource Manager} +分散環境上でのJungleの性能を測定するにあたり、VM32台にJungleを起動させた後、それぞれでデータを書き込むプログラムを動作させる。プログラムを起動する順番やタイミングは、TORQUE Resource Managerというジョブスケジューラーによって管理する。 + +TORQUE Resource Manager は、ジョブを管理・投下・実行する３つのデーモンで構成されており、 +ジョブの管理・投下を担うデーモンが稼働しているヘッダーノードから、ジョブの実行を担うデーモンが稼働している計算ノードへジョブが投下される（図\ref{fig:torque} ）。 + \begin{figure}[ht] + \begin{center} + \includegraphics[width=100mm]{./pic/torque.pdf} + \end{center} + \caption{TORQUEの構成} + \label{fig:torque} +\end{figure} + +ユーザーはジョブを記述したシェルスクリプトを用意し、スケジューラーに投入する。その際に、利用したいマシン数やCPUコア数を指定する。TORQUEは、ジョブに必要なマシンが揃い次第、受け取ったジョブを実行する。 + +\newpage + +\section{Jungleの分散性能測定用テストプログラム} +これまでの分散環境上でのJungleの性能を測定する実験で使われたテストプログラムは、フロントエンドにJettyというWebサーバーが使われていた。 +しかし、Webサーバーが仲介した測定結果となってしまい、純粋なJungleの性能を測定できないという問題がある。 +そこで、Webサーバーを取り除き、これまでの研究により純粋にJungleの性能を測定するテストプログラムを作成する。 + +テストプログラムは、木構造における子ノードに、データを複数書き込む機能を提供する。 +末端の複数の子ノードにデータをそれぞれ書き込み、最終的にrootノードへデータをmergeしていく(図\ref{fig:logupdatetest} ）。 + +測定範囲は、 +\begin{itemize} + \item 末端ノードからrootノードへデータが到達する時間 + \item 末端Jungleからrootノードを介して別の末端ノードへデータが到達する時間 +\end{itemize} +の２点を計測する予定である。 +\begin{figure}[H] + \centering + \includegraphics[width=100mm]{pic/logupdatetest.pdf} + \caption{TestプログラムによるJungleの性能測定} + \label{fig:logupdatetest} +\end{figure} + +\section{LogupdateTree.sh} +LogupdateTree.shは、Aliceのトポロジーマネージャー起動後、引数で渡した数の分だけnodeを立ち上げる。複数のnodeのうち、１つをルートノードとして立ち上げ、残りを子ノードとして、ルートノードの下にツリー上に接続されていく。(図\ref{fig:LogupdateTree.pdf}) +\begin{figure}[H] + \centering + \includegraphics[width=100mm]{pic/LogupdateTree.pdf} + \caption{ルートノードと子ノードによって構成されるツリー構造} + \label{fig:LogupdateTree.pdf} +\end{figure} +\section{killLogupdate.sh}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/chapter4.tex Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,19 @@ +%比較実験は間に合わないかもしれない +%もしかしたら、本当に結果だけ出して、手法として紹介する...? +\chapter{性能評価} +\section{java版jungleとhuskell版jungleの比較} + + +\section{java版jungleの分散性能の評価} + + +\section{性能測定方法の評価} + + + + +\newpage + + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/chapter5.tex Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,6 @@ +% 今後の課題 +\chapter{結論} +\section{まとめ} + +\section{今後の課題} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/chapter6.tex Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,1 @@ +%
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/main.aux Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,52 @@ +\relax +\@writefile{toc}{\contentsline {chapter}{\numberline {第1章}はじめに}{1}} +\@writefile{lof}{\addvspace {10\p@ }} +\@writefile{lot}{\addvspace {10\p@ }} +\newlabel{chap:introduction}{{1}{1}} +\@writefile{toc}{\contentsline {section}{\numberline {1.1}研究背景}{1}} +\@writefile{toc}{\contentsline {section}{\numberline {1.2}研究目的}{2}} +\@writefile{toc}{\contentsline {chapter}{\numberline {第2章}分散版jungleデータベース}{3}} +\@writefile{lof}{\addvspace {10\p@ }} +\@writefile{lot}{\addvspace {10\p@ }} +\@writefile{toc}{\contentsline {section}{\numberline {2.1}Jungleデータベースの構造}{3}} +\@writefile{toc}{\contentsline {section}{\numberline {2.2}分散機構}{3}} +\@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces ring型のトポロジー}}{4}} +\newlabel{fig:ring}{{2.1}{4}} +\@writefile{lof}{\contentsline {figure}{\numberline {2.2}{\ignorespaces メッシュ型のトポロジー}}{4}} +\newlabel{fig:mesh}{{2.2}{4}} +\@writefile{lof}{\contentsline {figure}{\numberline {2.3}{\ignorespaces ツリー型のトポロジー}}{5}} +\newlabel{fig:tree}{{2.3}{5}} +\@writefile{toc}{\contentsline {chapter}{\numberline {第3章}評価実験}{6}} +\@writefile{lof}{\addvspace {10\p@ }} +\@writefile{lot}{\addvspace {10\p@ }} +\@writefile{toc}{\contentsline {section}{\numberline {3.1}実験目的}{6}} +\@writefile{lof}{\contentsline {figure}{\numberline {3.1}{\ignorespaces テストプログラムによるJungleの性能測定}}{7}} +\newlabel{fig:logupdatetest}{{3.1}{7}} +\@writefile{toc}{\contentsline {section}{\numberline {3.2}分散フレームワーク Alice による分散環境の構築}{8}} +\@writefile{lof}{\contentsline {figure}{\numberline {3.2}{\ignorespaces AliceによるJungleの木構造トポロジーの形成}}{8}} +\newlabel{fig:topologymanager}{{3.2}{8}} +\@writefile{toc}{\contentsline {section}{\numberline {3.3}TORQUE Resource Manager}{9}} +\@writefile{lof}{\contentsline {figure}{\numberline {3.3}{\ignorespaces TORQUEの構成}}{9}} +\newlabel{fig:torque}{{3.3}{9}} +\@writefile{toc}{\contentsline {section}{\numberline {3.4}Jungleの分散性能測定用テストプログラム}{10}} +\@writefile{lof}{\contentsline {figure}{\numberline {3.4}{\ignorespaces TestプログラムによるJungleの性能測定}}{10}} +\newlabel{fig:logupdatetest}{{3.4}{10}} +\@writefile{toc}{\contentsline {section}{\numberline {3.5}LogupdateTree.sh}{10}} +\@writefile{lof}{\contentsline {figure}{\numberline {3.5}{\ignorespaces ルートノードと子ノードによって構成されるツリー構造}}{11}} +\newlabel{fig:LogupdateTree.pdf}{{3.5}{11}} +\@writefile{toc}{\contentsline {section}{\numberline {3.6}killLogupdate.sh}{11}} +\@writefile{toc}{\contentsline {chapter}{\numberline {第4章}性能評価}{12}} +\@writefile{lof}{\addvspace {10\p@ }} +\@writefile{lot}{\addvspace {10\p@ }} +\@writefile{toc}{\contentsline {section}{\numberline {4.1}java版jungleとhuskell版jungleの比較}{12}} +\@writefile{toc}{\contentsline {section}{\numberline {4.2}java版jungleの分散性能の評価}{12}} +\@writefile{toc}{\contentsline {section}{\numberline {4.3}性能測定方法の評価}{12}} +\@writefile{toc}{\contentsline {chapter}{\numberline {第5章}結論}{13}} +\@writefile{lof}{\addvspace {10\p@ }} +\@writefile{lot}{\addvspace {10\p@ }} +\@writefile{toc}{\contentsline {section}{\numberline {5.1}まとめ}{13}} +\@writefile{toc}{\contentsline {section}{\numberline {5.2}今後の課題}{13}} +\bibcite{1}{1} +\bibcite{2}{2} +\bibcite{3}{3} +\bibcite{4}{4}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/main.lof Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,13 @@ +\addvspace {10\p@ } +\addvspace {10\p@ } +\contentsline {figure}{\numberline {2.1}{\ignorespaces ring型のトポロジー}}{4} +\contentsline {figure}{\numberline {2.2}{\ignorespaces メッシュ型のトポロジー}}{4} +\contentsline {figure}{\numberline {2.3}{\ignorespaces ツリー型のトポロジー}}{5} +\addvspace {10\p@ } +\contentsline {figure}{\numberline {3.1}{\ignorespaces テストプログラムによるJungleの性能測定}}{7} +\contentsline {figure}{\numberline {3.2}{\ignorespaces AliceによるJungleの木構造トポロジーの形成}}{8} +\contentsline {figure}{\numberline {3.3}{\ignorespaces TORQUEの構成}}{9} +\contentsline {figure}{\numberline {3.4}{\ignorespaces TestプログラムによるJungleの性能測定}}{10} +\contentsline {figure}{\numberline {3.5}{\ignorespaces ルートノードと子ノードによって構成されるツリー構造}}{11} +\addvspace {10\p@ } +\addvspace {10\p@ }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/main.log Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,656 @@ +This is e-pTeX, Version 3.14159265-p3.7.1-161114-2.6 (utf8.euc) (TeX Live 2017) (preloaded format=platex 2017.10.20) 11 FEB 2018 03:06 +entering extended mode + restricted \write18 enabled. + %&-line parsing enabled. +**main +(./main.tex +pLaTeX2e <2017/05/05> (based on LaTeX2e <2017-04-15>) +Babel <3.10> and hyphenation patterns for 84 language(s) loaded. +(/usr/local/texlive/2017/texmf-dist/tex/platex/base/jreport.cls +Document Class: jreport 2017/03/05 v1.7e Standard pLaTeX class +\c@@paper=\count82 +(/usr/local/texlive/2017/texmf-dist/tex/platex/base/jsize12.clo +File: jsize12.clo 2017/03/05 v1.7e Standard pLaTeX file (size option) +) +\c@part=\count83 +\c@chapter=\count84 +\c@section=\count85 +\c@subsection=\count86 +\c@subsubsection=\count87 +\c@paragraph=\count88 +\c@subparagraph=\count89 +\c@figure=\count90 +\c@table=\count91 +\abovecaptionskip=\skip41 +\belowcaptionskip=\skip42 +\symmincho=\mathgroup4 +LaTeX Font Info: Overwriting symbol font `mincho' in version `bold' +(Font) JY1/mc/m/n --> JY1/gt/m/n on input line 702. +\toclineskip=\dimen118 +\@lnumwidth=\dimen119 +\bibindent=\dimen120 +\heisei=\count92 +) +(/usr/local/texlive/2017/texmf-dist/tex/latex/graphics/graphicx.sty +Package: graphicx 2014/10/28 v1.0g Enhanced LaTeX Graphics (DPC,SPQR) + +(/usr/local/texlive/2017/texmf-dist/tex/latex/graphics/keyval.sty +Package: keyval 2014/10/28 v1.15 key=value parser (DPC) +\KV@toks@=\toks15 +) +(/usr/local/texlive/2017/texmf-dist/tex/latex/graphics/graphics.sty +Package: graphics 2017/04/14 v1.1b Standard LaTeX Graphics (DPC,SPQR) + +(/usr/local/texlive/2017/texmf-dist/tex/latex/graphics/trig.sty +Package: trig 2016/01/03 v1.10 sin cos tan (DPC) +) +(/usr/local/texlive/2017/texmf-dist/tex/latex/graphics-cfg/graphics.cfg +File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration +) +Package graphics Info: Driver file: dvipdfmx.def on input line 99. + +(/usr/local/texlive/2017/texmf-dist/tex/latex/graphics-def/dvipdfmx.def +File: dvipdfmx.def 2016/07/11 v4.12 LaTeX color/graphics driver for dvipdfmx (L +3/ChoF) +)) +\Gin@req@height=\dimen121 +\Gin@req@width=\dimen122 +) +(./mythesis.sty) +(/usr/local/texlive/2017/texmf-dist/tex/latex/bussproofs/bussproofs.sty +Proof Tree (bussproofs) style macros. Version 1.1. +\theLevel=\count93 +\myMaxLevel=\count94 +\myBoxA=\box42 +\myBoxB=\box43 +\myBoxC=\box44 +\myBoxD=\box45 +\myBoxLL=\box46 +\myBoxRL=\box47 +\thisAboveSkip=\dimen123 +\thisBelowSkip=\dimen124 +\newScoreStart=\dimen125 +\newScoreEnd=\dimen126 +\newCenter=\dimen127 +\displace=\dimen128 +\leftLowerAmt=\dimen129 +\rightLowerAmt=\dimen130 +\scoreHeight=\dimen131 +\scoreDepth=\dimen132 +\htLbox=\dimen133 +\htRbox=\dimen134 +\htRRbox=\dimen135 +\htRRRbox=\dimen136 +\htAbox=\dimen137 +\htCbox=\dimen138 +) (/usr/local/texlive/2017/texmf-dist/tex/latex/multirow/multirow.sty +Package: multirow 2016/11/25 v2.2 Span multiple rows of a table +\multirow@colwidth=\skip43 +\multirow@cntb=\count95 +\multirow@dima=\skip44 +\bigstrutjot=\dimen139 +) +(/usr/local/texlive/2017/texmf-dist/tex/latex/here/here.sty) +(/usr/local/texlive/2017/texmf-dist/tex/latex/float/float.sty +Package: float 2001/11/08 v1.3d Float enhancements (AL) +\c@float@type=\count96 +\float@exts=\toks16 +\float@box=\box48 +\@float@everytoks=\toks17 +\@floatcapt=\box49 +) +(/usr/local/texlive/2017/texmf-dist/tex/latex/listings/listings.sty +\lst@mode=\count97 +\lst@gtempboxa=\box50 +\lst@token=\toks18 +\lst@length=\count98 +\lst@currlwidth=\dimen140 +\lst@column=\count99 +\lst@pos=\count100 +\lst@lostspace=\dimen141 +\lst@width=\dimen142 +\lst@newlines=\count101 +\lst@lineno=\count102 +\lst@maxwidth=\dimen143 + +(/usr/local/texlive/2017/texmf-dist/tex/latex/listings/lstmisc.sty +File: lstmisc.sty 2015/06/04 1.6 (Carsten Heinz) +\c@lstnumber=\count103 +\lst@skipnumbers=\count104 +\lst@framebox=\box51 +) +(/usr/local/texlive/2017/texmf-dist/tex/latex/listings/listings.cfg +File: listings.cfg 2015/06/04 1.6 listings configuration +)) +Package: listings 2015/06/04 1.6 (Carsten Heinz) + +(/usr/local/texlive/2017/texmf-dist/tex/latex/url/url.sty +\Urlmuskip=\muskip10 +Package: url 2013/09/16 ver 3.4 Verb mode for urls, etc. +) +(/usr/local/texlive/2017/texmf-dist/tex/latex/cite/cite.sty +LaTeX Info: Redefining \cite on input line 302. +LaTeX Info: Redefining \nocite on input line 332. +Package: cite 2015/02/27 v 5.5 +) +(/usr/local/texlive/2017/texmf-dist/tex/latex/amsfonts/amssymb.sty +Package: amssymb 2013/01/14 v3.01 AMS font symbols + +(/usr/local/texlive/2017/texmf-dist/tex/latex/amsfonts/amsfonts.sty +Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support +\@emptytoks=\toks19 +\symAMSa=\mathgroup5 +\symAMSb=\mathgroup6 +LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold' +(Font) U/euf/m/n --> U/euf/b/n on input line 106. +)) +(/usr/local/texlive/2017/texmf-dist/tex/latex/amsmath/amsmath.sty +Package: amsmath 2016/11/05 v2.16a AMS math features +\@mathmargin=\skip45 + +For additional information on amsmath, use the `?' option. +(/usr/local/texlive/2017/texmf-dist/tex/latex/amsmath/amstext.sty +Package: amstext 2000/06/29 v2.01 AMS text + +(/usr/local/texlive/2017/texmf-dist/tex/latex/amsmath/amsgen.sty +File: amsgen.sty 1999/11/30 v2.0 generic functions +\@emptytoks=\toks20 +\ex@=\dimen144 +)) +(/usr/local/texlive/2017/texmf-dist/tex/latex/amsmath/amsbsy.sty +Package: amsbsy 1999/11/29 v1.2d Bold Symbols +\pmbraise@=\dimen145 +) +(/usr/local/texlive/2017/texmf-dist/tex/latex/amsmath/amsopn.sty +Package: amsopn 2016/03/08 v2.02 operator names +) +\inf@bad=\count105 +LaTeX Info: Redefining \frac on input line 213. +\uproot@=\count106 +\leftroot@=\count107 +LaTeX Info: Redefining \overline on input line 375. +\classnum@=\count108 +\DOTSCASE@=\count109 +LaTeX Info: Redefining \ldots on input line 472. +LaTeX Info: Redefining \dots on input line 475. +LaTeX Info: Redefining \cdots on input line 596. +\Mathstrutbox@=\box52 +\strutbox@=\box53 +\big@size=\dimen146 +LaTeX Font Info: Redeclaring font encoding OML on input line 712. +LaTeX Font Info: Redeclaring font encoding OMS on input line 713. +\macc@depth=\count110 +\c@MaxMatrixCols=\count111 +\dotsspace@=\muskip11 +\c@parentequation=\count112 +\dspbrk@lvl=\count113 +\tag@help=\toks21 +\row@=\count114 +\column@=\count115 +\maxfields@=\count116 +\andhelp@=\toks22 +\eqnshift@=\dimen147 +\alignsep@=\dimen148 +\tagshift@=\dimen149 +\tagwidth@=\dimen150 +\totwidth@=\dimen151 +\lineht@=\dimen152 +\@envbody=\toks23 +\multlinegap=\skip46 +\multlinetaggap=\skip47 +\mathdisplay@stack=\toks24 +LaTeX Info: Redefining \[ on input line 2817. +LaTeX Info: Redefining \] on input line 2818. +) +(/usr/local/texlive/2017/texmf-dist/tex/latex/base/inputenc.sty +Package: inputenc 2015/03/17 v1.2c Input encoding file +\inpenc@prehook=\toks25 +\inpenc@posthook=\toks26 + +(/usr/local/texlive/2017/texmf-dist/tex/latex/base/utf8.def +File: utf8.def 2017/01/28 v1.1t UTF-8 support for inputenc +Now handling font encoding OML ... +... no UTF-8 mapping file for font encoding OML +Now handling font encoding T1 ... +... processing UTF-8 mapping file for font encoding T1 + +(/usr/local/texlive/2017/texmf-dist/tex/latex/base/t1enc.dfu +File: t1enc.dfu 2017/01/28 v1.1t UTF-8 support for inputenc + defining Unicode char U+00A0 (decimal 160) + defining Unicode char U+00A1 (decimal 161) + defining Unicode char U+00A3 (decimal 163) + defining Unicode char U+00AB (decimal 171) + defining Unicode char U+00AD (decimal 173) + defining Unicode char U+00BB (decimal 187) + defining Unicode char U+00BF (decimal 191) + defining Unicode char U+00C0 (decimal 192) + defining Unicode char U+00C1 (decimal 193) + defining Unicode char U+00C2 (decimal 194) + defining Unicode char U+00C3 (decimal 195) + defining Unicode char U+00C4 (decimal 196) + defining Unicode char U+00C5 (decimal 197) + defining Unicode char U+00C6 (decimal 198) + defining Unicode char U+00C7 (decimal 199) + defining Unicode char U+00C8 (decimal 200) + defining Unicode char U+00C9 (decimal 201) + defining Unicode char U+00CA (decimal 202) + defining Unicode char U+00CB (decimal 203) + defining Unicode char U+00CC (decimal 204) + defining Unicode char U+00CD (decimal 205) + defining Unicode char U+00CE (decimal 206) + defining Unicode char U+00CF (decimal 207) + defining Unicode char U+00D0 (decimal 208) + defining Unicode char U+00D1 (decimal 209) + defining Unicode char U+00D2 (decimal 210) + defining Unicode char U+00D3 (decimal 211) + defining Unicode char U+00D4 (decimal 212) + defining Unicode char U+00D5 (decimal 213) + defining Unicode char U+00D6 (decimal 214) + defining Unicode char U+00D8 (decimal 216) + defining Unicode char U+00D9 (decimal 217) + defining Unicode char U+00DA (decimal 218) + defining Unicode char U+00DB (decimal 219) + defining Unicode char U+00DC (decimal 220) + defining Unicode char U+00DD (decimal 221) + defining Unicode char U+00DE (decimal 222) + defining Unicode char U+00DF (decimal 223) + defining Unicode char U+00E0 (decimal 224) + defining Unicode char U+00E1 (decimal 225) + defining Unicode char U+00E2 (decimal 226) + defining Unicode char U+00E3 (decimal 227) + defining Unicode char U+00E4 (decimal 228) + defining Unicode char U+00E5 (decimal 229) + defining Unicode char U+00E6 (decimal 230) + defining Unicode char U+00E7 (decimal 231) + defining Unicode char U+00E8 (decimal 232) + defining Unicode char U+00E9 (decimal 233) + defining Unicode char U+00EA (decimal 234) + defining Unicode char U+00EB (decimal 235) + defining Unicode char U+00EC (decimal 236) + defining Unicode char U+00ED (decimal 237) + defining Unicode char U+00EE (decimal 238) + defining Unicode char U+00EF (decimal 239) + defining Unicode char U+00F0 (decimal 240) + defining Unicode char U+00F1 (decimal 241) + defining Unicode char U+00F2 (decimal 242) + defining Unicode char U+00F3 (decimal 243) + defining Unicode char U+00F4 (decimal 244) + defining Unicode char U+00F5 (decimal 245) + defining Unicode char U+00F6 (decimal 246) + defining Unicode char U+00F8 (decimal 248) + defining Unicode char U+00F9 (decimal 249) + defining Unicode char U+00FA (decimal 250) + defining Unicode char U+00FB (decimal 251) + defining Unicode char U+00FC (decimal 252) + defining Unicode char U+00FD (decimal 253) + defining Unicode char U+00FE (decimal 254) + defining Unicode char U+00FF (decimal 255) + defining Unicode char U+0100 (decimal 256) + defining Unicode char U+0101 (decimal 257) + defining Unicode char U+0102 (decimal 258) + defining Unicode char U+0103 (decimal 259) + defining Unicode char U+0104 (decimal 260) + defining Unicode char U+0105 (decimal 261) + defining Unicode char U+0106 (decimal 262) + defining Unicode char U+0107 (decimal 263) + defining Unicode char U+0108 (decimal 264) + defining Unicode char U+0109 (decimal 265) + defining Unicode char U+010A (decimal 266) + defining Unicode char U+010B (decimal 267) + defining Unicode char U+010C (decimal 268) + defining Unicode char U+010D (decimal 269) + defining Unicode char U+010E (decimal 270) + defining Unicode char U+010F (decimal 271) + defining Unicode char U+0110 (decimal 272) + defining Unicode char U+0111 (decimal 273) + defining Unicode char U+0112 (decimal 274) + defining Unicode char U+0113 (decimal 275) + defining Unicode char U+0114 (decimal 276) + defining Unicode char U+0115 (decimal 277) + defining Unicode char U+0116 (decimal 278) + defining Unicode char U+0117 (decimal 279) + defining Unicode char U+0118 (decimal 280) + defining Unicode char U+0119 (decimal 281) + defining Unicode char U+011A (decimal 282) + defining Unicode char U+011B (decimal 283) + defining Unicode char U+011C (decimal 284) + defining Unicode char U+011D (decimal 285) + defining Unicode char U+011E (decimal 286) + defining Unicode char U+011F (decimal 287) + defining Unicode char U+0120 (decimal 288) + defining Unicode char U+0121 (decimal 289) + defining Unicode char U+0122 (decimal 290) + defining Unicode char U+0123 (decimal 291) + defining Unicode char U+0124 (decimal 292) + defining Unicode char U+0125 (decimal 293) + defining Unicode char U+0128 (decimal 296) + defining Unicode char U+0129 (decimal 297) + defining Unicode char U+012A (decimal 298) + defining Unicode char U+012B (decimal 299) + defining Unicode char U+012C (decimal 300) + defining Unicode char U+012D (decimal 301) + defining Unicode char U+012E (decimal 302) + defining Unicode char U+012F (decimal 303) + defining Unicode char U+0130 (decimal 304) + defining Unicode char U+0131 (decimal 305) + defining Unicode char U+0132 (decimal 306) + defining Unicode char U+0133 (decimal 307) + defining Unicode char U+0134 (decimal 308) + defining Unicode char U+0135 (decimal 309) + defining Unicode char U+0136 (decimal 310) + defining Unicode char U+0137 (decimal 311) + defining Unicode char U+0139 (decimal 313) + defining Unicode char U+013A (decimal 314) + defining Unicode char U+013B (decimal 315) + defining Unicode char U+013C (decimal 316) + defining Unicode char U+013D (decimal 317) + defining Unicode char U+013E (decimal 318) + defining Unicode char U+0141 (decimal 321) + defining Unicode char U+0142 (decimal 322) + defining Unicode char U+0143 (decimal 323) + defining Unicode char U+0144 (decimal 324) + defining Unicode char U+0145 (decimal 325) + defining Unicode char U+0146 (decimal 326) + defining Unicode char U+0147 (decimal 327) + defining Unicode char U+0148 (decimal 328) + defining Unicode char U+014A (decimal 330) + defining Unicode char U+014B (decimal 331) + defining Unicode char U+014C (decimal 332) + defining Unicode char U+014D (decimal 333) + defining Unicode char U+014E (decimal 334) + defining Unicode char U+014F (decimal 335) + defining Unicode char U+0150 (decimal 336) + defining Unicode char U+0151 (decimal 337) + defining Unicode char U+0152 (decimal 338) + defining Unicode char U+0153 (decimal 339) + defining Unicode char U+0154 (decimal 340) + defining Unicode char U+0155 (decimal 341) + defining Unicode char U+0156 (decimal 342) + defining Unicode char U+0157 (decimal 343) + defining Unicode char U+0158 (decimal 344) + defining Unicode char U+0159 (decimal 345) + defining Unicode char U+015A (decimal 346) + defining Unicode char U+015B (decimal 347) + defining Unicode char U+015C (decimal 348) + defining Unicode char U+015D (decimal 349) + defining Unicode char U+015E (decimal 350) + defining Unicode char U+015F (decimal 351) + defining Unicode char U+0160 (decimal 352) + defining Unicode char U+0161 (decimal 353) + defining Unicode char U+0162 (decimal 354) + defining Unicode char U+0163 (decimal 355) + defining Unicode char U+0164 (decimal 356) + defining Unicode char U+0165 (decimal 357) + defining Unicode char U+0168 (decimal 360) + defining Unicode char U+0169 (decimal 361) + defining Unicode char U+016A (decimal 362) + defining Unicode char U+016B (decimal 363) + defining Unicode char U+016C (decimal 364) + defining Unicode char U+016D (decimal 365) + defining Unicode char U+016E (decimal 366) + defining Unicode char U+016F (decimal 367) + defining Unicode char U+0170 (decimal 368) + defining Unicode char U+0171 (decimal 369) + defining Unicode char U+0172 (decimal 370) + defining Unicode char U+0173 (decimal 371) + defining Unicode char U+0174 (decimal 372) + defining Unicode char U+0175 (decimal 373) + defining Unicode char U+0176 (decimal 374) + defining Unicode char U+0177 (decimal 375) + defining Unicode char U+0178 (decimal 376) + defining Unicode char U+0179 (decimal 377) + defining Unicode char U+017A (decimal 378) + defining Unicode char U+017B (decimal 379) + defining Unicode char U+017C (decimal 380) + defining Unicode char U+017D (decimal 381) + defining Unicode char U+017E (decimal 382) + defining Unicode char U+01CD (decimal 461) + defining Unicode char U+01CE (decimal 462) + defining Unicode char U+01CF (decimal 463) + defining Unicode char U+01D0 (decimal 464) + defining Unicode char U+01D1 (decimal 465) + defining Unicode char U+01D2 (decimal 466) + defining Unicode char U+01D3 (decimal 467) + defining Unicode char U+01D4 (decimal 468) + defining Unicode char U+01E2 (decimal 482) + defining Unicode char U+01E3 (decimal 483) + defining Unicode char U+01E6 (decimal 486) + defining Unicode char U+01E7 (decimal 487) + defining Unicode char U+01E8 (decimal 488) + defining Unicode char U+01E9 (decimal 489) + defining Unicode char U+01EA (decimal 490) + defining Unicode char U+01EB (decimal 491) + defining Unicode char U+01F0 (decimal 496) + defining Unicode char U+01F4 (decimal 500) + defining Unicode char U+01F5 (decimal 501) + defining Unicode char U+0218 (decimal 536) + defining Unicode char U+0219 (decimal 537) + defining Unicode char U+021A (decimal 538) + defining Unicode char U+021B (decimal 539) + defining Unicode char U+0232 (decimal 562) + defining Unicode char U+0233 (decimal 563) + defining Unicode char U+1E02 (decimal 7682) + defining Unicode char U+1E03 (decimal 7683) + defining Unicode char U+200C (decimal 8204) + defining Unicode char U+2010 (decimal 8208) + defining Unicode char U+2011 (decimal 8209) + defining Unicode char U+2012 (decimal 8210) + defining Unicode char U+2013 (decimal 8211) + defining Unicode char U+2014 (decimal 8212) + defining Unicode char U+2015 (decimal 8213) + defining Unicode char U+2018 (decimal 8216) + defining Unicode char U+2019 (decimal 8217) + defining Unicode char U+201A (decimal 8218) + defining Unicode char U+201C (decimal 8220) + defining Unicode char U+201D (decimal 8221) + defining Unicode char U+201E (decimal 8222) + defining Unicode char U+2030 (decimal 8240) + defining Unicode char U+2031 (decimal 8241) + defining Unicode char U+2039 (decimal 8249) + defining Unicode char U+203A (decimal 8250) + defining Unicode char U+2423 (decimal 9251) + defining Unicode char U+1E20 (decimal 7712) + defining Unicode char U+1E21 (decimal 7713) +) +Now handling font encoding OT1 ... +... processing UTF-8 mapping file for font encoding OT1 + +(/usr/local/texlive/2017/texmf-dist/tex/latex/base/ot1enc.dfu +File: ot1enc.dfu 2017/01/28 v1.1t UTF-8 support for inputenc + defining Unicode char U+00A0 (decimal 160) + defining Unicode char U+00A1 (decimal 161) + defining Unicode char U+00A3 (decimal 163) + defining Unicode char U+00AD (decimal 173) + defining Unicode char U+00B8 (decimal 184) + defining Unicode char U+00BF (decimal 191) + defining Unicode char U+00C5 (decimal 197) + defining Unicode char U+00C6 (decimal 198) + defining Unicode char U+00D8 (decimal 216) + defining Unicode char U+00DF (decimal 223) + defining Unicode char U+00E6 (decimal 230) + defining Unicode char U+00EC (decimal 236) + defining Unicode char U+00ED (decimal 237) + defining Unicode char U+00EE (decimal 238) + defining Unicode char U+00EF (decimal 239) + defining Unicode char U+00F8 (decimal 248) + defining Unicode char U+0131 (decimal 305) + defining Unicode char U+0141 (decimal 321) + defining Unicode char U+0142 (decimal 322) + defining Unicode char U+0152 (decimal 338) + defining Unicode char U+0153 (decimal 339) + defining Unicode char U+0174 (decimal 372) + defining Unicode char U+0175 (decimal 373) + defining Unicode char U+0176 (decimal 374) + defining Unicode char U+0177 (decimal 375) + defining Unicode char U+0218 (decimal 536) + defining Unicode char U+0219 (decimal 537) + defining Unicode char U+021A (decimal 538) + defining Unicode char U+021B (decimal 539) + defining Unicode char U+2013 (decimal 8211) + defining Unicode char U+2014 (decimal 8212) + defining Unicode char U+2018 (decimal 8216) + defining Unicode char U+2019 (decimal 8217) + defining Unicode char U+201C (decimal 8220) + defining Unicode char U+201D (decimal 8221) +) +Now handling font encoding OMS ... +... processing UTF-8 mapping file for font encoding OMS + +(/usr/local/texlive/2017/texmf-dist/tex/latex/base/omsenc.dfu +File: omsenc.dfu 2017/01/28 v1.1t UTF-8 support for inputenc + defining Unicode char U+00A7 (decimal 167) + defining Unicode char U+00B6 (decimal 182) + defining Unicode char U+00B7 (decimal 183) + defining Unicode char U+2020 (decimal 8224) + defining Unicode char U+2021 (decimal 8225) + defining Unicode char U+2022 (decimal 8226) +) +Now handling font encoding OMX ... +... no UTF-8 mapping file for font encoding OMX +Now handling font encoding U ... +... no UTF-8 mapping file for font encoding U +Now handling font encoding JY1 ... +... no UTF-8 mapping file for font encoding JY1 +Now handling font encoding JT1 ... +... no UTF-8 mapping file for font encoding JT1 + defining Unicode char U+00A9 (decimal 169) + defining Unicode char U+00AA (decimal 170) + defining Unicode char U+00AE (decimal 174) + defining Unicode char U+00BA (decimal 186) + defining Unicode char U+02C6 (decimal 710) + defining Unicode char U+02DC (decimal 732) + defining Unicode char U+200C (decimal 8204) + defining Unicode char U+2026 (decimal 8230) + defining Unicode char U+2122 (decimal 8482) + defining Unicode char U+2423 (decimal 9251) +)) (./main.aux + +LaTeX Warning: Label `fig:logupdatetest' multiply defined. + +) +\openout1 = `main.aux'. + +LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 77. +LaTeX Font Info: ... okay on input line 77. +LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 77. +LaTeX Font Info: ... okay on input line 77. +LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 77. +LaTeX Font Info: ... okay on input line 77. +LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 77. +LaTeX Font Info: ... okay on input line 77. +LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 77. +LaTeX Font Info: ... okay on input line 77. +LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 77. +LaTeX Font Info: ... okay on input line 77. +LaTeX Font Info: Checking defaults for JY1/mc/m/n on input line 77. +LaTeX Font Info: ... okay on input line 77. +LaTeX Font Info: Checking defaults for JT1/mc/m/n on input line 77. +LaTeX Font Info: ... okay on input line 77. +\c@lstlisting=\count117 +File: fig/ryukyu.pdf Graphic file (type pdf) + <fig/ryukyu.pdf> [0 + +] +LaTeX Font Info: Font shape `JT1/mc/bx/n' in size <24.88> not available +(Font) Font shape `JT1/gt/m/n' tried instead on input line 86. +LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <24.88> not available +(Font) Font shape `JY1/gt/m/n' tried instead on input line 86. + (./main.toc +LaTeX Font Info: Font shape `JT1/mc/bx/n' in size <12> not available +(Font) Font shape `JT1/gt/m/n' tried instead on input line 1. +LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <12> not available +(Font) Font shape `JY1/gt/m/n' tried instead on input line 1. +LaTeX Font Info: Try loading font information for U+msa on input line 2. + +(/usr/local/texlive/2017/texmf-dist/tex/latex/amsfonts/umsa.fd +File: umsa.fd 2013/01/14 v3.01 AMS symbols A +) +LaTeX Font Info: Try loading font information for U+msb on input line 2. + +(/usr/local/texlive/2017/texmf-dist/tex/latex/amsfonts/umsb.fd +File: umsb.fd 2013/01/14 v3.01 AMS symbols B +)) +\tf@toc=\write3 +\openout3 = `main.toc'. + + [1 + +] +(./main.lof) +\tf@lof=\write4 +\openout4 = `main.lof'. + + [2 + +] (./main.lol) +\tf@lol=\write5 +\openout5 = `main.lol'. + + (./chapter1.tex [3 + +] +第 1 章 +LaTeX Font Info: Font shape `JT1/mc/bx/n' in size <17.28> not available +(Font) Font shape `JT1/gt/m/n' tried instead on input line 6. +LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <17.28> not available +(Font) Font shape `JY1/gt/m/n' tried instead on input line 6. +[1 + +]) (./chapter2.tex [2] +第 2 章 +File: pic/ring.pdf Graphic file (type pdf) +<pic/ring.pdf> [3 + +] +File: pic/mesh.pdf Graphic file (type pdf) + <pic/mesh.pdf> +File: pic/tree.pdf Graphic file (type pdf) + <pic/tree.pdf> [4]) (./chapter3.tex [5] +第 3 章 +LaTeX Font Info: Try loading font information for OMS+cmr on input line 18. +(/usr/local/texlive/2017/texmf-dist/tex/latex/base/omscmr.fd +File: omscmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions +) +LaTeX Font Info: Font shape `OMS/cmr/m/n' in size <12> not available +(Font) Font shape `OMS/cmsy/m/n' tried instead on input line 18. +File: pic/logupdatetest.pdf Graphic file (type pdf) + +<pic/logupdatetest.pdf> [6 + +] [7] +File: pic/topologymanager.pdf Graphic file (type pdf) + <pic/topologymanager.pdf> [8] +File: ./pic/torque.pdf Graphic file (type pdf) + +<./pic/torque.pdf> [9] +File: pic/logupdatetest.pdf Graphic file (type pdf) + <pic/logupdatetest.pdf> +File: pic/LogupdateTree.pdf Graphic file (type pdf) + <pic/LogupdateTree.pdf> [10]) +(./chapter4.tex [11] +第 4 章 +[12 + +]) (./chapter5.tex +第 5 章 +) (./bibliography.tex [13 + +]) (./thanks.tex [14 + +]) [15 + +] (./main.aux) + +LaTeX Warning: There were multiply-defined labels. + + ) +Here is how much of TeX's memory you used: + 3774 strings out of 493653 + 47210 string characters out of 6148873 + 113868 words of memory out of 5000000 + 7278 multiletter control sequences out of 15000+600000 + 16075 words of font info for 64 fonts, out of 8000000 for 9000 + 929 hyphenation exceptions out of 8191 + 27i,5n,32p,520b,324s stack positions out of 5000i,500n,10000p,200000b,80000s + +Output written on main.dvi (19 pages, 32296 bytes).
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/main.tex Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,127 @@ +\documentclass[a4j,12pt]{jreport} +\usepackage[dvipdfmx]{graphicx} +\usepackage{mythesis} +\usepackage{bussproofs} +\usepackage{multirow} +\usepackage{here} +\usepackage{listings} +\usepackage{url} +\usepackage{cite} +\usepackage{listings} +\usepackage{amssymb} +\usepackage{amsmath} +\usepackage[utf8]{inputenc} + +\lstset{ + basicstyle={\ttfamily}, + breaklines=true, + columns=[l]{fullflexible}, + commentstyle={\ttfamily}, + escapechar={@}, + frame=single, + framerule=.5pt, + identifierstyle={\ttfamily}, + keepspaces=true, + keywordstyle={\ttfamily}, + language={}, + lineskip=-0.1zw, + numbers=left, + numbersep=1em, + numberstyle={\scriptsize}, + stepnumber=1, + stringstyle={\ttfamily}, + tabsize=4, + xleftmargin=0zw, + xrightmargin=0zw, +} + +% \lstset{ +% language={C}, +% basicstyle={\footnotesize\ttfamily}, +% identifierstyle={\footnotesize}, +% commentstyle={\footnotesize\itshape}, +% keywordstyle={\footnotesize\bfseries}, +% ndkeywordstyle={\footnotesize}, +% stringstyle={\footnotesize\ttfamily}, +% frame={tb}, +% breaklines=true, +% columns=[l]{fullflexible}, +% numbers=left, +% xrightmargin=0zw, +% xleftmargin=3zw, +% numberstyle={\scriptsize}, +% stepnumber=1, +% numbersep=1zw, +% lineskip=-0.5ex +% } +\def\lstlistingname{リスト} +\def\lstlistlistingname{リスト目次} +\setlength{\itemsep}{-1zh} +\title{分散版jungleデータベースの性能測定方法} +\icon{ + \includegraphics[width=80mm,bb=0 0 595 642]{fig/ryukyu.pdf} %%元は 642じゃなくて842 +} +\year{平成30年度 卒業論文} +\belongto{琉球大学工学部情報工学科} +\author{145762E 仲松 栞 \\ 指導教員 {河野 真治} } +%% +%% プリアンブルに記述 +%% Figure 環境中で Table 環境の見出しを表示・カウンタの操作に必要 +%% +\makeatletter +\newcommand{\figcaption}[1]{\def\@captype{figure}\caption{#1}} +\newcommand{\tblcaption}[1]{\def\@captype{table}\caption{#1}} +\makeatother +\setlength\abovecaptionskip{0pt} + +\begin{document} + +% タイトル +\maketitle +\baselineskip 17pt plus 1pt minus 1pt + +\pagenumbering{roman} +\setcounter{page}{0} + +\tableofcontents % 目次 +\listoffigures % 図目次 +%\listoftables % 表目次 +\lstlistoflistings + +%以下のように、章ごとに個別の tex ファイルを作成して、 +% main.tex をコンパイルして確認する。 +%章分けは個人で違うので下のフォーマットを参考にして下さい。 + +% はじめに +\input{chapter1.tex} + +% 分散版jungleの概要 +\input{chapter2.tex} + +% 実験概要 +\input{chapter3.tex} + +% 性能評価 +\input{chapter4.tex} + +% まとめ +\input{chapter5.tex} + +% -- +%\input{chapter6.tex} + +% 参考文献 + +% \bibliographystyle{junsrt} +% \bibliography{reference} + +\input{bibliography.tex} + +% 謝辞 +\input{thanks.tex} + +\appendix +% 付録 +%\input{appendix.tex} + +\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/main.toc Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,20 @@ +\contentsline {chapter}{\numberline {第1章}はじめに}{1} +\contentsline {section}{\numberline {1.1}研究背景}{1} +\contentsline {section}{\numberline {1.2}研究目的}{2} +\contentsline {chapter}{\numberline {第2章}分散版jungleデータベース}{3} +\contentsline {section}{\numberline {2.1}Jungleデータベースの構造}{3} +\contentsline {section}{\numberline {2.2}分散機構}{3} +\contentsline {chapter}{\numberline {第3章}評価実験}{6} +\contentsline {section}{\numberline {3.1}実験目的}{6} +\contentsline {section}{\numberline {3.2}分散フレームワーク Alice による分散環境の構築}{8} +\contentsline {section}{\numberline {3.3}TORQUE Resource Manager}{9} +\contentsline {section}{\numberline {3.4}Jungleの分散性能測定用テストプログラム}{10} +\contentsline {section}{\numberline {3.5}LogupdateTree.sh}{10} +\contentsline {section}{\numberline {3.6}killLogupdate.sh}{11} +\contentsline {chapter}{\numberline {第4章}性能評価}{12} +\contentsline {section}{\numberline {4.1}java版jungleとhuskell版jungleの比較}{12} +\contentsline {section}{\numberline {4.2}java版jungleの分散性能の評価}{12} +\contentsline {section}{\numberline {4.3}性能測定方法の評価}{12} +\contentsline {chapter}{\numberline {第5章}結論}{13} +\contentsline {section}{\numberline {5.1}まとめ}{13} +\contentsline {section}{\numberline {5.2}今後の課題}{13}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/mythesis.sty Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,156 @@ +% +% 卒業論文スタイルファイル(mythesis.sty) +% version 1.0e +% +% ver 1.0e 02/07/2000 since +% usage: + +%\documentclass[a4j]{jreport} +%\usepackage{master_paper} +% +% +%\title{卒論タイトル \\ 長い} +%\etitle{\pLaTeX2e style test file for Teri's thesis } +%\year{平成11年度} +%\belongto{琉球大学大学工学部\\ 情報工学科} +%\author{豊平 絵梨} +% +%\begin{document} +% +%\maketitle +% +%%要旨 +%\input{abstract.tex} +% +%%目次 +%\tableofcontents +% +%%図目次 +%\listoffigures +% +%%表目次 +%\listoftables +% +%%第一章 +%\input{chapter1.tex} +%%chapter1.texの\chapter{}の後ろに次のコマンドを追加してください。 +%%ページカウントがリセットされ、ページ数がアラビア文字になります。 +%% \pagenumbering{arabic} +%%第二章 +%\input{chapter2.tex} +%%第三章 +%\input{chapter3.tex} +% +%%付録 +%\input{appendix.tex} +% +%%謝辞 +%%\input{thanx.tex} +% +%%参考文献 +%\input{biblography.tex} +% +%\end{document} + + +%長さ設定 +%\setlength{\topmargin}{-30mm} +%\addtolength{\oddsidemargin}{-15mm} +%\addtolength{\textwidth}{60mm} + +\topmargin -1in \addtolength{\topmargin}{35mm} +\headheight 0mm +\headsep 0mm +\oddsidemargin -1in \addtolength{\oddsidemargin}{30mm} +%\evensidemargin -1in \addtolength{\evensidemargin}{8mm} +\textwidth 160mm +\textheight 230mm +%\footheight 0mm +%\footskip 0mm +%\pagestyle{empty} + + +%年度 +\def\@year{} +\def\year#1{\gdef\@year{#1}} +%英文タイトル +\def\@etitle{} +\def\etitle#1{\gdef\@etitle{#1}} +%アイコン +\def\@icon{} +\def\icon#1{\gdef\@icon{#1}} +%所属 +\def\@belongto{} +\def\belongto#1{\gdef\@belongto{#1}} + +%表紙 +\renewcommand{\maketitle}{% +\newpage\null +\thispagestyle{empty} +\vskip 0cm% +\begin{center}% +\let\footnote\thanks + {\huge \@year \par}% + \vskip 3em% + {\Huge \@title \par}% + \vskip 1em% + {\huge \@etitle \par}% + \vskip 8em% + {\huge \@icon \par}% + \vskip 0.5em% + {\huge \@belongto \par}% + \vskip 1.0em% + {\huge \@author \par}% + +\end{center}% +\par\vskip 1.5em +} + + +%abstract +\renewenvironment{abstract}{% + \titlepage + \thispagestyle{empty} + \null\vfil + \@beginparpenalty\@lowpenalty + {\Huge \bfseries \abstractname}% + \begin{center}% + \@endparpenalty\@M + \end{center} +}% + + +%目次 +\renewcommand{\tableofcontents}{% + \pagestyle{plain} + \if@twocolumn\@restonecoltrue\onecolumn + \else\@restonecolfalse\fi + \chapter*{\contentsname + \@mkboth{\contentsname}{\contentsname}% + } \pagenumbering{roman}\@starttoc{toc}% + \if@restonecol\twocolumn\fi +} + +%章 +\renewcommand{\chapter}{% + \pagestyle{plain} + \if@openright\cleardoublepage\else\clearpage\fi + \thispagestyle{jpl@in}% + \global\@topnum\z@ + \@afterindentfalse + \secdef\@chapter\@schapter} + + +\renewcommand{\prepartname}{} %\renewcommand{\prepartname}{第} +\renewcommand{\postpartname}{部} +\renewcommand{\prechaptername}{第}%\renewcommand{\prechaptername}{第} +\renewcommand{\postchaptername}{章} +\renewcommand{\contentsname}{目 次} +\renewcommand{\listfigurename}{図 目 次} +\renewcommand{\listtablename}{表 目 次} +\renewcommand{\bibname}{参考文献} +\renewcommand{\indexname}{索 引} +\renewcommand{\figurename}{図} +\renewcommand{\tablename}{表} +\renewcommand{\appendixname}{付 録} +\renewcommand{\abstractname}{要 旨}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaBasics.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,1 @@ +module AgdaBasics where
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaBool.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,3 @@ +data Bool : Set where + true : Bool + false : Bool
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaElem.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,3 @@ +elem : {A : Set} {{eqA : Eq A}} → A → List A → Bool +elem {{eqA}} x (y ∷ xs) = (Eq._==_ eqA x y) || (elem {{eqA}} x xs) +elem x [] = false
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaElemApply.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,3 @@ +listHas4 : Bool +listHas4 = elem 4 (3 ∷ 2 ∷ 5 ∷ 4 ∷ []) -- true +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaFunction.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,2 @@ +f : Bool -> Bool +f x = true
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaId.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,5 @@ +identity : (A : Set) -> A -> A +identity A x = x + +identity-zero : Nat +identity-zero = identity Nat zero
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaImplicitId.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,11 @@ +id : {A : Set} -> A -> A +id x = x + +id-zero : Nat +id-zero = id zero + +id' : {A : Set} -> A -> A +id' {A} x = x + +id-true : Bool +id-true = id {Bool} true
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaImport.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,6 @@ +import Data.Nat -- import module +import Data.Bool as B -- renamed module +import Data.List using (head) -- import Data.head function +import Level renaming (suc to S) -- import module with rename suc to S +import Data.String hiding (_++_) -- import module without _++_ +open import Data.List -- import and expand Data.List
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaInstance.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,9 @@ +_==Nat_ : Nat -> Nat -> Bool +zero ==Nat zero = true +(suc n) ==Nat zero = false +zero ==Nat (suc m) = false +(suc n) ==Nat (suc m) = n ==Nat m + +instance + natHas== : Eq Nat + natHas== = record { _==_ = _==Nat_}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaLambda.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,5 @@ +not-apply : Bool -> Bool +not-apply = (\b -> not b) -- use lambda + +not-apply : Bool -> Bool +not-appy b = not b -- not use lambda
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaModusPonens.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,2 @@ +f : {A B C : Set} -> ((A -> B) × (B -> C)) -> (A -> C) +f = \p x -> (snd p) ((fst p) x)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaNPushNPop.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,13 @@ +n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta +n-push {{mm}} (zero) = M.cs {{mm}} {{mm}} id +n-push {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-push {m} {{mm}} n) (pushOnce m)) + +n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta +n-pop {{mm}} (zero) = M.cs {{mm}} {{mm}} id +n-pop {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-pop {m} {{mm}} n) (popOnce m)) + +pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ +pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta + ≡ M.exec (n-push {meta} n) meta + where + meta = id-meta cn ce s
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaNPushNPopProof.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,58 @@ +pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ +pop-n-push-type n cn ce s = M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) meta + ≡ M.exec (n-push n) meta + where + meta = id-meta cn ce s + +pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s +pop-n-push zero cn ce s = refl +pop-n-push (suc n) cn ce s = begin + M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta cn ce s) + ≡⟨ refl ⟩ + M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta cn ce s) + ≡⟨ exec-comp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩ + M.exec (M.cs popOnce) (M.exec (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s)) + ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩ + M.exec (M.cs popOnce) (M.exec (n-push (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s))) + ≡⟨ refl ⟩ + M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) + ≡⟨ sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩ + M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) + ≡⟨ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩ + M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) + ≡⟨ refl ⟩ + M.exec (n-push n) (pushOnce (id-meta cn ce s)) + ≡⟨ refl ⟩ + M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s)) + ≡⟨ refl ⟩ + M.exec (n-push (suc n)) (id-meta cn ce s) + ∎ + + + +n-push-pop-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ +n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop n) (n-push n)) meta ≡ meta + where + meta = id-meta cn ce st + +n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s +n-push-pop zero cn ce s = refl +n-push-pop (suc n) cn ce s = begin + M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta cn ce s) + ≡⟨ refl ⟩ + M.exec (M.csComp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push (suc n))) (id-meta cn ce s) + ≡⟨ exec-comp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push (suc n)) (id-meta cn ce s) ⟩ + M.exec (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (M.exec (n-push (suc n)) (id-meta cn ce s)) + ≡⟨ refl ⟩ + M.exec (n-pop n) (popOnce (M.exec (n-push (suc n)) (id-meta cn ce s))) + ≡⟨ refl ⟩ + M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce s))) + ≡⟨ cong (\x -> M.exec (n-pop n) x) (sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce s))) ⟩ + M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s)) + ≡⟨ cong (\x -> M.exec (n-pop n) x) (pop-n-push n cn ce s) ⟩ + M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s)) + ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩ + M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s) + ≡⟨ n-push-pop n cn ce s ⟩ + id-meta cn ce s + ∎
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaNat.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,3 @@ +data Nat : Set where + zero : Nat + suc : Nat -> Nat
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaNot.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,3 @@ +not : Bool -> Bool +not true = false +not false = true
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaParameterizedModule.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,7 @@ +module Sort (A : Set) (_<_ : A -> A -> Bool) where +sort : List A -> List A +sort = -- 実装は省略 ... + +-- Parameterized Module により N.sort や B.sort が可能 +open import Sort Nat Nat._<_ as N +open import Sort Bool Bool._<_ as B
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaPattern.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,3 @@ +not : Bool -> Bool +not false = true +not x = false
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaPlus.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,3 @@ +_+_ : Nat -> Nat -> Nat +zero + m = m +suc n + m = suc (n + m)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaProduct.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,8 @@ +data _×_ (A B : Set) : Set where + <_,_> : A -> B -> A × B + +fst : {A B : Set} -> A × B -> A +fst < a , _ > = a + +snd : {A B : Set} -> A × B -> B +snd < _ , b > = b
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaProp.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,2 @@ +prop : Bool +prop = true
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaPushPop.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,28 @@ +pushSingleLinkedStack : Meta -> Meta +pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) }) + where + n = Meta.nextCS m + s = Meta.stack m + e = Context.element (Meta.context m) + push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A + push s nothing = s + push s (just x) = record {top = just (cons x (top s))} + +popSingleLinkedStack : Meta -> Meta +popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}}) + where + n = Meta.nextCS m + con = Meta.context m + elem : Meta -> Maybe A + elem record {stack = record { top = (just (cons x _)) }} = just x + elem record {stack = record { top = nothing }} = nothing + st : Meta -> SingleLinkedStack A + st record {stack = record { top = (just (cons _ s)) }} = record {top = s} + st record {stack = record { top = nothing }} = record {top = nothing} + + +pushSingleLinkedStackCS : M.CodeSegment Meta Meta +pushSingleLinkedStackCS = M.cs pushSingleLinkedStack + +popSingleLinkedStackCS : M.CodeSegment Meta Meta +popSingleLinkedStackCS = M.cs popSingleLinkedStack
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaPushPopProof.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,11 @@ +id-meta : ℕ -> ℕ -> SingleLinkedStack ℕ -> Meta +id-meta n e s = record { context = record {n = n ; element = just e} + ; nextCS = (N.cs id) ; stack = s} + +push-pop-type : ℕ -> ℕ -> ℕ -> Element ℕ -> Set₁ +push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta + where + meta = id-meta n e record {top = just (cons x (just s))} + +push-pop : (n e x : ℕ) -> (s : Element ℕ) -> push-pop-type n e x s +push-pop n e x s = refl
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaRecord.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,7 @@ +record Point : Set where + field + x : Nat + y : Nat + +makePoint : Nat -> Nat -> Point +makePoint a b = record { x = a ; y = b }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaRecordProj.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,8 @@ +getX : Point -> Nat +getX p = Point.x p + +getY : Point -> Nat +getY record { x = a ; y = b} = b + +xPlus5 : Point -> Point +xPlus5 p = record p { x = (Point.x p) + 5}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaStack.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,13 @@ +data Element (a : Set) : Set where + cons : a -> Maybe (Element a) -> Element a + +datum : {a : Set} -> Element a -> a +datum (cons a _) = a + +next : {a : Set} -> Element a -> Maybe (Element a) +next (cons _ n) = n + +record SingleLinkedStack (a : Set) : Set where + field + top : Maybe (Element a) +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaStackDS.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,17 @@ +record Context : Set where + field + -- fields for stack + element : Maybe A + + +open import subtype Context as N + +record Meta : Set₁ where + field + -- context as set of data segments + context : Context + stack : SingleLinkedStack A + nextCS : N.CodeSegment Context Context + +open import subtype Meta as M +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaTypeClass.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,3 @@ +record Eq (A : Set) : Set where + field + _==_ : A -> A -> Bool
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/AgdaWhere.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,7 @@ +f : Int -> Int -> Int +f a b c = (t a) + (t b) + (t c) + where + t x = x + x + x + +f' : Int -> Int -> Int +f' a b c = (a + a + a) + (b + b + b) + (c + c + c)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/CodeSegment.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,2 @@ +data CodeSegment {l1 l2 : Level} (I : Set l1) (O : Set l2) : Set (l ⊔ l1 ⊔ l2) where + cs : (I -> O) -> CodeSegment I O
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/CodeSegments.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,12 @@ +cs2 : CodeSegment ds1 ds1 +cs2 = cs id + +cs1 : CodeSegment ds1 ds1 +cs1 = cs (\d -> goto cs2 d) + +cs0 : CodeSegment ds0 ds1 +cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) + +main : ds1 +main = goto cs0 (record {a = 100 ; b = 50}) +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/DataSegment.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,8 @@ +record ds0 : Set where + field + a : Int + b : Int + +record ds1 : Set where + field + c : Int
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/Eq.Agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,30 @@ +module Eq where +open import Data.Nat +open import Data.Bool +open import Data.List + +record Eq (A : Set) : Set where + field + _==_ : A -> A -> Bool + +_==Nat_ : ℕ -> ℕ -> Bool +zero ==Nat zero = true +(suc n) ==Nat zero = false +zero ==Nat (suc m) = false +(suc n) ==Nat (suc m) = n ==Nat m + + +instance + _ : Eq ℕ + _ = record { _==_ = _==Nat_} + +_||_ : Bool -> Bool -> Bool +true || _ = true +false || x = x + +elem : {A : Set} {{eqA : Eq A}} → A → List A → Bool +elem {{eqA}} x (y ∷ xs) = (Eq._==_ eqA x y) || (elem {{eqA}} x xs) +elem x [] = false + +listHas4 : Bool +listHas4 = elem 4 (3 ∷ 2 ∷ 5 ∷ 4 ∷ []) -- true
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/Equiv.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,1 @@ +data _≡_ {a} {A : Set a} (x : A) : A → Set a where refl : x ≡ x \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/Exec.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,5 @@ +exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} + {{_ : DataSegment I}} {{_ : DataSegment O}} + -> CodeSegment I O -> Context -> Context +exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c)) +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/Goto.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,4 @@ +goto : {l1 l2 : Level} {I : Set l1} {O : Set l2} + -> CodeSegment I O -> I -> O +goto (cs b) i = b i +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/Maybe.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,3 @@ +data Maybe {a} (A : Set a) : Set a where + just : (x : A) -> Maybe A + nothing : Maybe A
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/MetaCodeSegment.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,4 @@ +data CodeSegment {l1 l2 : Level} (A : Set l1) (B : Set l2) : Set (l ⊔ l1 ⊔ l2) where + cs : {{_ : DataSegment A}} {{_ : DataSegment B}} + -> (A -> B) -> CodeSegment A B +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/MetaDataSegment.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,7 @@ +module subtype {l : Level} (Context : Set l) where + +record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where + field + get : Context -> A + set : Context -> A -> Context +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/MetaMetaCodeSegment.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,29 @@ +-- meta level +liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context +liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c))) + +liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y +liftMeta (N.cs f) = M.cs f + +gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} -> M.CodeSegment Meta Meta -> N.CodeSegment I O -> Meta -> Meta +gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)}) + +push : M.CodeSegment Meta Meta +push = M.cs (\m -> M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)})) + +-- normal level + +cs2 : N.CodeSegment ds1 ds1 +cs2 = N.cs id + +cs1 : N.CodeSegment ds1 ds1 +cs1 = N.cs (\d -> N.goto cs2 d) + +cs0 : N.CodeSegment ds0 ds1 +cs0 = N.cs (\d -> N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) + +-- meta level (with extended normal) +main : Meta +main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)}) +-- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/MetaMetaDataSegment.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,12 @@ +-- 上で各 DataSegement の定義を行なっているとする +open import subtype Context as N -- Meta Datasegment を定義 + +-- Meta DataSegment を持つ Meta Meta DataSegment を定義できる +record Meta : Set where + field + context : Context + c' : Int + next : N.CodeSegment Context Context + +open import subtype Meta as M +-- 以下よりメタメタレベルのプログラムを記述できる
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/Nat.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,5 @@ +module nat where + +data Nat : Set where + O : Nat + S : Nat -> Nat \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/NatAdd.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,6 @@ +open import nat +module nat_add where + +_+_ : Nat -> Nat -> Nat +O + m = m +(S n) + m = S (n + m) \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/NatAddSym.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,12 @@ +open import Relation.Binary.PropositionalEquality +open import nat +open import nat_add +open ≡-Reasoning + +module nat_add_sym where + +addSym : (n m : Nat) -> n + m ≡ m + n +addSym O O = refl +addSym O (S m) = cong S (addSym O m) +addSym (S n) O = cong S (addSym n O) +addSym (S n) (S m) = {!!} -- 後述
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/PushPopType.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,9 @@ +pushOnce : Meta -> Meta +pushOnce m = M.exec pushSingleLinkedStackCS m + +popOnce : Meta -> Meta +popOnce m = M.exec popSingleLinkedStackCS m + +push-pop-type : Meta -> Set₁ +push-pop-type meta = + M.exec (M.csComp (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/Reasoning.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,21 @@ +open import Relation.Binary.PropositionalEquality +open import nat +open import nat_add +open ≡-Reasoning + +module nat_add_sym_reasoning where + +addToRight : (n m : Nat) -> S (n + m) ≡ n + (S m) +addToRight O m = refl +addToRight (S n) m = cong S (addToRight n m) + +addSym : (n m : Nat) -> n + m ≡ m + n +addSym O O = refl +addSym O (S m) = cong S (addSym O m) +addSym (S n) O = cong S (addSym n O) +addSym (S n) (S m) = begin + (S n) + (S m) ≡⟨ refl ⟩ + S (n + S m) ≡⟨ cong S (addSym n (S m)) ⟩ + S ((S m) + n) ≡⟨ addToRight (S m) n ⟩ + S (m + S n) ≡⟨ refl ⟩ + (S m) + (S n) ∎
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/SingleLinkedStack.cbc Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,110 @@ +#include "../context.h" +#include "../origin_cs.h" +#include <stdio.h> + +// typedef struct SingleLinkedStack { +// struct Element* top; +// } SingleLinkedStack; + +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; + stack->pop2 = C_pop2SingleLinkedStack; + stack->get = C_getSingleLinkedStack; + stack->get2 = C_get2SingleLinkedStack; + stack->isEmpty = C_isEmptySingleLinkedStack; + stack->clear = C_clearSingleLinkedStack; + return stack; +} + +void printStack1(union Data* data) { + struct Node* node = &data->Element.data->Node; + if (node == NULL) { + printf("NULL"); + } else { + printf("key = %d ,", node->key); + printStack1((union Data*)data->Element.next); + } +} + +void printStack(union Data* data) { + printStack1(data); + printf("\n"); +} + +__code clearSingleLinkedStack(struct SingleLinkedStack* stack,__code next(...)) { + stack->top = NULL; + goto next(...); +} + +__code pushSingleLinkedStack(struct SingleLinkedStack* stack,union Data* data, __code next(...)) { + Element* element = new Element(); + element->next = stack->top; + element->data = data; + stack->top = element; + goto next(...); +} + +__code popSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) { + if (stack->top) { + data = stack->top->data; + stack->top = stack->top->next; + } else { + data = NULL; + } + goto next(data, ...); +} + +__code pop2SingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) { + if (stack->top) { + data = stack->top->data; + stack->top = stack->top->next; + } else { + data = NULL; + } + if (stack->top) { + data1 = stack->top->data; + stack->top = stack->top->next; + } else { + data1 = NULL; + } + goto next(data, data1, ...); +} + + +__code getSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) { + if (stack->top) + data = stack->top->data; + else + data = NULL; + goto next(data, ...); +} + +__code get2SingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) { + if (stack->top) { + data = stack->top->data; + if (stack->top->next) { + data1 = stack->top->next->data; + } else { + data1 = NULL; + } + } else { + data = NULL; + data1 = NULL; + } + goto next(data, data1, ...); +} + +__code isEmptySingleLinkedStack(struct SingleLinkedStack* stack, __code next(...), __code whenEmpty(...)) { + if (stack->top) + goto next(...); + else + goto whenEmpty(...); +} + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/ThreePlusOne.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,8 @@ +open import Relation.Binary.PropositionalEquality +open import nat +open import nat_add + +module three_plus_one where + +3+1 : (S (S (S O))) + (S O) ≡ (S (S (S (S O)))) +3+1 = refl \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/akashaContext.h Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,31 @@ +// Data Segment +union Data { + struct Tree { /* ... 赤黒木の定義と同様 */ } tree; + struct Node { /* ... 赤黒木の定義と同様 */ } node; + + /* for verification */ + struct IterElem { + unsigned int val; + struct IterElem* next; + } iterElem; + struct Iterator { + struct Tree* tree; + struct Iterator* previousDepth; + struct IterElem* head; + struct IterElem* last; + unsigned int iteratedValue; + unsigned long iteratedPointDataNum; + void* iteratedPointHeap; + } iterator; + struct AkashaInfo { + unsigned int minHeight; + unsigned int maxHeight; + struct AkashaNode* akashaNode; + } akashaInfo; + struct AkashaNode { + unsigned int height; + struct Node* node; + struct AkashaNode* nextAkashaNode; + } akashaNode; +}; +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/akashaMeta.c Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,31 @@ +__code meta(struct Context* context, enum Code next) { + struct Iterator* iter = &context->data[Iter]->iterator; + + switch (context->prev) { + case GoToPreviousDepth: + if (iter->iteratedPointDataNum == 0) break; + if (iter->iteratedPointHeap == NULL) break; + + unsigned int diff =(unsigned long)context->heap - (unsigned long)iter->iteratedPointHeap; + memset(iter->iteratedPointHeap, 0, diff); + context->dataNum = iter->iteratedPointDataNum; + context->heap = iter->iteratedPointHeap; + break; + default: + break; + } + switch (next) { + case PutAndGoToNextDepth: // with assert check + if (context->prev == GoToPreviousDepth) break; + if (iter->previousDepth == NULL) break; + iter->previousDepth->iteratedPointDataNum = context->dataNum; + iter->previousDepth->iteratedPointHeap = context->heap; + break; + default: + break; + } + + context->prev = next; + goto (context->code[next])(context); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/assert.c Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,7 @@ +__code verifySpecificationFinish(struct Context* context) { + if (context->data[AkashaInfo]->akashaInfo.maxHeight > 2*context->data[AkashaInfo]->akashaInfo.minHeight) { + context->next = Exit; + goto meta(context, ShowTrace); + } + goto meta(context, DuplicateIterator); +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/atton-master-meta-sample.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,77 @@ +module atton-master-meta-sample where + +open import Data.Nat +open import Data.Unit +open import Function +Int = ℕ + +record Context : Set where + field + a : Int + b : Int + c : Int + +open import subtype Context as N + +record Meta : Set where + field + context : Context + c' : Int + next : N.CodeSegment Context Context + +open import subtype Meta as M + +instance + _ : N.DataSegment Context + _ = record { get = id ; set = (\_ c -> c) } + _ : M.DataSegment Context + _ = record { get = (\m -> Meta.context m) ; + set = (\m c -> record m {context = c}) } + _ : M.DataSegment Meta + _ = record { get = id ; set = (\_ m -> m) } + + +liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context +liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c))) + +liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y +liftMeta (N.cs f) = M.cs f + + +gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} -> M.CodeSegment Meta Meta -> N.CodeSegment I O -> Meta -> Meta +gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)}) + +push : M.CodeSegment Meta Meta +push = M.cs (\m -> M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)})) + + +record ds0 : Set where + field + a : Int + b : Int + +record ds1 : Set where + field + c : Int + +instance + _ : N.DataSegment ds0 + _ = record { set = (\c d -> record c {a = (ds0.a d) ; b = (ds0.b d)}) + ; get = (\c -> record { a = (Context.a c) ; b = (Context.b c)})} + _ : N.DataSegment ds1 + _ = record { set = (\c d -> record c {c = (ds1.c d)}) + ; get = (\c -> record { c = (Context.c c)})} + +cs2 : N.CodeSegment ds1 ds1 +cs2 = N.cs id + +cs1 : N.CodeSegment ds1 ds1 +cs1 = N.cs (\d -> N.goto cs2 d) + +cs0 : N.CodeSegment ds0 ds1 +cs0 = N.cs (\d -> N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) + + +main : Meta +main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)}) +-- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/atton-master-sample.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,46 @@ +module atton-master-sample where + +open import Data.Nat +open import Data.Unit +open import Function +Int = ℕ + +record Context : Set where + field + a : Int + b : Int + c : Int + + +open import subtype Context + + + +record ds0 : Set where + field + a : Int + b : Int + +record ds1 : Set where + field + c : Int + +instance + _ : DataSegment ds0 + _ = record { set = (\c d -> record c {a = (ds0.a d) ; b = (ds0.b d)}) + ; get = (\c -> record { a = (Context.a c) ; b = (Context.b c)})} + _ : DataSegment ds1 + _ = record { set = (\c d -> record c {c = (ds1.c d)}) + ; get = (\c -> record { c = (Context.c c)})} + +cs2 : CodeSegment ds1 ds1 +cs2 = cs id + +cs1 : CodeSegment ds1 ds1 +cs1 = cs (\d -> goto cs2 d) + +cs0 : CodeSegment ds0 ds1 +cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) + +main : ds1 +main = goto cs0 (record {a = 100 ; b = 50})
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/cbmc-assert.c Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,7 @@ +void verifySpecification(struct Context* context, + struct Tree* tree) { + assert(!(maxHeight(tree->root, 1) > + 2*minHeight(tree->root, 1))); + return meta(context, EnumerateInputs); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/context.h Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,47 @@ +/* Context definition */ + +#define ALLOCATE_SIZE 1024 + +enum Code { + Code1, + Code2, + Allocator, +}; + +enum UniqueData { + Allocate, + Tree, +}; + +struct Context { + int codeNum; + __code (**code) (struct Context *); + void* heap_start; + void* heap; + long dataSize; + int dataNum; + union Data **data; +}; + +union Data { + struct Tree { + union Data* root; + union Data* current; + union Data* prev; + int result; + } tree; + struct Node { + int key; + int value; + enum Color { + Red, + Black, + } color; + union Data* left; + union Data* right; + } node; + struct Allocate { + long size; + enum Code next; + } allocate; +};
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/enumerate-inputs.c Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,13 @@ +void enumerateInputs(struct Context* context, + struct Node* node) { + if (context->loopCount > LIMIT_OF_VERIFICATION_SIZE) { + return meta(context, Exit); + } + + node->key = nondet_int(); + node->value = node->key; + context->next = VerifySpecification; + context->loopCount++; + + return meta(context, Put); +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/expr-term.txt Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,8 @@ +t ::= + true + false + if t then t else t + 0 + succ t + pred t + iszero t
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/factrial.cbc Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,29 @@ +__code print_factorial(int prod) +{ + printf("factorial = %d\n", prod); + exit(0); +} + +__code factorial0(int prod, int x) +{ + if (x >= 1) { + goto factorial0(prod*x, x-1); + } else { + goto print_factorial(prod); + } + +} + +__code factorial(int x) +{ + goto factorial0(1, x); +} + +int main(int argc, char **argv) +{ + int i; + i = atoi(argv[1]); + + goto factorial(i); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/getMinHeight.c Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,51 @@ +__code getMinHeight_stub(struct Context* context) { + goto getMinHeight(context, &context->data[Allocate]->allocate, &context->data[AkashaInfo]->akashaInfo); +} + +__code getMinHeight(struct Context* context, struct Allocate* allocate, struct AkashaInfo* akashaInfo) { + const struct AkashaNode* akashaNode = akashaInfo->akashaNode; + + if (akashaNode == NULL) { + allocate->size = sizeof(struct AkashaNode); + allocator(context); + akashaInfo->akashaNode = (struct AkashaNode*)context->data[context->dataNum]; + + akashaInfo->akashaNode->height = 1; + akashaInfo->akashaNode->node = context->data[Tree]->tree.root; + + goto getMaxHeight_stub(context); + } + + const struct Node* node = akashaInfo->akashaNode->node; + if (node->left == NULL && node->right == NULL) { + if (akashaInfo->minHeight > akashaNode->height) { + akashaInfo->minHeight = akashaNode->height; + akashaInfo->akashaNode = akashaNode->nextAkashaNode; + goto getMinHeight_stub(context); + } + } + + akashaInfo->akashaNode = akashaInfo->akashaNode->nextAkashaNode; + + if (node->left != NULL) { + allocate->size = sizeof(struct AkashaNode); + allocator(context); + struct AkashaNode* left = (struct AkashaNode*)context->data[context->dataNum]; + left->height = akashaNode->height+1; + left->node = node->left; + left->nextAkashaNode = akashaInfo->akashaNode; + akashaInfo->akashaNode = left; + } + + if (node->right != NULL) { + allocate->size = sizeof(struct AkashaNode); + allocator(context); + struct AkashaNode* right = (struct AkashaNode*)context->data[context->dataNum]; + right->height = akashaNode->height+1; + right->node = node->right; + right->nextAkashaNode = akashaInfo->akashaNode; + akashaInfo->akashaNode = right; + } + + goto getMinHeight_stub(context); +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/goto.cbc Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,7 @@ +__code cs0(int a, int b){ + goto cs1(a+b); +} + +__code cs1(int c){ + goto cs2(c); +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/initLLRBContext.c Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,53 @@ +__code initLLRBContext(struct Context* context, int num) { + context->heapLimit = sizeof(union Data)*ALLOCATE_SIZE; + context->code = malloc(sizeof(__code*)*ALLOCATE_SIZE); + context->data = malloc(sizeof(union Data*)*ALLOCATE_SIZE); + context->heapStart = malloc(context->heapLimit); + + context->codeNum = Exit; + + context->code[Code1] = code1_stub; + context->code[Code2] = code2_stub; + context->code[Code3] = code3_stub; + context->code[Code4] = code4; + context->code[Code5] = code5; + context->code[Find] = find; + context->code[Not_find] = not_find; + context->code[Code6] = code6; + context->code[Put] = put_stub; + context->code[Replace] = replaceNode_stub; + context->code[Insert] = insertNode_stub; + context->code[RotateL] = rotateLeft_stub; + context->code[RotateR] = rotateRight_stub; + context->code[InsertCase1] = insert1_stub; + context->code[InsertCase2] = insert2_stub; + context->code[InsertCase3] = insert3_stub; + context->code[InsertCase4] = insert4_stub; + context->code[InsertCase4_1] = insert4_1_stub; + context->code[InsertCase4_2] = insert4_2_stub; + context->code[InsertCase5] = insert5_stub; + context->code[StackClear] = stackClear_stub; + context->code[Exit] = exit_code; + + context->heap = context->heapStart; + + context->data[Allocate] = context->heap; + context->heap += sizeof(struct Allocate); + + context->data[Tree] = context->heap; + context->heap += sizeof(struct Tree); + + context->data[Node] = context->heap; + context->heap += sizeof(struct Node); + + context->dataNum = Node; + + struct Tree* tree = &context->data[Tree]->tree; + tree->root = 0; + tree->current = 0; + tree->deleted = 0; + + context->node_stack = stack_init(sizeof(struct Node*), 100); + context->code_stack = stack_init(sizeof(enum Code), 100); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/insertCase2.c Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,17 @@ +__code insertCase2(struct Context* context, struct Node* current) { + struct Node* parent; + stack_pop(context->node_stack, &parent); + + if (parent->color == Black) { + stack_pop(context->code_stack, &context->next); + goto meta(context, context->next); + } + + stack_push(context->node_stack, &parent); + goto meta(context, InsertCase3); +} + +__code insert2_stub(struct Context* context) { + goto insertCase2(context, context->data[Tree]->tree.current); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/meta.c Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,4 @@ +__code meta(struct Context* context, enum Code next) { + goto (context->code[next])(context); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/rbtreeContext.h Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,50 @@ +// DataSegments for Red-Black Tree +union Data { + struct Comparable { // interface + enum Code compare; + union Data* data; + } compare; + struct Count { + enum Code next; + long i; + } count; + struct Tree { + enum Code next; + struct Node* root; + struct Node* current; + struct Node* deleted; + int result; + } tree; + struct Node { + // need to tree + enum Code next; + int key; // comparable data segment + int value; + struct Node* left; + struct Node* right; + // need to balancing + enum Color { + Red, + Black, + } color; + } node; + struct Allocate { + enum Code next; + long size; + } allocate; +}; + + +// Meta DataSegment +struct Context { + enum Code next; + int codeNum; + __code (**code) (struct Context*); + void* heapStart; + void* heap; + long heapLimit; + int dataNum; + stack_ptr code_stack; + stack_ptr node_stack; + union Data **data; +};
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/singleLinkedStack.c Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,18 @@ +__code pushSingleLinkedStack(struct SingleLinkedStack* stack,union Data* data, __code next(...)) { + Element* element = new Element(); + element->next = stack->top; + element->data = data; + stack->top = element; + goto next(...); +} + +__code popSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) { + if (stack->top) { + data = stack->top->data; + stack->top = stack->top->next; + } else { + data = NULL; + } + goto next(data, ...); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/stack-product.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,158 @@ +module stack-product where + +open import product +open import Data.Product +open import Data.Nat +open import Function using (id) +open import Relation.Binary.PropositionalEquality + +-- definition based from Gears(209:5708390a9d88) src/parallel_execution +goto = executeCS + +data Bool : Set where + True : Bool + False : Bool + +data Maybe (a : Set) : Set where + Nothing : Maybe a + Just : a -> Maybe a + + +record Stack {a t : Set} (stackImpl : Set) : Set where + field + stack : stackImpl + push : CodeSegment (stackImpl × a × (CodeSegment stackImpl t)) t + pop : CodeSegment (stackImpl × (CodeSegment (stackImpl × Maybe a) t)) t + + +data Element (a : Set) : Set where + cons : a -> Maybe (Element a) -> Element a + +datum : {a : Set} -> Element a -> a +datum (cons a _) = a + +next : {a : Set} -> Element a -> Maybe (Element a) +next (cons _ n) = n + +record SingleLinkedStack (a : Set) : Set where + field + top : Maybe (Element a) +open SingleLinkedStack + +emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a +emptySingleLinkedStack = record {top = Nothing} + + + + +pushSingleLinkedStack : {a t : Set} -> CodeSegment ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) t +pushSingleLinkedStack = cs push + where + push : {a t : Set} -> ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) -> t + push (stack , datum , next) = goto next stack1 + where + element = cons datum (top stack) + stack1 = record {top = Just element} + +popSingleLinkedStack : {a t : Set} -> CodeSegment (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t)) t +popSingleLinkedStack = cs pop + where + pop : {a t : Set} -> (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t)) -> t + pop (record { top = Nothing } , nextCS) = goto nextCS (emptySingleLinkedStack , Nothing) + pop (record { top = Just x } , nextCS) = goto nextCS (stack1 , (Just datum1)) + where + datum1 = datum x + stack1 = record { top = (next x) } + + + + + +createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a) +createSingleLinkedStack = record { stack = emptySingleLinkedStack + ; push = pushSingleLinkedStack + ; pop = popSingleLinkedStack + } + + + + +test01 : {a : Set} -> CodeSegment (SingleLinkedStack a × Maybe a) Bool +test01 = cs test01' + where + test01' : {a : Set} -> (SingleLinkedStack a × Maybe a) -> Bool + test01' (record { top = Nothing } , _) = False + test01' (record { top = Just x } , _) = True + + +test02 : {a : Set} -> CodeSegment (SingleLinkedStack a) (SingleLinkedStack a × Maybe a) +test02 = cs test02' + where + test02' : {a : Set} -> SingleLinkedStack a -> (SingleLinkedStack a × Maybe a) + test02' stack = goto popSingleLinkedStack (stack , (cs id)) + + +test03 : {a : Set} -> CodeSegment a (SingleLinkedStack a) +test03 = cs test03' + where + test03' : {a : Set} -> a -> SingleLinkedStack a + test03' a = goto pushSingleLinkedStack (emptySingleLinkedStack , a , (cs id)) + + +lemma : {A : Set} {a : A} -> goto (test03 ◎ test02 ◎ test01) a ≡ False +lemma = refl + + +n-push : {A : Set} {a : A} -> CodeSegment (ℕ × SingleLinkedStack A) (ℕ × SingleLinkedStack A) +n-push {A} {a} = cs (push {A} {a}) + where + push : {A : Set} {a : A} -> (ℕ × SingleLinkedStack A) -> (ℕ × SingleLinkedStack A) + push {A} {a} (zero , s) = (zero , s) + push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , {!!} {- n-push -}) -- needs subtype + + +{- + +n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A +n-push zero s = s +n-push {A} {a} (suc n) s = pushSingleLinkedStack (n-push {A} {a} n s) a (\s -> s) + +n-pop : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A +n-pop zero s = s +n-pop {A} {a} (suc n) s = popSingleLinkedStack (n-pop {A} {a} n s) (\s _ -> s) + +open ≡-Reasoning + +push-pop-equiv : {A : Set} {a : A} (s : SingleLinkedStack A) -> popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ≡ s +push-pop-equiv s = refl + +push-and-n-pop : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {A} {a} n s +push-and-n-pop zero s = refl +push-and-n-pop {A} {a} (suc n) s = begin + n-pop (suc (suc n)) (pushSingleLinkedStack s a id) + ≡⟨ refl ⟩ + popSingleLinkedStack (n-pop (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s) + ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s)) (push-and-n-pop n s) ⟩ + popSingleLinkedStack (n-pop n s) (\s _ -> s) + ≡⟨ refl ⟩ + n-pop (suc n) s + ∎ + + +n-push-pop-equiv : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> (n-pop {A} {a} n (n-push {A} {a} n s)) ≡ s +n-push-pop-equiv zero s = refl +n-push-pop-equiv {A} {a} (suc n) s = begin + n-pop (suc n) (n-push (suc n) s) + ≡⟨ refl ⟩ + n-pop (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s)) + ≡⟨ push-and-n-pop n (n-push n s) ⟩ + n-pop n (n-push n s) + ≡⟨ n-push-pop-equiv n s ⟩ + s + ∎ + + +n-push-pop-equiv-empty : {A : Set} {a : A} -> (n : Nat) -> n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack) ≡ emptySingleLinkedStack +n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack +-} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/stack-subtype-sample.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,212 @@ +module stack-subtype-sample where + +open import Level renaming (suc to S ; zero to O) +open import Function +open import Data.Nat +open import Data.Maybe +open import Relation.Binary.PropositionalEquality + +open import stack-subtype ℕ +open import subtype Context as N +open import subtype Meta as M + + +record Num : Set where + field + num : ℕ + +instance + NumIsNormalDataSegment : N.DataSegment Num + NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c}) + ; set = (\c n -> record c {n = Num.num n})} + NumIsMetaDataSegment : M.DataSegment Num + NumIsMetaDataSegment = record { get = (\m -> record {num = Context.n (Meta.context m)}) + ; set = (\m n -> record m {context = record (Meta.context m) {n = Num.num n}})} + + +plus3 : Num -> Num +plus3 record { num = n } = record {num = n + 3} + +plus3CS : N.CodeSegment Num Num +plus3CS = N.cs plus3 + + + +plus5AndPushWithPlus3 : {mc : Meta} {{_ : N.DataSegment Num}} + -> M.CodeSegment Num (Meta) +plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n -> record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} ) + where + co = Meta.context mc + con : Num -> Context + con record { num = num } = N.DataSegment.set nn co record {num = num + 5} + st = Meta.stack mc + + + + +push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta +push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc + where + con = record { n = 4 ; element = just 0} + code = N.cs (\c -> c) + mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code} + + +push-sample-equiv : push-sample ≡ record { nextCS = liftContext plus3CS + ; stack = record { top = nothing} + ; context = record { n = 9} } +push-sample-equiv = refl + + +pushed-sample : {m : Meta} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta +pushed-sample {m} {{nd}} {{md}} = M.exec {{md}} (M.csComp {m} {{md}} pushSingleLinkedStackCS (plus5AndPushWithPlus3 {mc} {{nd}})) mc + where + con = record { n = 4 ; element = just 0} + code = N.cs (\c -> c) + mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code} + + + +pushed-sample-equiv : {m : Meta} -> + pushed-sample {m} ≡ record { nextCS = liftContext plus3CS + ; stack = record { top = just (cons 0 nothing) } + ; context = record { n = 12} } +pushed-sample-equiv = refl + + + +pushNum : N.CodeSegment Context Context +pushNum = N.cs pn + where + pn : Context -> Context + pn record { n = n } = record { n = pred n ; element = just n} + + +pushOnce : Meta -> Meta +pushOnce m = M.exec pushSingleLinkedStackCS m + +n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta +n-push {{mm}} (zero) = M.cs {{mm}} {{mm}} id +n-push {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-push {m} {{mm}} n) (pushOnce m)) + +popOnce : Meta -> Meta +popOnce m = M.exec popSingleLinkedStackCS m + +n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta +n-pop {{mm}} (zero) = M.cs {{mm}} {{mm}} id +n-pop {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-pop {m} {{mm}} n) (popOnce m)) + + + +initMeta : ℕ -> Maybe ℕ -> N.CodeSegment Context Context -> Meta +initMeta n mn code = record { context = record { n = n ; element = mn} + ; stack = emptySingleLinkedStack + ; nextCS = code + } + +n-push-cs-exec = M.exec (n-push {meta} 3) meta + where + meta = (initMeta 5 (just 9) pushNum) + + +n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS = pushNum + ; context = record {n = 2 ; element = just 3} + ; stack = record {top = just (cons 4 (just (cons 5 (just (cons 9 nothing)))))}} +n-push-cs-exec-equiv = refl + + +n-pop-cs-exec = M.exec (n-pop {meta} 4) meta + where + meta = record { nextCS = N.cs id + ; context = record { n = 0 ; element = nothing} + ; stack = record {top = just (cons 9 (just (cons 8 (just (cons 7 (just (cons 6 (just (cons 5 nothing)))))))))} + } + +n-pop-cs-exec-equiv : n-pop-cs-exec ≡ record { nextCS = N.cs id + ; context = record { n = 0 ; element = just 6} + ; stack = record { top = just (cons 5 nothing)} + } + +n-pop-cs-exec-equiv = refl + + +open ≡-Reasoning + +id-meta : ℕ -> ℕ -> SingleLinkedStack ℕ -> Meta +id-meta n e s = record { context = record {n = n ; element = just e} + ; nextCS = (N.cs id) ; stack = s} + +exec-comp : (f g : M.CodeSegment Meta Meta) (m : Meta) -> M.exec (M.csComp {m} f g) m ≡ M.exec f (M.exec g m) +exec-comp (M.cs x) (M.cs _) m = refl + + +push-pop-type : ℕ -> ℕ -> ℕ -> Element ℕ -> Set₁ +push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta + where + meta = id-meta n e record {top = just (cons x (just s))} + +push-pop : (n e x : ℕ) -> (s : Element ℕ) -> push-pop-type n e x s +push-pop n e x s = refl + + + +pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ +pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta + ≡ M.exec (n-push {meta} n) meta + where + meta = id-meta cn ce s + +pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s + +pop-n-push zero cn ce s = refl +pop-n-push (suc n) cn ce s = begin + M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc (suc n)))) (id-meta cn ce s) + ≡⟨ refl ⟩ + M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce))) (id-meta cn ce s) + ≡⟨ exec-comp (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩ + M.exec (M.cs popOnce) (M.exec (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s)) + ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩ + M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s))) + ≡⟨ refl ⟩ + M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) + ≡⟨ sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩ + M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) + ≡⟨ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩ + M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) + ≡⟨ refl ⟩ + M.exec (n-push n) (pushOnce (id-meta cn ce s)) + ≡⟨ refl ⟩ + M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s)) + ≡⟨ refl ⟩ + M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s) + ∎ + + + +n-push-pop-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ +n-push-pop-type n cn ce st = M.exec (M.csComp {meta} (n-pop {meta} n) (n-push {meta} n)) meta ≡ meta + where + meta = id-meta cn ce st + +n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s +n-push-pop zero cn ce s = refl +n-push-pop (suc n) cn ce s = begin + M.exec (M.csComp {id-meta cn ce s} (n-pop {id-meta cn ce s} (suc n)) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s) + ≡⟨ refl ⟩ + M.exec (M.csComp {id-meta cn ce s} (M.cs (\m -> M.exec (n-pop {id-meta cn ce s} n) (popOnce m))) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s) + ≡⟨ exec-comp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s) ⟩ + M.exec (M.cs (\m -> M.exec (n-pop {id-meta cn ce s} n) (popOnce m))) (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)) + ≡⟨ refl ⟩ + M.exec (n-pop n) (popOnce (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s))) + ≡⟨ refl ⟩ + M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s))) + ≡⟨ cong (\x -> M.exec (n-pop {id-meta cn ce s} n) x) (sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s))) ⟩ + M.exec (n-pop n) (M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s)) + ≡⟨ cong (\x -> M.exec (n-pop {id-meta cn ce s} n) x) (pop-n-push n cn ce s) ⟩ + M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s)) + ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩ + M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s) + ≡⟨ n-push-pop n cn ce s ⟩ + id-meta cn ce s + ∎ +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/stack-subtype.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,123 @@ +open import Level hiding (lift) +open import Data.Maybe +open import Data.Product +open import Data.Nat hiding (suc) +open import Function + +module stack-subtype (A : Set) where + +-- data definitions + +data Element (a : Set) : Set where + cons : a -> Maybe (Element a) -> Element a + +datum : {a : Set} -> Element a -> a +datum (cons a _) = a + +next : {a : Set} -> Element a -> Maybe (Element a) +next (cons _ n) = n + +record SingleLinkedStack (a : Set) : Set where + field + top : Maybe (Element a) +open SingleLinkedStack + +record Context : Set where + field + -- fields for concrete data segments + n : ℕ + -- fields for stack + element : Maybe A + + + + + +open import subtype Context as N + +instance + ContextIsDataSegment : N.DataSegment Context + ContextIsDataSegment = record {get = (\c -> c) ; set = (\_ c -> c)} + + +record Meta : Set₁ where + field + -- context as set of data segments + context : Context + stack : SingleLinkedStack A + nextCS : N.CodeSegment Context Context + + + + +open import subtype Meta as M + +instance + MetaIncludeContext : M.DataSegment Context + MetaIncludeContext = record { get = Meta.context + ; set = (\m c -> record m {context = c}) } + + MetaIsMetaDataSegment : M.DataSegment Meta + MetaIsMetaDataSegment = record { get = (\m -> m) ; set = (\_ m -> m) } + + +liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y +liftMeta (N.cs f) = M.cs f + +liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context +liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c))) + +-- definition based from Gears(209:5708390a9d88) src/parallel_execution + +emptySingleLinkedStack : SingleLinkedStack A +emptySingleLinkedStack = record {top = nothing} + + +pushSingleLinkedStack : Meta -> Meta +pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) }) + where + n = Meta.nextCS m + s = Meta.stack m + e = Context.element (Meta.context m) + push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A + push s nothing = s + push s (just x) = record {top = just (cons x (top s))} + + + +popSingleLinkedStack : Meta -> Meta +popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}}) + where + n = Meta.nextCS m + con = Meta.context m + elem : Meta -> Maybe A + elem record {stack = record { top = (just (cons x _)) }} = just x + elem record {stack = record { top = nothing }} = nothing + st : Meta -> SingleLinkedStack A + st record {stack = record { top = (just (cons _ s)) }} = record {top = s} + st record {stack = record { top = nothing }} = record {top = nothing} + + + + +pushSingleLinkedStackCS : M.CodeSegment Meta Meta +pushSingleLinkedStackCS = M.cs pushSingleLinkedStack + +popSingleLinkedStackCS : M.CodeSegment Meta Meta +popSingleLinkedStackCS = M.cs popSingleLinkedStack + + +-- for sample + +firstContext : Context +firstContext = record {element = nothing ; n = 0} + + +firstMeta : Meta +firstMeta = record { context = firstContext + ; stack = emptySingleLinkedStack + ; nextCS = (N.cs (\m -> m)) + } + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/stack.h Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,7 @@ +struct SingleLinkedStack { + struct Element* top; +} SingleLinkedStack; +struct Element { + union Data* data; + struct Element* next; +} Element;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/struct-init.c Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,1 @@ +struct Point p = {100 , 200};
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/struct.c Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,4 @@ +struct Point { + int x; + int y; +};
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/stub.cbc Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,17 @@ +__code put(struct Context* context, + struct Tree* tree, + struct Node* root, + struct Allocate* allocate) +{ + /* 実装コードは省略 */ +} + +__code put_stub(struct Context* context) +{ + goto put(context, + &context->data[Tree]->tree, + context->data[Tree]->tree.root, + &context->data[Allocate]->allocate); +} + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/subtype.agda Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,44 @@ +open import Level +open import Relation.Binary.PropositionalEquality + +module subtype {l : Level} (Context : Set l) where + + +record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where + field + get : Context -> A + set : Context -> A -> Context +open DataSegment + +data CodeSegment {l1 l2 : Level} (A : Set l1) (B : Set l2) : Set (l ⊔ l1 ⊔ l2) where + cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B + +goto : {l1 l2 : Level} {I : Set l1} {O : Set l2} -> CodeSegment I O -> I -> O +goto (cs b) i = b i + +exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}} + -> CodeSegment I O -> Context -> Context +exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c)) + + +comp : {con : Context} -> {l1 l2 l3 l4 : Level} + {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4} + {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}} + -> (C -> D) -> (A -> B) -> A -> D +comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x))) + +csComp : {con : Context} -> {l1 l2 l3 l4 : Level} + {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4} + {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}} + -> CodeSegment C D -> CodeSegment A B -> CodeSegment A D +csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} (cs g) (cs f) + = cs {{da}} {{dd}} (comp {con} {{da}} {{db}} {{dc}} {{dd}} g f) + + + +comp-associative : {A B C D E F : Set l} {con : Context} + {{da : DataSegment A}} {{db : DataSegment B}} {{dc : DataSegment C}} + {{dd : DataSegment D}} {{de : DataSegment E}} {{df : DataSegment F}} + -> (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F) + -> csComp {con} c (csComp {con} b a) ≡ csComp {con} (csComp {con} c b) a +comp-associative (cs _) (cs _) (cs _) = refl
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/type-cs.c Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,9 @@ +__code getMinHeight_stub(struct Context* context) { + goto getMinHeight(context, &context->data[Allocate]->allocate, &context->data[AkashaInfo]->akashaInfo); +} + +__code getMinHeight(struct Context* context, struct Allocate* allocate, struct AkashaInfo* akashaInfo) { + /* ... */ + goto getMinHeight_stub(context); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/type-ds.h Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,5 @@ +struct AkashaInfo { + unsigned int minHeight; + unsigned int maxHeight; + struct AkashaNode* akashaNode; +};
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/src/type-mds.h Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,15 @@ +struct Data { /* data segments as types */ + struct Tree { /* ... */ } tree; + struct Node { /* ... */ } node; + + struct IterElem { /* ... */ } iterElem; + struct Iterator { /* ... */ } iterator; + struct AkashaInfo { /* ... */} akashaInfo; + struct AkashaNode { /* ... */} akashaNode; +}; + + +struct Context { /* meta data segment as subtype */ + /* ... fields for meta computations ... */ + struct Data **data; /* data segments */ +};
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/final_main/thanks.tex Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,17 @@ +\chapter*{謝辞} +\thispagestyle{empty} + +%基本的な内容は以下の通り．参考にしてみて下さい． +%厳密な決まりは無いので，個々人の文体でも構わない． +%GISゼミや英語ゼミに参加した人はその分も入れておく． +%順番は重要なので気を付けるように．(提出前に周りの人に確認してもらう．) + +\hspace{1zw} + +謝辞だよ。 + +%% \begin{flushright} +%% % 2018年 3月 \\ 仲松 栞 +%% \end{flushright} + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/suruga-thesis/thesis.mm Thu Feb 15 14:46:18 2018 +0900 @@ -0,0 +1,92 @@ +<map version="1.1.0"> +<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> +<node CREATED="1516447600591" ID="ID_1323189017" MODIFIED="1516447624027" TEXT="thesis"> +<node CREATED="1516447625087" FOLDED="true" ID="ID_1724518003" MODIFIED="1517385478036" POSITION="left" TEXT="はじめに"> +<node CREATED="1516448006125" ID="ID_801881892" MODIFIED="1516448107906" TEXT="動作するプログラムの信頼性を保証したい"/> +<node CREATED="1516448247561" ID="ID_951851740" MODIFIED="1516448282443" TEXT="CodeSegment,DataSegmentという単位でプログラムを書く手法を提案している"/> +<node CREATED="1516448220906" ID="ID_182832086" MODIFIED="1516448412313" TEXT="CbC(Continuation based C )ではこのようにプログラムを記述することでメタ計算として検証をすることができた（あっとんさんの論文）"/> +<node CREATED="1516448414254" ID="ID_1047962267" MODIFIED="1516448573215" TEXT="CbCでは自身で証明をすることができない為、（何らかの理由で）Agdaを使って証明する"/> +<node CREATED="1516448574477" ID="ID_1442131681" MODIFIED="1516453035591" TEXT="本研究ではAgdaでCodeSegment、DataSegmentという単位を使ってCbCで記述したものと等価なUnbarrancedTreeを作り、ノードを入れる際ノードがなくならないこと、などを証明をする"/> +</node> +<node CREATED="1516447638226" FOLDED="true" ID="ID_1889545574" MODIFIED="1517385480087" POSITION="left" TEXT="基礎概念"> +<node CREATED="1516448673422" ID="ID_1274177968" MODIFIED="1516448683325" TEXT="CbC"> +<node CREATED="1516448708973" ID="ID_815925469" MODIFIED="1516454414422" TEXT="CodeSegmentとは"> +<node CREATED="1516454422237" ID="ID_661052887" MODIFIED="1516454424583" TEXT="例題"/> +</node> +<node CREATED="1516448719701" ID="ID_1017753652" MODIFIED="1516454421110" TEXT="DataSegmentとは"> +<node CREATED="1516454425392" ID="ID_221829180" MODIFIED="1516454427407" TEXT="例題"/> +</node> +<node CREATED="1517214307007" ID="ID_1524511628" MODIFIED="1517214330536" TEXT="Metaな話は多分いらない"/> +</node> +<node CREATED="1516448684110" ID="ID_1770419109" MODIFIED="1517214374341" TEXT="Agda"> +<node CREATED="1516454190133" ID="ID_445682748" MODIFIED="1516454207271" TEXT="その他の証明支援系"/> +<node CREATED="1516454167956" ID="ID_1326840818" MODIFIED="1516454171204" TEXT="記述方法"/> +<node CREATED="1516454171715" ID="ID_1880237124" MODIFIED="1516454184781" TEXT="例題"/> +</node> +<node CREATED="1516448688109" ID="ID_594761054" MODIFIED="1516448692742" TEXT="証明"> +<node CREATED="1516454132267" ID="ID_1490526606" MODIFIED="1516693045587" TEXT="自然証明"> +<node CREATED="1517214338214" ID="ID_794688351" MODIFIED="1517214354528" TEXT="説明"/> +<node CREATED="1516454431900" ID="ID_1113949900" MODIFIED="1516454434111" TEXT="例題"/> +</node> +<node CREATED="1516454140637" ID="ID_1834687592" MODIFIED="1516455188550" TEXT="カリーハワード同型対応"/> +<node CREATED="1517214363342" ID="ID_1381920910" MODIFIED="1517214367584" TEXT="Agdaでの証明"/> +</node> +<node CREATED="1516448778576" ID="ID_1454457815" MODIFIED="1516453085568" TEXT="Tree,RedBlackTree"/> +</node> +<node CREATED="1516448781436" FOLDED="true" ID="ID_732614714" MODIFIED="1517385481609" POSITION="left" TEXT="実験"> +<node CREATED="1516448792793" ID="ID_590034820" MODIFIED="1516448919993" TEXT="Treeの作成方針"/> +<node CREATED="1516448843266" ID="ID_1177321611" MODIFIED="1516454291651" TEXT="証明方針の検討,実装時の改善"/> +</node> +<node CREATED="1516448766134" FOLDED="true" ID="ID_712304841" MODIFIED="1517385482976" POSITION="left" TEXT="実装"> +<node CREATED="1516448769994" ID="ID_1122278060" MODIFIED="1516453267632" TEXT="CbCでの実装"/> +<node CREATED="1516453268445" ID="ID_1239636691" MODIFIED="1516453272713" TEXT="Agdaでの実装"/> +<node CREATED="1516453273168" ID="ID_1420286449" MODIFIED="1516454130460" TEXT="Agdaでの証明,解説"/> +</node> +<node CREATED="1516455668900" FOLDED="true" ID="ID_155403381" MODIFIED="1517385484966" POSITION="left" TEXT="評価"> +<node CREATED="1516455671828" ID="ID_1828774278" MODIFIED="1516455677370" TEXT="?"/> +</node> +<node CREATED="1516448787093" FOLDED="true" ID="ID_1477806830" MODIFIED="1517385486194" POSITION="left" TEXT="結論"> +<node CREATED="1516453116787" ID="ID_1750859738" MODIFIED="1516453146188" TEXT="TreeをCodeSegment,DataSegmentを用いて二つの言語で記述した"/> +<node CREATED="1516453146841" ID="ID_495843685" MODIFIED="1516695852072" TEXT="等価なコードができた?"/> +<node CREATED="1516453179338" ID="ID_710713278" MODIFIED="1516695815136" TEXT="証明支援器を使ってunBalanceなTreeができることを証明した?"/> +<node CREATED="1516693502350" ID="ID_1803347987" MODIFIED="1516695887153" TEXT="その他、今後の話"> +<node CREATED="1516693505485" ID="ID_727445874" MODIFIED="1516693962403" TEXT="CbCのコンパイル時にTypeCheckingもできるかもしれないねみたいなはなし"/> +</node> +</node> +<node CREATED="1516695662563" ID="ID_1054440656" MODIFIED="1516695667362" POSITION="right" TEXT="章構成"> +<node CREATED="1516695644106" ID="ID_736329900" MODIFIED="1516695909066" TEXT="研究背景"> +<node CREATED="1517385504371" ID="ID_201034437" MODIFIED="1517385507130" TEXT="はじめに"/> +</node> +<node CREATED="1517384887536" ID="ID_1535504778" MODIFIED="1517384893658" TEXT="CbC"> +<node CREATED="1516695675644" ID="ID_922716453" MODIFIED="1517385660735" TEXT="CodeSegmentとDataSegment"/> +<node CREATED="1517385681042" ID="ID_1583563260" MODIFIED="1517385703041" TEXT="CbCの記述"> +<node CREATED="1517385703503" ID="ID_298253554" MODIFIED="1517385713098" TEXT="CbC上でのCodeSegmentの例"/> +<node CREATED="1517385714282" ID="ID_87445580" MODIFIED="1517385732747" TEXT="CbC上でのDataSegmentの例"/> +</node> +</node> +<node CREATED="1516695699548" ID="ID_1160729877" MODIFIED="1517384881720" TEXT="Agda"> +<node CREATED="1517385743439" ID="ID_948325222" MODIFIED="1517385763996" TEXT="Agda文法"/> +<node CREATED="1516695675644" ID="ID_1174205441" MODIFIED="1517385787006" TEXT="Agda での CodeSegment、DataSegmentの例"/> +<node CREATED="1516695711821" ID="ID_886806884" MODIFIED="1517385815751" TEXT="Agda でのInterface部分の例"/> +</node> +<node CREATED="1516695693068" ID="ID_1567452235" MODIFIED="1517214279808" TEXT="証明とプログラミング"> +<node CREATED="1517385849109" ID="ID_808144723" MODIFIED="1517385854297" TEXT="自然演繹"/> +<node CREATED="1517385855121" ID="ID_910986235" MODIFIED="1517385874635" TEXT="Curry-Howard同型対応"/> +<node CREATED="1517385877162" ID="ID_869768510" MODIFIED="1517385926540" TEXT="Agdaと自然演繹の証明の例(たぶん三段論法になる?)"/> +</node> +<node CREATED="1516695770479" ID="ID_289839920" MODIFIED="1517214287535" TEXT="Agdaでの証明"> +<node CREATED="1517385826823" ID="ID_778238289" MODIFIED="1517385842945" TEXT="Interface部分の証明(stack,tree)"/> +</node> +<node CREATED="1516695962331" ID="ID_1727743322" MODIFIED="1516695964397" TEXT="まとめ"> +<node CREATED="1517384473095" ID="ID_1131464081" MODIFIED="1517385933785" TEXT="いいたいとこ"> +<node CREATED="1517384520003" ID="ID_1024027966" MODIFIED="1517384562444" TEXT="Agdaで記述することでGearsの文法的曖昧な部分が明確化された"/> +<node CREATED="1517384563497" ID="ID_1552767038" MODIFIED="1517384599221" TEXT="先行研究との違い"> +<node CREATED="1517384599498" ID="ID_7745421" MODIFIED="1517384649848" TEXT="ノーマルレベルでのインターフェース部分の記述"/> +<node CREATED="1517384690992" ID="ID_895803544" MODIFIED="1517384717943" TEXT="インターフェースを使って抽象化した(stack,tree))"/> +<node CREATED="1517384651337" ID="ID_1071842343" MODIFIED="1517384658640" TEXT="インターフェース部分の証明"/> +</node> +</node> +</node> +</node> +</node> +</map>
--- a/分散版jungleデータベースの性能想定方法.mm Thu Feb 01 22:01:16 2018 +0900 +++ b/分散版jungleデータベースの性能想定方法.mm Thu Feb 15 14:46:18 2018 +0900 @@ -1,6 +1,6 @@ <map version="1.0.1"> <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> -<node CREATED="1517398052968" ID="ID_1630312179" MODIFIED="1517489946519" TEXT="分散版jungleデータベースの性能測定方法"> +<node CREATED="1517398052968" ID="ID_1630312179" MODIFIED="1517494769565" TEXT="分散版jungleデータベースの性能測定方法"> <node CREATED="1517398073287" ID="ID_165185668" MODIFIED="1517398283946" POSITION="right" TEXT="研究目的"> <node CREATED="1517399672148" ID="ID_88058044" MODIFIED="1517399681279" TEXT="スケーラビリティ"> <node CREATED="1517399685966" ID="ID_33794870" MODIFIED="1517399704649" TEXT="スマホやタブレットの普及"/> @@ -90,6 +90,7 @@ <node CREATED="1517405843195" ID="ID_824132120" MODIFIED="1517405851941" TEXT="実験目的"> <node CREATED="1517489621897" ID="ID_141089909" MODIFIED="1517489637973" TEXT="java版jungleの性能を正確に計りたい"> <node CREATED="1517489662514" ID="ID_1388356588" MODIFIED="1517489760933" TEXT="これまで行われていたjungleの性能を測定する実験の概要(この項は実験目的か、または測定環境のところに書くべきか)"/> +<node CREATED="1517491912768" ID="ID_1758077162" MODIFIED="1517491940161" TEXT="Huskell版jungleとjava版jungleのコード量や複雑度？の比較？"/> </node> <node CREATED="1517406272151" ID="ID_683474142" MODIFIED="1517406487204" TEXT="jungleに分散性能があるか"> <node CREATED="1517406490583" ID="ID_440672906" MODIFIED="1517406551790" TEXT="分散機能を備えたデータベースとして開発していたが、実際に実験をしてその機能を確認することはできていなかった。"/>