%% v3.2 [2019/03/19]
%\documentclass[Proof,technicalreport]{ieicej}
\documentclass[technicalreport]{ieicej}
%\usepackage{graphicx}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{textcomp}
\usepackage{latexsym}
%\usepackage[fleqn]{amsmath}
%\usepackage{amssymb}
\usepackage{listings}
\usepackage[dvipdfmx]{graphicx}
\usepackage{graphicx}
\usepackage{lmodern}
\usepackage{textcomp}
\usepackage{latexsym}
\usepackage{ascmac}
\usepackage[fleqn]{amsmath}
\usepackage{amssymb}
\usepackage[deluxe, multi]{otf}
\usepackage{url}
\usepackage{cite}




\lstset{
  frame=single,
  keepspaces=true,
  breaklines=true,
  xleftmargin=0zw,
  xrightmargin=0zw,
  framerule=.2pt,
  columns=[l]{fullflexible},
  language={},
  tabsize=4,
  lineskip=-0.5zw,
  inputencoding=utf8,
  extendedchars=true,
  stringstyle={\ttfamily},
  escapechar={@},
}

% basicstyle={\ttfamily},
\renewcommand{\lstlistingname}{Code}
\usepackage{caption}
\captionsetup[lstlisting]{font={small,tt}}


\def\IEICEJcls{\texttt{ieicej.cls}}
\def\IEICEJver{3.2}
\newcommand{\AmSLaTeX}{%
 $\mathcal A$\lower.4ex\hbox{$\!\mathcal M\!$}$\mathcal S$-\LaTeX}
%\newcommand{\PS}{{\scshape Post\-Script}}
\def\BibTeX{{\rmfamily B\kern-.05em{\scshape i\kern-.025em b}\kern-.08em
 T\kern-.1667em\lower.7ex\hbox{E}\kern-.125em X}}

\jtitle{継続を基本とする言語 CbC での Hoare Logic による健全性の考察}


\authorlist{
 \authorentry[masataka@cr.ie.u-ryukyu.ac.jp]{外間 政尊}{Masataka Hokama}{1}% 
 \authorentry[kono@cr.ie.u-ryukyu.ac.jp]{河野 真治}{Shinji Kono}{2}% 
}
\affiliate[1]{琉球大学大学院理工学研究科情報工学専攻}
  {Interdisciplinary Information Engineering, Graduate School of Engineering and Science, University of the Ryukyus.}
\affiliate[2]{琉球大学工学部情報工学科}
          {Information Engineering, University of the Ryukyus.}
          
%\MailAddress{$\dagger$hanako@denshi.ac.jp,
% $\dagger\dagger$\{taro,jiro\}@jouhou.co.jp}



\begin{document}
\begin{jabstract}
CbC は継続を主とする言語上で、HoareLogicをベースとし
た検証を提案している。
OSなどの手続き型の記述に対しても有効なものを目指
している。
Curry-Howard対応にもとづく証明支援系であるAgdaを用い
て検証手法の健全性を示す手法について考察する。
\end{jabstract}
\begin{jkeyword}
  プログラミング言語,
  CbC, Gears OS, Agda, 検証
\end{jkeyword}
%% \begin{eabstract}
%% IEICE (the Institute of Electronics, Information 
%% and Communication Engineers) provides 
%% a p\LaTeXe\ class file, named \IEICEJcls\ (ver.\,\IEICEJver), 
%% for the Technical Report of IEICE. 
%% This document describes how to use the class file, 
%% and also makes some remarks about typesetting a document by using p\LaTeXe. 
%% The design is based on ASCII Japanese p\LaTeXe. 
%% \end{eabstract}
%% \begin{ekeyword}
%% \LaTeXe\ class file, typesetting
%% \end{ekeyword}
\maketitle

