Continuation Based C の Hoare Logic を用いた仕様記述と検証 ===== 琉球大学大学院 : 並列信頼研究室\ 外間 政尊 --- ## OS の検証技術としての Hoare Logic の問題点 - OS やアプリケーションの信頼性は重要な課題 - 信頼性を上げるために仕様の検証が必要 - 検証にはモデル検査や**定理証明**などが存在する - 定理証明では証明の手法と型システムの対応を用いて検証 - また、仕様検証の手法として **Hoare Logic** がある - Hoare Logic ではコマンドを実行する上で事前の条件があり、実行が停止したとき成立する条件がある - コマンドが細かいため大きなプログラムを記述するのが大変 --- ## Hoare Logic　をベースにした Gears 単位での検証 - 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案している - CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む - CodeGear は継続を用いて次の CodeGear に接続される - **定理証明支援機**である **Agda** 上で CodeGear DataGear の単位を用いた検証を行う - 本研究では Gears 単位を用いた Hoare Logic ベースの検証手法を提案する --- ## Hoare Logic Hoare Logic はプログラム検証の手法 事前条件( P )が成り立つとき、コマンド( C )を実行すると事後条件( Q )が成り立つ これは **{ P } C { Q }** の形で表され、Hoare Triple と呼ばれる 以下のような while program を検証した n = 10 となっているが検証では n は任意の自然数 ```C n = 10; i = 0; while (n>0) { i++; n--; } ``` --- ## Hoare Logic と while program **Seq** はコマンドを2つ受け取って順に実行する **PComm** は代入 **while** は変数の状態が(0