\begin{abstract}

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として
自分で記述するところに特徴がある。これにより健全性自体の証明が可能になった。

\end{abstract}
%% \chapter*{Abstract}

\begin{abstract_eng}


OS and application reliability are important.
To increase reliability, verifications of program with specifications are necessary.
Floyd-Hoare logic (hereafter Hoare Logic) is a wellknown program verification method.
Hoare Logic verifies the postonditions of a function are satisfied when the postconditions are satisfied.
It also checks the halt condition of the program.
Hoare Logic is a useful simple approach but often only applies to a limited set of commands and while programs.
It is not generaly suitable for complex ordinary programming languages.

Our laboratory is developping Continuation based C (CbC) as a reliable language.
In CbC, programs are described using units of CodeGear and DataGear.

CodeGear can be described in Agda as a function using the description of a light weight continuous passing.
Agda is a theorem proof system based Curry Howard correspondence, and it is also a functional programming language.
In Agda, conditions can be described as propositions,
The continuation can have preconditions and postconditions.

In existing languages, conditions are described in asserts, etc., but the proof cannot be done in that programming language.
Since Agda can describe the proof itself, that is, the inference among the propositions, as λ terms,
The proof of Hoare Logic itself can be described as Meta CodeGear. This was not possible with existing languages.
The point is that the program itself can be described with CodeGear of Agda base.
CodeGear has only input and output, and executes continuously in a goto manner without calling a function. This format is
naturally define Hoare Logic commands.

Hoare Logic's proof requires three conditions. One,
Pre-conditions and post-conditions are connected correctly throughout the program.
The preconditions and postconditions are equal in the loop (the connection of CodeGear including the loop) and constitute an invariant condition.
In addition, we need to show that the loop stops. For a program that does not stop, it is possible to define partial validity without stopping.

In this paper, we created and proved a simple while Loop program using the description of Hoare Logic on Agda.
This proof includes termination and the overall soundness of the proof. Previously, the soundness of Hoare Logic was limited to rather simple commands.
However, in this method, individual proofs are given as Meta CodeGears for complex CodeGears.

This made it possible to prove the soundness itself.

\end{abstract_eng}