\section{OSの検証}
OS やアプリケーションの信頼性は重要である。
信頼性を上げるにはプログラムが仕様を満たしていることを検証する必要がある。
プログラムの検証手法として、Floyd–Hoare Logic (以下 Hoare Logic)が知られている。
Hoare Logic は事前条件が成り立っているときにある関数を実行して、それが停止する際に事後条件を満たすことを確認することで、検証を行う。
Hoare Logic はシンプルなアプローチであるが限定されたコマンド群や while programにしか適用されないことが多く、
複雑な通常のプログラミング言語には向いていない。

当研究室では信頼性の高い言語として Continuation based C (CbC)を開発している。
CbC では CodeGear、DataGear という単位を用いてプログラムを記述する。

CodeGearを Agda で継続渡しの記述を用いた関数として記述する。ここで
Agda は Curry Howard 対応にもどつく定理証明系であり、それ自身が関数型プログラング言語でもある。
Agda では条件を命題として記述することができるので、
継続に事前条件や事後条件をもたせることができる。

既存の言語では条件は assert などで記述することになるが、その証明をそのプログラミング言語内で行うことはできない。
Agdaでは証明そのもの、つまり命題に対する推論をλ項として記述することができるので、
Hoare Logicの証明そのものを Meta CodeGearとして記述できる。これは既存の言語では不可能であった。
ポイントは、プログラムそのものを Agda baseのCodeGearで記述できることである。
CodeGearは入力と出力のみを持ち関数呼び出しせずにgoto的に継続実行する。この形式がそのまま
Hoare Logicのコマンドを自然に定義する。

Hoare Logicの証明には３つの条件が必要である。一つは
事前条件と事後条件がプログラム全体で正しく接続されていることである。
ループ(ループを含むCodeGearの接続)で、事前条件と事後条件が等しく、不変条件を構成していること。
さらに、ループが停止することを示す必要がある。停止しないプログラムに対しては停止性を省いた部分正当性を定義できる。

本論文では Agda 上での Hoare Logic の記述を使い、簡単な while Loop のプログラムの作成、証明を行った。
この証明は停止性と証明全体の健全性を含んでいる。従来はHoare Logicの健全性は制限されたコマンドなどに
対して一般的に示すのが普通であるが、本手法では複雑なCodeGearに対して、個別の証明をMeta CodeGearとして
自分で記述するところに特徴がある。これにより健全性自体の証明が可能になった。

\section{Continuation based C}
Continuation based C\cite{kaito-lola} (以下 CbC) は CodeGear を処理の単位、
DataGear をデータの単位として記述するプログラミング言語である。
CbC は C 言語とほぼ同じ構文を持つが、よりアセンブラに近い記述になる。

CbC では検証しやすいプログラムの単位として DataGear と CodeGear という
単位を用いるプログラミングスタイルを提案している。

DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータである。
CodeGear の入力となる DataGear を Input DataGear と呼び、
出力は Output DataGear と呼ぶ。

CodeGear はプログラムの処理そのもので、図 \ref{fig:cgdg}で示しているように任意の数の
Input DataGear を参照し、処理が完了すると任意の数の Output DataGear に書き込む。

CodeGear 間の移動は継続を用いて行われる。継続は関数呼び出しとは異なり、呼び出し
た後に元のコードに戻らず、次の CodeGear へ継続を行う。
これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。

\begin{figure}[htpb]
 \begin{center}
  \scalebox{0.3}{\includegraphics{fig/cgdg.pdf}}
 \end{center}
 \caption{CodeGear と DataGear}
 \label{fig:cgdg}
\end{figure}

また、プログラムの記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、資源管理等を記述しなければならない処理が存在する。
これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ。

メタ計算は OS の機能を通して処理することが多く、信頼性の高い記述が求められる。
そのため、 CbC ではメタ計算を分離するために Meta CodeGear、 Meta DataGear を定義している。

Meta CodeGear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。
図 \ref{fig:meta-cgdg} のように CodeGear を実行する前後や DataGear の大枠として Meta Gear が存在している。

