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<n)の間、コマンドを繰り返し実行

実際に while program を表すために、コマンドでの構文木を記述している

```
        Seq
       /    \
  PComm      Seq
 (n=10)    /     \
         PComm   While
         (i=0)      |
                   Cond
                   (0<n)
                     |
                    Seq
                   /   \
               PComm    PComm
               (i++)     (n--) 
```
更にこの後、プログラムの仕様を記述して証明する

---

## CbC での Hoare Logic 概略
CodeGear は処理の単位、更にメタレベルの処理を Meta CodeGear という単位で分けてる

メタレベルの処理は今見えるところだと CodeGear 間を接続する処理とか

![](./hoare-cg-dg.svg)
![](/attachment/5e469a577b378d004670d3d6)

Meta CodeGear で信頼性の検証を行う



## 詳しい話、質問等はポスターで！
よろしくお願いします

ご静聴ありがとうございました


## CbC での Hoare Logic 記述
「代入」、「ループ」の２つの CodeGear に分けた

代入では「事前条件なし」 から 「n=10 かつ i=0」

ループでは少し条件を緩めて 「n + i = 10」

ループ終了後は 「i=0」が成り立ってるはず

というのを Gears 単位上で Hoare Logic っぽく検証しましたというお話になる予定

---