Mercurial > hg > Papers > 2020 > ryokka-master
changeset 1:ee44dbda6bd3
fix
| author | ryokka |
|---|---|
| date | Thu, 16 Jan 2020 19:21:45 +0900 |
| parents | 41a936510fd0 |
| children | c7acb9211784 |
| files | paper/Makefile paper/agda.tex paper/cbc.tex paper/hoare.tex paper/reference.bib ryokka-master.mm |
| diffstat | 6 files changed, 593 insertions(+), 225 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/Makefile Thu Jan 02 21:25:52 2020 +0900 +++ b/paper/Makefile Thu Jan 16 19:21:45 2020 +0900 @@ -32,7 +32,7 @@ .PHONY : clean all open remake clean: - rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg *.idx src/*.replaced + rm -f *.dvi *.aux *.log *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg *.idx src/*.replaced all: $(TARGET).pdf
--- a/paper/agda.tex Thu Jan 02 21:25:52 2020 +0900 +++ b/paper/agda.tex Thu Jan 16 19:21:45 2020 +0900 @@ -1,14 +1,175 @@ \chapter{Agda} -Agda についての説明 +Adga \cite{agda} とは証明支援系の関数型言語である。 +Agda は依存型という型システムを持つ。依存型とは型も第一級オブジェクトとする型シ +ステムで、依存型を持っている言語では型を基本的な操作に制限なしに使用できる +。 +型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応する。 + +本章では Agda で証明をするために必要な要素について説明を行う。 +また、定理証明支援器としての Agda について解説する。 + +\section{Agda の文法} + +Agda はインデントに意味を持つため、きちんと揃える必要がある。 +また、スペースの有無は厳格にチェックされる。 +なお、 \verb/--/ の後はコメントである。 + +Agda のプログラムでは全てモジュール内部に記述されるため、まずはトップレベルにモ +ジュールを定義する必要がある。トップレベルのモジュールはファイル名と同一になる。 + +通常のモジュールをインポートする時は \verb/import/ キーワードを指定する。 +また、インポートを行なう際に名前を別名に変更することもでき、その際は \verb/as/ キーワードを用いる。 +モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワードの後に +関数名を、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠 +す場合は \verb/hiding/ キーワードを用いる。 +なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/opestack に対する操作を定義しており、n/ キーワードを使うことで展開できる。 +モジュールをインポートする例をリスト~\ref{src:agda-import}に示す。 -\section{Agda の Data Type} -data とか record とか +\lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda} + +Agda における型指定は $:$ を用いて行う。 + +例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。 + + +\section{Agda のデータ} +Agdaにおける型指定は : を用いて行う。例えば、 変数 x が型 A を持つ、ということを表すには x : A と記述する。 +データ型は、代数的なデータ構造で、その定義には data キーワードを用いる。 +data キーワードの後に data の名前と、型、 where 句を書きインデントを深 くした後、 +値にコンストラクタとその型を列挙する。 + +Agda には C における構造体に相当するレコード型というデータも存在する、 +record キーワード後の内部に field キーワードを記述し、その下に Name = value の形で値を列挙していく。 +複数の値を列挙する際は ; で区切る必要がある。 + +データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。 +\verb/data/キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。 +例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。 +Bool はコンストラクタ \verb/true/ と \verb/false/ を持つデータ型である。 +Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。 +Set は階層構造を持ち、型集合の集合の型を指定するには Set1 と書く + +\lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda} + \section{Agda の関数} -関数定義だったり型とかの話 +%% 関数の定義は、関数名と型を記述した後に関数の本体を = の後に記述する。関数の型には → 、または$->$ を用いる。 +%% 例えば引数が型 A で返り値が型 B の関数は A $->$ B のように書ける。また、複数の引数を取る関数の型は A $->$ A $->$ B のように書ける。この時の型は A $->$ (A $->$ B) のように考えられる。 + + +関数の定義は、関数名と型を記述した後に関数の本体を \verb/=/ の後に記述する。 +関数の型には $ \rightarrow $ 、 または\verb/->/ を用いる。 + +例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書 +ける。 +また、複数の引数を取る関数の型は \verb/A -> A -> B/ のように書ける。この +時の型は \verb/A -> (A -> B)/のように考えられる。 +Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{src:agda-function}のようになる。 + +\lstinputlisting[label=src:agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda} + +引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 +これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなもので +例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。 + +\lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda} + +パターンマッチでは全てのコンストラクタのパターンを含まなくてはならない。 +例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。 +なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。 +例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。 +なお、マッチした値以外の挙動をまとめて書く際には \verb/_/ を用いることもできる。 + +\lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda} + +Agda にはラムダ計算が存在している。ラムダ計算とは関数内で生成できる無名の関数であり、 +\verb/\arg1 arg2 -> function body/ のように書くことができる。 +例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ計算で書くとリスト~\ref{src:agda-lambda}のようになる。 +関数 \verb/not-apply/ をラムダ計算を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。 + +\lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda} + +Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。 +スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。 +例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト~\ref{src:agda-where} のように書ける。 +これは \verb/f'/ と同様の動作をする。 +\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。 + +\lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda} + + +\section{定理証明支援器としての Agda} +Agda での証明では型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明が完成する。 +証明の例として Code \ref{proof} を見る。 +ここでの $+zero$ は右から zero を足しても $\equiv$ の両辺は等しいことを証明している。 +これは、引数として受けている y が Nat なので、 zero の時と suc y の二つの場合を証明する必要がある。 + +$y = zero$ の時は両辺が zero とできて、左右の項が等しいということを表す refl で証明することができる。 +$y = suc y$ の時は x == y の時 fx == fy が成り立つという cong を使って、y の値を 1 減らしたのちに再帰的に $+zero y$ +を用いて証明している。 -\section{Agda での検証} -検証の話 +\lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced} +%% \begin{lstlisting}[caption=等式変形の例,label=proof] +%% +zero : { y : ℕ } → y + zero ≡ y +%% +zero {zero} = refl +%% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) +%% \end{lstlisting} + +また、他にも $\lambda$ 項部分で等式を変形する構文が存在している。 + Code \ref{agda-term-pre}、 \ref{agda-term-post} は等式変形の例である。 +始めに等式変形を始めたいところで $let open \equiv-Reasoning in begin$と記述する。 +Agda 上では分からないところを ? と置いておくことができるので、残りを ? としておく。 +$--$ は Agda 上ではコメントである。 + +\lstinputlisting[caption=等式変形の例1/2,label=agda-term-pre]{src/term1.agda.replaced} +%% \begin{lstlisting}[caption=等式変形の例1/3,label=agda-term-pre] +%% stmt2Cond : {c10 : ℕ} → Cond +%% stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) + +%% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ +%% 10}) +%% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in +%% begin +%% ? -- ?0 +%% ≡⟨ ? ⟩ -- ?1 +%% ? -- ?2 +%% ∎ ) + +%% -- ?0 : Bool +%% -- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) ≡ true +%% -- ?2 : Bool +%% \end{lstlisting} + +この状態で実行すると ? 部分に入る型を Agda が示してくれる。 +始めに変形する等式を ?0 に記述し、?1 の中に $x == y$ のような変形規則を入れることで等式を変形して証明することができる。 + +ここでは \ref{agda-term-mid} の Bool 値 x を受け取って $x \wedge true$ の時必ず x であるという証明 $\wedge$true と 値と Env を受け取って Bool 値を返す stmt1Cond を使って等式変形を行う。 +\lstinputlisting[caption=使っている等式変形規則,label=agda-term-mid]{src/term2.agda.replaced} +%% \begin{lstlisting}[caption=等式変形の例2/3,label=agda-term-mid] +%% ∧true : { x : Bool } → x ∧ true ≡ x +%% ∧true {x} with x +%% ∧true {x} | false = refl +%% ∧true {x} | true = refl + +%% stmt1Cond : {c10 : ℕ} → Cond +%% stmt1Cond {c10} env = Equal (varn env) c10 +%% \end{lstlisting} + +最終的な証明は\ref{agda-term-post} のようになる。 +\lstinputlisting[caption=等式変形の例2/2,label=agda-term-post]{src/term3.agda.replaced} +%% \begin{lstlisting}[caption=等式変形の例2/2,label=agda-term-post] +%% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ +%% 10}) +%% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in +%% begin +%% (Equal (varn env) c10 ) ∧ true +%% ≡⟨ ∧true ⟩ +%% Equal (varn env) c10 +%% ≡⟨ cond ⟩ +%% true +%% ∎ ) +%% \end{lstlisting} + \section{定理証明とプログラミング検証} たぶん Curry-Howard isomorphism の話
--- a/paper/cbc.tex Thu Jan 02 21:25:52 2020 +0900 +++ b/paper/cbc.tex Thu Jan 16 19:21:45 2020 +0900 @@ -1,13 +1,80 @@ % だいたい sigss のやつ \chapter{Continuation based C} -CbC について +Continuation based C\cite{cbc} (以下 CbC) は CodeGear を処理の単位、 DataGear をデータの単位として記述するプログラミング言語である。 CbC は C 言語とほぼ同じ構文を持つが、よりアセンブラに近いプログラムを記述することになる。 +CbC でのプログラミングは DataGear を CodeGear で変更し、その変更を次の CodeGear に渡して処理を実行する。 +現在 CbC の処理系には llvm/clang による実装\cite{llvm}と gcc\cite{gcc} による実装が存在している。 + +本章は CbC について説明する。 \section{Code GearとData Gear} -概念 +本研究室では検証しやすいプログラムの単位として CodeGear と DataGear という +単位を用いるプログラミングスタイルを提案している。 + +CodeGear とは処理を行う単位である。 + +DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータである。 +CodeGear の入力となる DataGear を Input DataGear と呼び、 +出力は Output DataGear と呼ぶ。 + +図\ref{fig:csds}のように Input DataGear を受け取り、 CodeGear で処理を行い、 +Output DataGear に変更を加え、プログラム全体を記述する。 +% CS,DSの図 +\begin{figure}[htpb] + \begin{center} + \scalebox{0.55}{\includegraphics{fig/csds.pdf}} + \end{center} + \caption{CodeGear と DataGear} + \label{fig:csds} +\end{figure} + + + +%% Gears OS ではプログラムとデータの単位として CodeGear、 DataGear を用いる。 Gear +%% は並列実行の単位、データ分割、 Gear 間の接続等になる。 +%% CodeGear はプログラムの処理そのもので、図 Code \ref{fig:cgdg}で示しているように任意の数の +%% Input DataGear を参照し、処理が完了すると任意の数の Output DataGear に書き込む。 + +%% CodeGear 間の移動は継続を用いて行われる。継続は関数呼び出しとは異なり、呼び出し +%% た後に元のコードに戻らず、次の CodeGear へ継続を行う。 +%% これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。 + +%% \begin{figure}[htpb] +%% \begin{center} +%% \scalebox{0.425}{\includegraphics{pic/meta_cg_dg.pdf}} +%% \end{center} +%% \caption{CodeGear と DataGear の関係} +%% \label{fig:cgdg} +%% \end{figure} + + \section{メタ計算} -メタ計算の話 + +%% プログラムの記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、CPUがGPUの資源管理等を記述しなければならない処理が存在する。 +%% これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ。 +メタ計算(自己反映計算)\cite{weko_5056_1} とはプログラムを記述する際に通常の処理 +と分離し、他に記述しなければならない処理である。例えばプログラム実行時のメモリ管 +理やスレッド管理、資源管理等の計算がこれに当たる。 + +メタ計算は関数型言語では Monad\cite{moggi-monad} を用いて表現される\cite{kkb-sigos}。 +Monad は Haskell では実行時の環境を記述する構文として使われる。 -\section{Meta Gear} -Meta Gears の概念 +従来の OS では、メタ計算はシステムコールやライブラリーコールの単位で行われる。 +実行時にメタ計算の変更を行う場合には OS 内部のパラメータの変更を使用し、実行されるユーザープログラム自体への変更は限定的である。 +しかし、メタ計算は性能測定あるいはプログラム検証、さらに並列分散計算のチューニングなど細かい処理が必要で実際のシステムコール単位では不十分である。 +例えば、モデル検査ではアセンブラあるいは バイトコード、インタプリタレベルでのメタ計算が必要になる。 +しかし、バイトコードレベルでは 粒度が細かすぎて扱いが困難になっている。具体的にはメタ計算の実行時間が大きくなってしまう。 + +\section{Context} +CbC では、接続可能な CodeGear、 DataGear のリスト、Temporal DataGear のためのメモリ空間などを +Context として保持している。 +CbC で必要な CodeGear 、 DataGear を参照する際は Context を通してアクセスする。 + + +\section{Meta Gears} +Meta Gear は CbC 上でのメタ計算である。 +CodeGear を実行する際、必要な DataGear を Context から取得する必要がある。 +しかし、 ユーザーが Context から直接データを扱える状態は信頼性を欠く。 +そのため、 CbC では Meta CodeGear を用いて Context から必要な DataGear を取り出し、 CodeGear に接続する stub CodeGear という Meta Gear を定義している。 +
--- a/paper/hoare.tex Thu Jan 02 21:25:52 2020 +0900 +++ b/paper/hoare.tex Thu Jan 16 19:21:45 2020 +0900 @@ -1,17 +1,205 @@ \chapter{Floyd-Hoare Logic} -HoareLogic の話 +HoareLogic\cite{hoare} とは C.A.R Hoare、 R.W Floyd らによるプログラムの検証の手法である。 +HoareLogic では事前条件(Pre-Condition)が成り立つとき、何らかの計算(Command)を実行した後に +事後条件(Post-Condition)が成り立つことを検証する。 +事前条件を P 、 何らかの計算を C 、 事後条件を Q としたとき、 ${P} C {Q}$ といった形で表される。 +この ${P} C {Q}$ のことを HoareTriple と呼ぶ。 +HoareTriple ではプログラムの部分的な正当性を検証することができ、 +Q のあとに別の C をつなげてプログラムを構築し、すべての実行を検証することができる。 + +\section{Agda での Hoare Logic システムの構築} +現在 Agda 上での HoareLogic は初期の Agda で実装されたもの \cite{agda-alpa}とそれを現在の Agda に対応させたもの \cite{agda2-hoare}が存在している。 + +例として Agda に対応させたもの \cite{agda2-hoare}の Command と証明のためのルールを使って HoareLogic を実装した。 + Code \ref{agda-hoare} は Agda上での HoareLogic の構築子である。 +ここでの Comm は Agda2 に対応した Command の定義を使用している。 + +例として Code \ref{agda-while} のようなプログラムを記述した。 + +\begin{lstlisting}[caption=while Loop Program,label=agda-while] + n = 10; + i = 0; + + while (n>0) + { + i++; + n--; + } +\end{lstlisting} + +$Env$ は Code \ref{agda-while}の n、 i といった変数をまとめたものであり、型として Agda 上での自然数の型である Nat を持つ。 + +PrimComm は Primitive Command で、 n、i といった変数に 代入するときに使用される関数である。 + +Cond は HoareLogic の Condition で、 Env を受け取って Bool 値を返す関数となっている。 + +Agda のデータで定義されている Comm は HoareLogic での Command を表す。 + +Skip は何も変更しない Command で、 Abort はプログラムを中断する Command である。 + +PComm は PrimComm を受けて Command を返す型で定義されており、 変数を代入するときに使われる。 + +Seq は Sequence で Command を2つ受けて Command を返す型で定義されている。 +これは、ある Command から Command に移り、その結果を次の Command に渡す型になっている。 + +If は Cond と Comm を2つ受け取り、 Cond が true か false かで 実行する Comm を変える Command である。 + +While は Cond と Comm を受け取り、 Cond の中身が True である間、 Comm を繰り返す Command である。 + +\begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare] +PrimComm : Set +PrimComm = Env → Env -\section{Hoare Triple} -HoareLogic の概念 +Cond : Set +Cond = (Env → Bool) + +data Comm : Set where + Skip : Comm + Abort : Comm + PComm : PrimComm -> Comm + Seq : Comm -> Comm -> Comm + If : Cond -> Comm -> Comm -> Comm + While : Cond -> Comm -> Comm +\end{lstlisting} + +Agda 上の HoareLogic で使われるプログラムは Comm 型の関数となる。 +プログラムの処理を Seq でつないでいき、最終的な状態にたどり着くと値を返して止まる。 +%% Code \ref{agda-hoare-simpl} は 変数 $i$、 $n$ に代入を行うプログラムである。 +%% これは Seq で PComm を2つ繋げた形になる。 + + Code \ref{agda-hoare-prog}は Code \ref{agda-while}で書いた While Loop を HoareLogic での Comm で記述したものである。 +ここでの $\$$は $()$の対応を合わせる Agda の糖衣構文で、行頭から行末までを $()$で囲っていることと同義である。 -\section{Agda での Hoare Logic} -人のコード解説になりそう +\begin{lstlisting}[caption= HoareLogic のプログラム ,label=agda-hoare-prog,mathescape=false] +program : Comm +program = + Seq ( PComm (λ env → record env {varn = 10})) + $ Seq ( PComm (λ env → record env {vari = 0})) + $ While (λ env → lt zero (varn env ) ) + (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) + $ PComm (λ env → record env {varn = ((varn env) - 1)} )) +\end{lstlisting} + +この Comm は Command をならべているだけである。 +この Comm を Agda 上で実行するため、 Code \ref{agda-hoare-interpret} のような interpreter を記述した。 + +\begin{lstlisting}[caption=Agda での HoareLogic interpreter ,label=agda-hoare-interpret] +{-# TERMINATING #-} +interpret : Env → Comm → Env +interpret env Skip = env +interpret env Abort = env +interpret env (PComm x) = x env +interpret env (Seq comm comm1) = interpret (interpret env comm) comm1 +interpret env (If x then else) with x env +... | true = interpret env then +... | false = interpret env else +interpret env (While x comm) with x env +... | true = interpret (interpret env comm) (While x comm) +... | false = env +\end{lstlisting} + + Code \ref{agda-hoare-interpret}は 初期状態の Env と 実行する Command の並びを受けとって、実行後の Env を返すものとなっている。 + +\begin{lstlisting}[caption=Agda での HoareLogic の実行 ,label=agda-hoare-run] +test : Env +test = interpret ( record { vari = 0 ; varn = 0 } ) program +\end{lstlisting} + + Code \ref{agda-hoare-run}のように interpret に $vari = 0 , varn = 0$ の record を渡し、 実行する Comm を渡して 評価してやると$record { varn = 0 ; vari = 10 }$ のような Env が返ってくる。 -\section{Hoare Logic の Soundness} -Soundness 周り +\section{Agda 上での Hoare Logic システムの検証} +ここでは先程例とした \ref{agda-while} の検証を例とする。 + + Code \ref{agda-hoare-rule} は Agda 上での HoareLogic での証明の構成である。 +HTProof では Condition と Command もう一つ Condition を受け取って、 Set を返す Agda のデータである。 +ここでの HTProof \cite{agda2-hoare} も Agda2 に移植されたものを使っている。 + +PrimRule は Code \ref{axiom-taut} の Axiom という関数を使い、事前条件が成り立っている時、 +実行後に事後条件が成り立つならば、 PComm で変数に値を代入できることを保証している。 + +SkipRule は Condition を受け取ってそのままの Condition を返すことを保証する。 + +AbortRule は PreContition を受け取って、Abort を実行して終わるルールである。 + +WeakeningRule は \ref{axiom-taut} の Tautology という関数を使って通常の逐次処理から、 +WhileRule のみに適応されるループ不変変数に移行する際のルールである。 + +SeqRule は3つの Condition と 2つの Command を受け取り、これらのプログラムの逐次的な実行を保証する。 + +IfRule は分岐に用いられ、3つの Condition と 2つの Command を受け取り、判定の Condition が成り立っているかいないかで実行する Command を変えるルールである。 +この時、どちらかの Command が実行されることを保証している。 + +WhileRule はループに用いられ、1つの Command と２つの Condition を受け取り、事前条件が成り立っている間、 Command を繰り返すことを保証している。 + +\lstinputlisting[caption=Axiom と Tautology,label=axiom-taut]{src/axiom-taut.agda.replaced} -\section{Hoare Logic での証明} -whileTestPrim.agda の解説 +\begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare-rule] +data HTProof : Cond -> Comm -> Cond -> Set where + PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} -> + (pr : Axiom bPre pcm bPost) -> + HTProof bPre (PComm pcm) bPost + SkipRule : (b : Cond) -> HTProof b Skip b + AbortRule : (bPre : Cond) -> (bPost : Cond) -> + HTProof bPre Abort bPost + WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} -> + {bPost' : Cond} -> {bPost : Cond} -> + Tautology bPre bPre' -> + HTProof bPre' cm bPost' -> + Tautology bPost' bPost -> + HTProof bPre cm bPost + SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} -> + {cm2 : Comm} -> {bPost : Cond} -> + HTProof bPre cm1 bMid -> + HTProof bMid cm2 bPost -> + HTProof bPre (Seq cm1 cm2) bPost + IfRule : {cmThen : Comm} -> {cmElse : Comm} -> + {bPre : Cond} -> {bPost : Cond} -> + {b : Cond} -> + HTProof (bPre /\ b) cmThen bPost -> + HTProof (bPre /\ neg b) cmElse bPost -> + HTProof bPre (If b cmThen cmElse) bPost + WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> + HTProof (bInv /\ b) cm bInv -> + HTProof bInv (While b cm) (bInv /\ neg b) +\end{lstlisting} + +Code \ref{agda-hoare-rule}を使って Code \ref{agda-while}の whileProgram の証明を構築する。 + +全体の証明は Code \ref{agda-hoare-while}の proof1 の様になる。 +proof1 では型で initCond、 Code \ref{agda-hoare-prog}のprogram、 termCond を記述しており、 +initCond から program を実行し termCond に行き着く HoareLogic の証明になる。 + +それぞれの Condition は Rule の後に記述されている {} に囲まれた部分で、 +initCondのみ無条件で true を返す Condition になっている。 + +それぞれの Rule の中にそこで証明する必要のある補題が lemma で埋められている。 +lemma1 から lemma5 の証明は幅を取ってしまうため、 詳細は当研究室レポジトリ \cite{cr-ryukyu} のプログラムを参照していただきたい。 + +これらの lemma は HTProof の Rule に沿って必要なものを記述されており、 +lemma1 では PreCondition と PostCondition が存在するときの代入の保証、 +lemma2 では While Loop に入る前の Condition からループ不変条件への変換の証明、 +lemma3 では While Loop 内での PComm の代入の証明、 +lemma4 では While Loop を抜けたときの Condition の整合性、 +lemma5 では While Loop を抜けた後のループ不変条件からCondition への変換と termCond への移行の整合性を保証している。 + +\begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while] +proof1 : HTProof initCond program termCond +proof1 = + SeqRule {λ e → true} ( PrimRule empty-case ) + $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 ) + $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 ( + WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10} + $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 +\end{lstlisting} + +proof1 は Code \ref{agda-hoare-prog}の program と似た形をとっている。 +HoareLogic では Comannd に対応する証明規則があるため、証明はプログラムに対応している。 +\section{Agda 上での Hoare Logic システムの健全性} +\ref{agda-hoare-while} では Agda での HoareLogic を用いた証明の構築を行った。 +システムの健全性は本来 Agda 側で保証する必要があるが、今回の例では Agda 上に Hoare Logic +を行えるシステムを構築したので健全性を担保する必要がある。 +hogefugapiyo
--- a/paper/reference.bib Thu Jan 02 21:25:52 2020 +0900 +++ b/paper/reference.bib Thu Jan 16 19:21:45 2020 +0900 @@ -1,20 +1,4 @@ -@inproceedings{queue, - author = {Michael, Maged M. and Scott, Michael L.}, title = {Simple, Fast, and Practical Non-blocking and Blocking Concurrent Queue Algorithms}, - booktitle = {Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing}, - series = {PODC '96}, - year = {1996}, - isbn = {0-89791-800-2}, - location = {Philadelphia, Pennsylvania, USA}, - pages = {267--275}, - numpages = {9}, - url = {http://doi.acm.org/10.1145/248052.248106}, - doi = {10.1145/248052.248106}, - acmid = {248106}, - publisher = {ACM}, - address = {New York, NY, USA}, - keywords = {compare_and_swap, concurrent queue, lock-free, multiprogramming, non-blocking}, -} - + @inproceedings{agda, author = {Norell, Ulf}, title = {Dependently Typed Programming in Agda}, @@ -33,75 +17,6 @@ keywords = {dependent types, programming}, } -@inproceedings{Chen:2015:UCH:2815400.2815402, - author = {Chen, Haogang and Ziegler, Daniel and Chajed, Tej and Chlipala, Adam and Kaashoek, M. Frans and Zeldovich, Nickolai}, - title = {Using Crash Hoare Logic for Certifying the FSCQ File System}, - booktitle = {Proceedings of the 25th Symposium on Operating Systems Principles}, - series = {SOSP '15}, - year = {2015}, - isbn = {978-1-4503-3834-9}, - location = {Monterey, California}, - pages = {18--37}, - numpages = {20}, - url = {http://doi.acm.org/10.1145/2815400.2815402}, - doi = {10.1145/2815400.2815402}, - acmid = {2815402}, - publisher = {ACM}, - address = {New York, NY, USA}, -} - -@inproceedings{Klein:2009:SFV:1629575.1629596, - author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon}, - title = {seL4: Formal Verification of an OS Kernel}, - booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles}, - series = {SOSP '09}, - year = {2009}, - isbn = {978-1-60558-752-3}, - location = {Big Sky, Montana, USA}, - pages = {207--220}, - numpages = {14}, - url = {http://doi.acm.org/10.1145/1629575.1629596}, - doi = {10.1145/1629575.1629596}, - acmid = {1629596}, - publisher = {ACM}, - address = {New York, NY, USA}, - keywords = {isabelle/hol, l4, microkernel, sel4}, -} - - -@inproceedings{Sigurbjarnarson:2016:PVF:3026877.3026879, - author = {Sigurbjarnarson, Helgi and Bornholt, James and Torlak, Emina and Wang, Xi}, - title = {Push-button Verification of File Systems via Crash Refinement}, - booktitle = {Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation}, - series = {OSDI'16}, - year = {2016}, - isbn = {978-1-931971-33-1}, - location = {Savannah, GA, USA}, - pages = {1--16}, - numpages = {16}, - url = {http://dl.acm.org/citation.cfm?id=3026877.3026879}, - acmid = {3026879}, - publisher = {USENIX Association}, - address = {Berkeley, CA, USA}, -} - -@inproceedings{Yang:2010:SLI:1806596.1806610, - author = {Yang, Jean and Hawblitzel, Chris}, - title = {Safe to the Last Instruction: Automated Verification of a Type-safe Operating System}, - booktitle = {Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation}, - series = {PLDI '10}, - year = {2010}, - isbn = {978-1-4503-0019-3}, - location = {Toronto, Ontario, Canada}, - pages = {99--110}, - numpages = {12}, - url = {http://doi.acm.org/10.1145/1806596.1806610}, - doi = {10.1145/1806596.1806610}, - acmid = {1806610}, - publisher = {ACM}, - address = {New York, NY, USA}, - keywords = {operating system, run-time system, type safety, verification}, -} @article{atton-ipsj, author="比嘉 健太 and 河野 真治", @@ -118,19 +33,6 @@ DOI="", } -@article{go, -author={J. Meyerson}, -journal={IEEE Software}, -title={The Go Programming Language}, -year={2014}, -volume={31}, -number={5}, -pages={104-104}, -keywords={Andrew Gerrand;C;Go;Google;arrays;build times;compilers;garbage collection;golang;imports;interfaces;open source;readability;scalability;slices;standard library;syntax}, -doi={10.1109/MS.2014.127}, -ISSN={0740-7459}, -month={Sept},} - @article{moggi-monad, author = {Moggi, Eugenio}, title = {Notions of Computation and Monads}, @@ -150,16 +52,6 @@ address = {Duluth, MN, USA}, } -@inproceedings{nobu-prosym, - author = "大城信康 and 河野真治", - title = "Continuation based C の GCC4.6 上の実装について", - booktitle = "第53回プログラミング・シンポジウム予稿集", - year = "2012", - volume = "2012", - pages = "69--78", - month = "jan" -} - @inproceedings{mitsuki-prosym, author = "宮城光希 and 河野真治", title = "Code Gear と Data Gear を持つ Gears OS の設計", @@ -171,63 +63,107 @@ } -@InProceedings{llvm, -author = {Chris Lattner and Vikram Adve}, -title = "{LLVM: A Compilation Framework for Lifelong Program Analysis \& Transformation}", -booktitle = "{Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO'04)}", -address = {Palo Alto, California}, -month = {Mar}, -year = {2004} +@techreport{ryokka-sigos, + author = "外間,政尊 and 河野,真治", + title = "GearsOSのAgdaによる記述と検証", + year = "2018", + institution = "琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科", + number = "5", + month = "may" +} + +@misc{agda, + title = {The Agda wiki}, + howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}}, + note = {Accessed: 2018/12/17(Mon)} +} + + +@misc{agda-documentation, + title = {Welcome to Agda’s documentation! — Agda latest documentation}, + howpublished = {\url{http://agda.readthedocs.io/en/latest/}}, + note = {Accessed: 2018/12/17(Mon)} } -@article{kaito-lola, - author = "Kaito, Tokumori and Shinji, Kono", - title = "Implementing Continuation based language in LLVM and Clang", - journal = "LOLA 2015, Kyoto", - month = "July", - year = 2015 +@book{Stump:2016:VFP:2841316, + author = {Stump, Aaron}, + title = {Verified Functional Programming in Agda}, + year = {2016}, + isbn = {978-1-97000-127-3}, + publisher = {Association for Computing Machinery and Morgan \&\#38; Claypool}, + address = {New York, NY, USA}, +} + +@misc{agda-alpa, + title = {Example - Hoare Logic}, + howpublished = {\url{http://ocvs.cfv.jp/Agda/readmehoare.html}}, + note = {Accessed: 2018/12/17(Mon)} } -@article{kkb-sigos, - author = "小久保翔平 and 伊波立樹 and 河野真治", - title = "Monad に基づくメタ計算を基本とする Gears OS の設計", - journal = "第133回情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)", - month = "May", - year = 2015 +@misc{agda2-hoare, + title = {Hoare Logic in Agda2}, + howpublished = {\url{https://github.com/IKEGAMIDaisuke/HoareLogic}}, + note = {Accessed: 2018/12/17(Mon)} +} + +@misc{coq, + title = {Welcome! | The Coq Proof Assistant}, + howpublished = {\url{https://coq.inria.fr/}}, + note = {Accessed: 2018/12/17(Mon)} } -@article{ikkun-sigos, - author = "東恩納琢偉 and 伊波立樹 and 河野真治", - title = "Gears OS における並列処理", - journal = "第140回 情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)", - month = "May", - year = 2017 +@misc{ats2, + title = {ATS-PL-SYS}, + howpublished = {\url{http://www.ats-lang.org/}}, + note = {Accessed: 2018/12/17(Mon)} } -@misc{openmp, - title = "OpenMP: Simple, portable, scalable SMP programming", - howpublished = {\url{http://www.openmp.org,}}, - note = {Accessed: 2018/02/05(Mon)} +@misc{rust, + title = {Rust programming language}, + howpublished = {\url{https://www.rust-lang.org/}}, + note = {Accessed: 2018/12/17(Mon)} } -@misc{cuda, - title = {CUDA Zone | NVIDIA Developer}, - howpublished = {\url{https://developer.nvidia.com/cuda-zone}}, - note = {Accessed: 2018/02/05(Mon)} -} + +@article{Klein:2010:SFV:1743546.1743574, + author = {Klein, Gerwin and Andronick, June and Elphinstone, Kevin and Heiser, Gernot and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon}, + title = {seL4: Formal Verification of an Operating-system Kernel}, + journal = {Commun. ACM}, + issue_date = {June 2010}, + volume = {53}, + number = {6}, + month = jun, + year = {2010}, + issn = {0001-0782}, + pages = {107--115}, + numpages = {9}, + url = {http://doi.acm.org/10.1145/1743546.1743574}, + doi = {10.1145/1743546.1743574}, + acmid = {1743574}, + publisher = {ACM}, + address = {New York, NY, USA}, +} -@mastersthesis{utah-master, - author = "徳森海斗", - title = "LLVM Clang 上の Continuation based C コンパイラ の改良", - school = "琉球大学 大学院理工学研究科 情報工学専攻", - year = "2016" -} +@inproceedings{Nelson:2017:HPV:3132747.3132748, + author = {Nelson, Luke and Sigurbjarnarson, Helgi and Zhang, Kaiyuan and Johnson, Dylan and Bornholt, James and Torlak, Emina and Wang, Xi}, + title = {Hyperkernel: Push-Button Verification of an OS Kernel}, + booktitle = {Proceedings of the 26th Symposium on Operating Systems Principles}, + series = {SOSP '17}, + year = {2017}, + isbn = {978-1-4503-5085-3}, + location = {Shanghai, China}, + pages = {252--269}, + numpages = {18}, + url = {http://doi.acm.org/10.1145/3132747.3132748}, + doi = {10.1145/3132747.3132748}, + acmid = {3132748}, + publisher = {ACM}, + address = {New York, NY, USA}, +} -@mastersthesis{kkb-master, - author = "小久保 翔平", - title = "Code Segment と Data Segment を持つ Gears OS の 設計", - school = "琉球大学 大学院理工学研究科 情報工学専攻", - year = "2016" -} - +@misc{cr-ryukyu, + title = {whileTestPrim.agda - 並列信頼研 mercurial repository}, + howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/file/tip/whileTestPrim.agda}}, + note = {Accessed: 2018/12/17(Mon)} +} \ No newline at end of file
--- a/ryokka-master.mm Thu Jan 02 21:25:52 2020 +0900 +++ b/ryokka-master.mm Thu Jan 16 19:21:45 2020 +0900 @@ -1,75 +1,91 @@ <map version="1.1.0"> <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> -<node CREATED="1577179229340" ID="ID_1981253136" MODIFIED="1577182620460" TEXT="GearsOS での HoareLogic を用いた実装と検証"> -<font NAME="SansSerif" SIZE="19"/> -<node CREATED="1577179287926" ID="ID_1165984884" MODIFIED="1577182620459" POSITION="right" TEXT="はじめに"> -<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179229340" ID="ID_1981253136" MODIFIED="1579169646928"> +<richcontent TYPE="NODE"><html> + <head> + + </head> + <body> + <p> + Continuation based C での + </p> + <p> + HoareLogic を用いた記述と検証 + </p> + </body> +</html></richcontent> +<font NAME="SansSerif" SIZE="14"/> +<node CREATED="1577179287926" ID="ID_1165984884" MODIFIED="1579169646928" POSITION="right" TEXT="はじめに"> +<font NAME="SansSerif" SIZE="14"/> </node> -<node CREATED="1577179299434" ID="ID_372153190" MODIFIED="1577182620459" POSITION="right" TEXT="Continuation based C"> -<font NAME="SansSerif" SIZE="19"/> -<node CREATED="1577179793073" ID="ID_1307352612" MODIFIED="1577182620458" TEXT="CodeGear"> -<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179299434" ID="ID_372153190" MODIFIED="1579169646928" POSITION="right" TEXT="Continuation based C"> +<font NAME="SansSerif" SIZE="14"/> +<node CREATED="1577179793073" ID="ID_1307352612" MODIFIED="1579169646928" TEXT="CodeGear"> +<font NAME="SansSerif" SIZE="14"/> </node> -<node CREATED="1577179805065" ID="ID_1214581036" MODIFIED="1577182620458" TEXT="DataGear"> -<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179805065" ID="ID_1214581036" MODIFIED="1579169646928" TEXT="DataGear"> +<font NAME="SansSerif" SIZE="14"/> </node> -<node CREATED="1577179939889" ID="ID_1188251116" MODIFIED="1577182620458" TEXT="Meta CodeGear,DataGear"> -<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179939889" ID="ID_1188251116" MODIFIED="1579169646928" TEXT="Meta CodeGear,DataGear"> +<font NAME="SansSerif" SIZE="14"/> </node> </node> -<node CREATED="1577179329845" ID="ID_1008088180" MODIFIED="1577182644207" POSITION="right" TEXT="Agda"> -<font NAME="SansSerif" SIZE="19"/> -<node CREATED="1577182682220" ID="ID_1522532015" MODIFIED="1577182690635" TEXT="入門"> -<font NAME="SansSerif" SIZE="18"/> +<node CREATED="1577179329845" ID="ID_1008088180" MODIFIED="1579169646927" POSITION="right" TEXT="Agda"> +<font NAME="SansSerif" SIZE="14"/> +<node CREATED="1577182682220" ID="ID_1522532015" MODIFIED="1579169646927" TEXT="入門"> +<font NAME="SansSerif" SIZE="14"/> </node> </node> -<node CREATED="1577179349458" ID="ID_739318439" MODIFIED="1577182637067" POSITION="right" TEXT="Hoare Logic"> -<font NAME="SansSerif" SIZE="19"/> -<node CREATED="1577179370109" ID="ID_809388614" MODIFIED="1577182664147" TEXT="whileTest (Hoare Logic の例)"> -<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179349458" ID="ID_739318439" MODIFIED="1579169646927" POSITION="right" TEXT="Hoare Logic"> +<font NAME="SansSerif" SIZE="14"/> +<node CREATED="1578999031670" ID="ID_517062300" MODIFIED="1579169646927" TEXT="入門"> +<font NAME="SansSerif" SIZE="14"/> +</node> +<node CREATED="1577179370109" ID="ID_809388614" MODIFIED="1579169646927" TEXT="whileTest (Hoare Logic の例)"> +<font NAME="SansSerif" SIZE="14"/> </node> -<node CREATED="1577179360283" ID="ID_501247037" MODIFIED="1577182670343" TEXT="Agda と Hoare Logic"> -<font NAME="SansSerif" SIZE="20"/> -<node CREATED="1577179441565" ID="ID_1388092541" MODIFIED="1577182620455" TEXT="記述"> -<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179360283" ID="ID_501247037" MODIFIED="1579169646927" TEXT="Agda と Hoare Logic"> +<font NAME="SansSerif" SIZE="14"/> +<node CREATED="1577179441565" ID="ID_1388092541" MODIFIED="1579169646927" TEXT="記述"> +<font NAME="SansSerif" SIZE="14"/> </node> -<node CREATED="1577179468054" ID="ID_545191696" MODIFIED="1577182620454" TEXT="Soundness 関連"> -<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179468054" ID="ID_545191696" MODIFIED="1579169646926" TEXT="Soundness 関連"> +<font NAME="SansSerif" SIZE="14"/> </node> </node> </node> -<node CREATED="1577179318540" ID="ID_402362033" MODIFIED="1577182658769" POSITION="right" TEXT="Continuation based C と Agda"> -<font NAME="SansSerif" SIZE="19"/> -<node CREATED="1577182741707" ID="ID_1751180005" MODIFIED="1577182751755" TEXT="HoareLogic"> -<font NAME="SansSerif" SIZE="16"/> +<node CREATED="1577179318540" ID="ID_402362033" MODIFIED="1579169646926" POSITION="right" TEXT="Continuation based C と HoareLogic"> +<font NAME="SansSerif" SIZE="14"/> +<node CREATED="1577182741707" ID="ID_1751180005" MODIFIED="1579169646926" TEXT="HoareLogic"> +<font NAME="SansSerif" SIZE="14"/> </node> </node> -<node CREATED="1577182694546" ID="ID_764943519" MODIFIED="1577182712199" POSITION="right" TEXT="BinaryTree と RedBlack Tree(Agda)"> -<font NAME="SansSerif" SIZE="15"/> -<node CREATED="1577182754406" ID="ID_1200857877" MODIFIED="1577182760901" TEXT="HoareLogic"> -<font NAME="SansSerif" SIZE="17"/> +<node CREATED="1577182694546" ID="ID_764943519" MODIFIED="1579169646926" POSITION="right" TEXT="BinaryTree と RedBlack Tree(Agda)"> +<font NAME="SansSerif" SIZE="14"/> +<node CREATED="1577182754406" ID="ID_1200857877" MODIFIED="1579169646926" TEXT="HoareLogic"> +<font NAME="SansSerif" SIZE="14"/> </node> -<node CREATED="1577182712718" ID="ID_283296995" MODIFIED="1577182732895" TEXT="BinaryTree の 条件つきのやつの話"> -<font NAME="SansSerif" SIZE="16"/> +<node CREATED="1577182712718" ID="ID_283296995" MODIFIED="1579169646926" TEXT="BinaryTree の 条件つきのやつの話"> +<font NAME="SansSerif" SIZE="14"/> </node> -<node CREATED="1577182765996" ID="ID_740598781" MODIFIED="1577182773370" TEXT="RedBlackTree"> -<font NAME="SansSerif" SIZE="16"/> +<node CREATED="1577182765996" ID="ID_740598781" MODIFIED="1579169646926" TEXT="RedBlackTree"> +<font NAME="SansSerif" SIZE="14"/> </node> </node> -<node CREATED="1577179295267" ID="ID_747054126" MODIFIED="1577182620450" POSITION="right" TEXT="まとめ"> -<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179295267" ID="ID_747054126" MODIFIED="1579169646925" POSITION="right" TEXT="まとめ"> +<font NAME="SansSerif" SIZE="14"/> </node> -<node CREATED="1577179315283" ID="ID_1375073128" MODIFIED="1577182620457" POSITION="left" TEXT="Gears OS"> -<font NAME="SansSerif" SIZE="19"/> -<node CREATED="1577179820187" ID="ID_519165935" MODIFIED="1577182654290" TEXT="-interface"> -<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179315283" ID="ID_1375073128" MODIFIED="1579169646925" POSITION="left" TEXT="Gears OS"> +<font NAME="SansSerif" SIZE="14"/> +<node CREATED="1577179820187" ID="ID_519165935" MODIFIED="1579169646925" TEXT="-interface"> +<font NAME="SansSerif" SIZE="14"/> </node> -<node CREATED="1577179862592" ID="ID_1991286966" MODIFIED="1577182620456" TEXT="Gears OS の検証"> -<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179862592" ID="ID_1991286966" MODIFIED="1579169646925" TEXT="Gears OS の検証"> +<font NAME="SansSerif" SIZE="14"/> </node> </node> -<node CREATED="1577179492520" ID="ID_1327764636" MODIFIED="1577182620454" POSITION="left" TEXT="できたらいいな(Binary-Tree)"> -<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179492520" ID="ID_1327764636" MODIFIED="1579169646912" POSITION="left" TEXT="できたらいいな(Binary-Tree)"> +<font NAME="SansSerif" SIZE="14"/> </node> </node> </map>