\begin{figure}[htpb]
 \begin{center}
  \scalebox{0.3}{\includegraphics{fig/meta-cg-dg.pdf}}
 \end{center}
 \caption{メタ計算を可視化した CodeGear と DataGear}
 \label{fig:meta-cgdg}
\end{figure}


\section{関数型言語 としての Agda}
Agda \cite{agda} は純粋関数型言語である。
Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱う。

Agda の記述ではインデントが意味を持ち、スペースの有無もチェックされる。
コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される。
また、\verb/_/でそこに入りうるすべての値を示すことができ、
\verb/?/でそこに入る値や型を不明瞭なままにしておくことができる。

%% データについて
Agda では型をデータや関数に記述する必要がある。
Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する。
このとき \verb/name/ に 空白があってはいけない。
データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。
\verb/data/ キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くし、
値にコンストラクタとその型を列挙する。

Code \ref{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である。

\lstinputlisting[label=agda-nat, caption=自然数を表すデータ型 Nat の定義] {src/nat.agda.replaced}

\verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である。
\verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を表す再帰的なデータになっており、
\verb/suc/ を連ねることで自然数全体を表現することができる。

$\mathbb{N}$ 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。
\verb/Set/ は階層構造を持ち、型集合の集合の型を指定するには \verb/Set1/ と書く。
%% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる。

Agda には C 言語における構造体に相当するレコード型というデータも存在する、
例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する。Code \ref{agda-record}のようになる。
\lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/env.agda.replaced}
レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する。
複数の値を列挙するには \verb/;/ で区切る必要がある。

%% 関数について
Agda での関数は型の定義と、関数の定義をする必要がある。
関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ に記述するが、入力を受け取り出力返す型として記述される。$\rightarrow$ 、 または\verb/→/ を用いて \verb/input → output/ のように記述される。
また、\verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味し、中間記法で関数を定義することもできる。
関数の定義は型の定義より下の行に、\verb/=/ を使い \verb/name input = output/ のように記述される。

例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A → B/ のように書くことができる。
また、複数の引数を取る関数の型は \verb/A → A → B/ のように書ける。
例として任意の自然数$\mathbb{N}$を受け取り、\verb/+1/した値を返す関数はCode \ref{agda-function}のように定義できる。
\lstinputlisting[label=agda-function, caption=Agda における関数定義] {src/agda-func.agda.replaced}


引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
例として自然数$\mathbb{N}$の加算を関数で書くとCode \ref{agda-plus}のようになる。

\lstinputlisting[label=agda-plus, caption=自然数での加算の定義] {src/agda-plus.agda.replaced}
%% \lstinputlisting[label=agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced}

パターンマッチでは全てのコンストラクタのパターンを含む必要がある。
例えば、自然数$\mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある。
なお、コンストラクタをいくつか指定した後に変数で受けることもでき、その変数では指定されたもの以外を受けることができる。
例えばCode \ref{agda-pattern}の減算では初めのパターンで2つ目の引数が\verb/zero/のすべてのパターンが入る。


\lstinputlisting[label=agda-pattern, caption=自然数の減算によるパターンマッチの例] {src/agda-pattern.agda.replaced}

Agda には$\lambda$計算が存在している。$\lambda$計算とは関数内で生成できる無名の関数であり、
\verb/\arg1 arg2 → function/ または $\lambda$\verb/arg1 arg2 → function/ のように書くことができる。
Code \ref{agda-function} で例とした \verb/+1/ をラムダ計算で書くとCode \ref{agda-lambda}の\verb/$\lambda$+1/ように書くことができる。この二つの関数は同一の動作をする。

\lstinputlisting[label=agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda.replaced}

Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。
スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。
例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリストCode \ref{agda-where} のように書ける。
これは \verb/f'/ と同様の動作をする。
\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。

\lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced}

