\chapter*{要旨}

OS やアプリケーションの信頼性は重要である。
信頼性を上げるにはプログラムが仕様を満たしていることを検証する必要がある。
プログラムの検証手法として、Floyd–Hoare logic (以下 Hoare Logic)が存在している。
HoareLogic は事前条件が成り立っているときにある
関数を実行して、それが停止する際に事後条件を満たすことを確認することで、検証を行う。
しかし、 HoareLogic はシンプルなアプローチであるが通常のプログラミング言語で使用することができず、
広まっているとはいえない。

当研究室では信頼性の高い OS として GearsOS を開発している。
現在 GearsOS ではCodeGear、DataGearという単位を用いてプログラムを記述する手法を用いており、
仕様の確認には定理証明系である Agda を用いている。

CodeGearは Agda 上では継続渡しの記述を用いた関数として
記述する。
また、継続にある関数を実行するための事前条件や
事後条件などをもたせることが可能である。

そのため Hoare Logic と CodeGear、DataGear という単位を用いたプログラミング手法
記述とは相性が良く、既存の言語とは異なり HoareLogic を使ったプログラミングが容易に行えると考えている。

本研究では Agda 上での HoareLogic の記述を使い、簡単な while Loop のプログラムの作成、証明を行った。
また、GearsOS の仕様確認のために CodeGear、DataGear という単位を用いた記述で Hoare Logic をベースと
した while Loop プログラムを記述、その証明を行なった。

\chapter*{Abstract}