また Agda では停止性の検出機能が存在し、プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る。
\verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない。
Code \ref{term} で書かれた、\verb/loop/ と \verb/stop/ は任意の自然数を受け取り、0になるまでループして0を返す関数である。
\verb/loop/ では $\mathbb{N}$ の数を受け取り、 \verb/loop/ 自身を呼び出しながら 数を減らす関数 pred を呼んでいる。しかし、\verb/loop/の記述では関数が停止すると言えないため、定義するには\verb/{-# TERMINATING #-}/のタグが必要である。
\verb/stop/ では自然数がパターンマッチで分けられ、\verb/zero/のときは \verb/zero/を返し、 \verb/suc n/ のときは \verb/suc/ を外した \verb/n/ で stop を実行するため停止する。

\lstinputlisting[label=term, caption=停止しない関数 loop、停止する関数 stop] {src/termination.agda.replaced}

このように再帰的な定義の関数が停止するときは、何らかの値が減少する必要がある。


\section{定理証明支援器としての Agda}
Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。
証明の例として Code Code \ref{proof} を見る。
ここでの \verb/+zero/ は右から \verb/zero/ を足しても ≡ の両辺は等しいことを証明している。
これは、引数として受けている \verb/y/ が \verb/Nat/ なので、 \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある。
\lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced}
\verb/y = zero/ の時は $zero \equiv zero$ とできて、左右の項が等しいということを表す \verb/refl/ で証明することができる。
\verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという
Code \ref{cong}の \verb/cong/ を使って、y の値を 1 減らしたのち、再帰的に \verb/+zero y/
を用いて証明している。
\lstinputlisting[caption=cong,label=cong]{src/cong.agda.replaced}

%% \begin{lstlisting}[caption=等式変形の例,label=proof]
%% +zero : { y : ℕ } → y + zero  ≡ y
%% +zero {zero} = refl
%% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
%%
%% -- cong : ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y
%% -- cong f refl = refl
%% \end{lstlisting}

また、他にも $\lambda$ 項部分で等式を変形する構文がいくつか存在している。
ここでは \verb/rewrite/ と ≡\verb/-Reasoning/ の構文を説明するとともに、等式を変形する構文の例として加算の交換則について示す。

\verb/rewrite/ では 関数の \verb/=/ 前に \verb/rewrite 変形規則/ の形で記述し、複数の規則を使う場合は \verb/rewrite/ 変形規則1 \verb/|/ 変形規則2 のように \verb/|/を用いて記述する。
Code \ref{agda-rewrite} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である。
ここでは、\verb/+zero/ を利用し、 \verb/zero + y/ を \verb/y/ に変形することで $y \equiv y$となり、左右の項が等しいことを示す \verb/refl/ になっている。

\lstinputlisting[caption=等式変形の例3/3,label=agda-term-post]{src/agda-term3.agda.replaced}
Code \ref{agda-term-post} では \verb/suc (y + x)/ $equiv$ \verb/y + (suc x)/ という等式に対して $equiv$ の対称律 \verb/sym/ を使って左右の項を反転させ\verb/y + (suc x)/ $equiv$ \verb/suc (y + x)/の形にし、\verb/y + (suc x)/が\verb/suc (y + x)/ に変形できることを \verb/+-suc/ を用いて示した。
これにより等式の左右の項が等しくなったため \verb/+-comm/ が示せた。

Agda ではこのような形で等式を変形しながら証明を行う事ができる。



\section{Hoare Logic}
Floyd-Hoare Logic \cite{10.1145/363235.363259}(以下 Hoare Logic) とは
C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。

Hoare Logic では事前条件が成り立つとき、何らかの計算(以下コマンド)を実行した後に
事後条件が成り立つことを検証する。
事前条件を P 、 何らかの計算を C 、 事後条件を Q としたとき、
\[\{P\}\ C \ \{Q\}\]
といった形で表される。
この三組は Hoare Triple と呼ばれる。

Code \ref{c-while} は while program の例である。
これは変数 \verb/n/ と \verb/i/ を持ち、\verb/n/が 0　より大きいとき、\verb/i/を増やし \verb/n/を減らす、
疑似プログラムである。

\begin{lstlisting}[label=c-while,captionpos=b]
n = 10;
i = 0;

while (n > 0) {
  i++;
  n--;
}
\end{lstlisting}



このプログラムでの状態は、初めの $n = 10$、 $i = 0$ を代入する条件、
while loop 中に成り立っている条件を $n + i = 10$、
while loop が終了したとき成り立っている条件を $i = 10$
としている。

CbC 上での Hoare Logic で同様のプログラムを作成し、検証を行う。

\section{DataGear、 CodeGear と Agdaの対応}
現在 CbC では検証用の上位言語として Agda を利用しており、
Agda では CbC のプログラムをメタ計算を含む形で記述することができる。


Agda での DataGear は Agda で使うことのできるすべてのデータに対応する。
また、Agda での記述はメタ計算として扱われる。


CodeGear は DataGear を受け取って処理を行い DataGear を返す。
また、CodeGear 間の移動は継続を用いて行われる。
継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻らず、
次の CodeGear へ継続を行うものであった。

これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当し、
継続渡し(Continuation Passing Style) で書かれた Agda の関数と対応する。
継続は不定の型 (\verb/t/) を返す関数で表される。
継続先は次に実行する関数の型を引数として受け取り不定の型\verb/t/を返す関数として記述され、
CodeGear 自体も同じ型 \verb/t/ を返す関数となる。

Code \ref{agda-cg} は Agda で記述した加算を行う CodeGear の例である。

\lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda.replaced}

\verb/plus 10 20/ を評価すると \verb/next/ に 30 が入力されていることがわかる。

\section{CbC での Hoare Logic の記述}
Hoare Logic の事前条件や事後条件は変数の大小関係や同値関係などで表される。
Agda 上では関係もデータとして扱うことができるため、関係を引数とした CodeGear を用いてプログラムを記述する。

\begin{figure}[htpb]
 \begin{center}
  \scalebox{0.1}{\includegraphics{fig/hoare_cg_dg.pdf}}
 \end{center}
 \caption{CodeGear、DataGear での Hoare Logic}
 \label{fig:hoare-cgdg}
\end{figure}


CbC での Hoare Logic は fig \ref{fig:hoare-cgdg} が示すように、
事前条件(Pre Condition) が Proof で成立しており、 CodeGear で変更し、事後条件(Post Condition)が成り立つことを Proof で検証している。


\ref{cbc-hoare-write} は通常の CodeGear と Hoare Logic ベースの CodeGear を例としている。
通常の CodeGear である \verb/whileLoop'/ と Hoare Logic ベースの CodeGear である \verb/whileLoopPwP'/ は同じ動作をする。

\lstinputlisting[label=cbc-hoare-write, caption=CbC 上での Hoare Logic, escapechar=@] {src/agda-hoare-write.agda.replaced}

\verb/whileLoopPwP'/ では引数として事前条件 pre と継続先の関数を受け取っており、継続先の関数が受け取る引数 post や fin などの条件がこの関数においての事後条件となる。

\section{CbC 上での Hoare Logic を用いた仕様記述と停止性}
Hoare Logic では用意されたシンプルなコマンドを用いてプログラムを記述したが、
CbC 上では CodeGear という単位でプログラムを記述する。
そのため Hoare Logic のコマンドと同様に CodeGear を使った仕様記述を行う必要がある。

while program には初めの $n = 10$、 $i = 0$ を代入する条件、
while loop 中に成り立っている条件を $n + i = 10$、
while loop が終了したとき成り立っている条件を $i = 10$
の3つの状態があった。

Code \ref{cbc-condition} は while program の3つの状態を記述したものである。
\lstinputlisting[label=cbc-condition, caption= CbC ベースの Hoare Logic] {src/cbc-condition.agda.replaced}

\verb/whileTestStateP/ では \verb/s1/ が初期状態、 \verb/s2/ がループ内不変条件、　\verb/fs/ が最終状態に対応している。
\verb/s1/、 \verb/s2/、 \verb/s3/ は それぞれ \verb/whileTestState/ で定義された識別子である。

これらの状態を使って、CbC 上の Hoare Logic を使って while program を作成していく。

Code \ref{cbc-hoare-prim} は代入部分の Meta CodeGear である。
代入では事前条件がなく、事後条件として \verb/s1/ の \verb/(vari env ≡ 0) ∧ (varn env ≡ c10 env)/ が成り立つ。
\lstinputlisting[label=cbc-hoare-prim, caption=CbC 上の Hoare Logic での 代入] {src/cbc-hoare-prim.agda.replaced}

Code \ref{cbc-hoare-loop} はループを行うコードである。
\verb/whileLoopP'/はループを続ける、終えるの判断を行う Meta CodeGear で、ループを続けている間、 \verb/varn/ の値を減らし、 \verb/vari/ の値を増やしている。
ループは \verb/varn/ が \verb/suc n/の間続き、その間の条件である\verb/s2/、つまり  \verb/(varn env + vari env ≡ c10 env)/ の状態が成り立つ。 \verb/varn/ が \verb/zero/ になると最後の \verb/loopPwP'/ に \verb/fs/ である \verb/(vari env ≡ c10 env)/を渡し、ループを終える。

\verb/loopPwP'/ は実際にループをする Meta CodeGear で、回って来た際に \verb/varn/ が \verb/suc n/の間は \verb/whileLoopPwP'/ を実行し、その継続先の Meta CodeGear に自身である \verb/loopPwP'/を入れてループを行う。
\verb/varn/ \verb/zero/のケースはその前の \verb/whileLoopPwP'/が \verb/zero/ で \verb/sf/ の最終状態を返してくるため、 \verb/loopPwP'/ でも同様に \verb/sf/ である \verb/(vari env ≡ c10 env)/ を返し、ループが終了する。

\lstinputlisting[label=cbc-hoare-loop, caption=CbC 上の Hoare Logic での while loop] {src/cbc-hoare-loop.agda.replaced}

これらの Meta CodeGear を使い仕様を記述する。
\lstinputlisting[label=cbc-hoare-while, caption=CbC 上の Hoare Logic] {src/cbc-hoare-while.agda.replaced}

\verb/whileTestPCallwP'/ はCode \ref{cbc-hoare-prim}やCode \ref{cbc-hoare-loop}で解説した Meta CodeGear を組み合わせた仕様である。

また、while program と同様にループ内ではそのままの条件だとループさせることが難しいため \verb/conv/ を使ってループ内不変条件へと変化させている。

この仕様では \verb/whileTestPwP/ と \verb/loopPwP'/ を続けて実行したとき、最後のラムダ式に入っている最終状態 \verb/vari env ≡ c10 env/ が必ず成り立つ。

\verb/loopHelper/ では \verb/loopPwP'/ が必ず停止し、
\verb/vari env ≡ c10 env/ が成り立つことが分かる。

\lstinputlisting[label=loophelper, caption=loopHelper を使った停止性] {src/cbc-hoare-SoundnessC.agda.replaced}


\section{CbC 上での Hoare Logic を用いた Soundness の証明}
ここでは CbC 上の Hoare Logic でのSoundness(健全性) について確認する。

Code \ref{implies} は A ならば B の命題により証明を行う implies である。
implies は Set である A と B を受け取る。このとき A → B が存在すれば A implies B を証明することができる。

\lstinputlisting[label=implies, caption=implies] {src/sound-impl.agda.replaced}

代入を行う CodeGear である whileTestP は初期状態を持たないため、
常に真の命題 $\top$ と代入を終えたときの事後条件である (vari env ≡ 0) ∧ (varn env ≡ c10 env) を implies に入れた型を記述する。
Code\ref{impl-pcom} は実際に implies を用いて記述した証明である。
証明では proof に( $\top$ → (vari env ≡ 0) ∧ (varn env ≡ c10 env) )であると記述できればよく、

ここでは λ \_ → record { pi1 = refl ; pi2 = refl } がこれに対応する。

\lstinputlisting[label=impl-pcom, caption=代入の implies による証明] {src/sound-pcom.agda.replaced}

Code\ref{impl-psemcom} の whileTestPSemSound は output ≡ whileTestP c (λ e → e) を受け取ることで whileTestP の実行が終わった結果、つまり停止した CodeGear の実行結果が事後条件を満たしていることを証明している

\lstinputlisting[label=impl-psemcom, caption=停止性を考慮した代入の健全性の証明] {src/sound-psemcom.agda.replaced}

同様に他の CodeGear に対しても健全性の証明が可能である。
Code \ref{sound-conv} の whileConvPSemSound は制約を緩める conversion の健全性の証明である。
\lstinputlisting[label=sound-conv, caption=conversionの implies による証明] {src/sound-conv.agda.replaced}
conversion でも同様に元のプログラムに対して証明を行えている。

Code \ref{sound-loop} は while loop でのループをする CodeGear である。
ここでは loopPPSemInduct という補助定理を使って証明を記述しているが、この証明は長くなったため、元のソースコード\cite{loop-proof}を参照していただきたい。
\lstinputlisting[label=sound-loop, caption= loop の implies による証明] {src/sound-loop.agda.replaced}


\ref{sound-looppsem} はループの判断をする CodeGear で loopPPSem を使って証明を行っている。
\lstinputlisting[label=sound-looppsem, caption= loop の implies による停止性を含めた証明] {src/sound-looppsem.agda.replaced}

ここでも同様に元のプログラムに対して証明を行うことができた。

CbC 上での Hoare Logic では implies を用いて健全性に対する証明が行えると考えている。


\section{まとめと今後の課題}
本論文では Continuation based C プログラムに対して
Hoare Logic をベースにした仕様記述と検証を行った。
また、CbC での Hoare Logic では仕様を含めた記述のまま、
実際にコードが実行できることを確認した。

実際に、 Hoare Logic ベースの記述を行うことで、
検証のメタ計算に使われる Meta DataGear や、
CodeGear の概念が明確となった。
また、 CbC 上での Pre Condition、
Post Conditionの記述方法が明確になった。

元の Hoare Logic ではコマンドのみでのプログラム記述と検証を行っていたが、
CodeGear をベースにすることでより柔軟な単位でのプログラム記述し、
実際に検証を行えることが分かった。

以前は検証時に無限ループでなくてもループが存在すると、 Agda が導出時に step での実行を行うため、
ループ回数分 step を実行する必要があったが、ループに対する簡約を記述することで、
有限回のループを抜けて証明が記述できることが判明した。
今後、ループ構造に対する証明は同様に解決できると考えられるため、
より多くの証明が可能となると期待している。

今後の課題として、他のループが発生するプログラムの検証が挙げられる。
同様に検証が行えるのであれば、共通で使えるライブラリのような形でまとめることで、
より容易な検証ができるようになるのではないかと考えている。
現在、検証が行われていないループが存在するプログラムとして、
Binary Tree や RedBlack Tree などのデータ構造が存在するため、
それらのループに対して今回の手法を適用して検証を行いたい。

また、Meta DataGear で DataGear の関係等の制約条件を扱うことで、
常に制約を満たすデータを作成することができる。
予めそのようなデータをプログラムを使用することで、検証を行う際の記述減らすことができると考えている。
これも同様に Binary Tree や RedBlack Tree などのデータ構造に適用し、
検証の一助になると考えている。

その他の課題としては、
CbC で開発されている GearsOS に存在する並列構文の検証や、
検証を行った Agda 上の CbC 記述から
ノーマルレベルの CbC プログラムの生成などが挙げられる。


\nocite{*}
\bibliography{tecrep}{}
\bibliographystyle{plain}
\end{document}