title: 「Agda による継続を用いたプログラムの検証」
author: 外間 政尊
profile: @並列信頼研
lang: Japanese
code-engine: coderay


## プログラムの信頼性の保証
* 動作するプログラムの信頼性を保証したい
* プログラムの仕様を検証するには **モデル検査** と **定理証明** の２つの手法がある
  * モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認する
  * 定理証明　はプログラムの性質を論理式で記述しそれが常に正しいことを証明する
* また、当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している


## CodeGear と DataGear
* CodeGear とはプログラムを記述する際の処理の単位である。
* DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。
* CodeGear はメタ計算によって CodeGear へ接続される
* メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる
* Agda 上で CodeGear 、 DataGear という単位を定義した

<div style="text-align: center;">
    <img src="./fig/cgdg.svg" alt="goto" width="800">
</div>


## Agda とは
* 定理証明支援系の関数型言語
* 型を明示する必要がある
* また、インデントも意味を持つ
* 型に命題を入れ、関数部分に証明を記述する事ができる


## Agda の型、関数
* 例として singleLinkedStack の pop を使う
* Agda の 型は **関数名 : 型** で定義される
* Agda の 項、関数部分は **関数名 = 値**
* なにかを受け取って計算して次の関数に継続する型(**-> (fa -> t) -> t**)
* これはstackを受け取り、stackの先頭を取ってという処理を行い、次の関数に渡すという関数の型
* このような形で CodeGear を Agda で定義できる

```AGDA
popSingleLinkedStack : -> SingleLinkedStack a 
       -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
```

## Maybe
* **Maybe** はNothingかJustを返す型でAgda の dataとして定義されている
* ここでは Just か Nothing をパターンマッチで返す
* 要素にも型を書く必要がある

```AGDA
data Maybe a : Set where
  Nothing : Maybe a
  Just    : a -> Maybe a
```

## refl
* data は **data データ名 :** と書く
* 等しいという data として **refl** が定義されている

```AGDA
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x
```

## Agdaの関数
* 例として popSingleLinkedStack の関数を使う
* 関数での引数は **関数名 a b :** のように書く

```AGDA
popSingleLinkedStack :  -> SingleLinkedStack a -> 
   (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
popSingleLinkedStack stack cs with (top stack)
popSingleLinkedStack stack cs | Nothing = cs stack  Nothing
popSingleLinkedStack stack cs | Just d  = cs record  { top = (next d) } (Just (datum d))
```

## record
* record は複数のデータを纏めて記述する型で、他の言語のオブジェクトのように **レコード名.フィールド名** でアクセスできる
* SingleLinkedStack を例にとる
* **record レコード名** と書き、その次の行に **field** と書く
* その下の行に **フィールド名:型名** と列挙する
* SingleLinkedStack では top というフィールドに Maybe のかかっている Element 型の要素aが定義されている
* Element では record で data と次の要素 next を定義している

```AGDA
record SingleLinkedStack (a : Set) : Set where
  field
    top : Maybe (Element a)
```

## pushSingleLinkedStackの定義とrecordの構築
* pushSingleLinkedStack の型では stack と data を受け取り、 CodeGear 中で Data を stack に入れ、新しいstack を継続し、次の CodeGear に継続している
* 関数側では record の構築を行う
* **record** の後ろの {} 内部で **フィールド名 = 値** の形で列挙する
* 複数書くときは **;** で区切る

```Agda
pushSingleLinkedStack2 : {n m : Level } {t : Set m } {Data : Set n} ->
    SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
pushSingleLinkedStack2 stack datum next = 
    next record {top = Just (record {datum = datum;next =(top stack)})}
```

## Agda での Interface の定義
* stack の色々な実装を抽象的に表すために record を使い **StackMethods** をつくった
* 実装時は関数の中で record を構築している
* push、 pop は実装によらないAPI
* push、 pop に singlelinkedstack の実装が入る

```AGDA
record StackMethods {n m : Level } (a : Set n ) 
    {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
      field
        push : stackImpl -> a -> (stackImpl -> t) -> t
        pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
```

## Agda での Interface を含めた部分的な証明
* stackInSomeState で不定な Stack を作成し、そこに push し、直後に pop した値が push した値と等しいことを示している
* Agda 中では不明な部分を **?** と書くことができる
* **?** 部分には値が入る
* 証明部分はラムダ式で与える

```AGDA
stackInSomeState : {l m : Level } {D : Set l} {t : Set m } 
   (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
```

```AGDA
push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
push->push->pop2 {l} {D} x y s = ?
```

## ラムダ式
* ラムダ式は関数内で無名の関数を定義することができる
* **\s1 ->** はラムダ式で pushStack の次の CodeGear 部分にラムダ式を使いStackを継続している

```AGDA
push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
```


## Agda での Interface を含めた部分的な証明
*  証明部分に書いた ? はコンパイル後に **{ }0** に変わり、中に入る型が表示される
* x、y はMaybe なので Justで返ってくる
* push した x、 y と x1、 y1 が共に等しいことを証明したい
* そこで **∧** の部分をrecordで定義した

```AGDA
push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 ->
    pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
push->push->pop2 {l} {D} x y s = { }0
```

```AGDA
-- Goal
?0 : pushStack (stackInSomeState s) x
(λ s1 →
   pushStack s1 y
   (λ s2 → pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))
```

## Agda での Interface を含めた部分的な証明(∧)
* a と b の証明から aかつb を作るコンストラクタ
* 直積を表す型を定義する

```AGDA
record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
  field
    pi1 : a
    pi2 : b
```

## Agda での Interface を含めた部分的な証明
* ∧でまとめたpi1、pi2は **refl** で証明することができた

```AGDA
push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
    pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
```

## 今後の課題
* 本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。
* これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。
* また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。
* 今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。また RedBlackTree の挿入、削除の性質に関する証明も行おうと考えている。


## Hoare Logic
* Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証するための手法
* 前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) によって変更する
* この {P} C {Q} でプログラムを部分的に表すことができるp

<div style="text-align: center;">
    <img src="./fig/hoare.svg" alt="hoare" width="1000">
</div>


## Hoare Logic と CbC

* Hoare Logic の状態と処理を CodeGear、 DataGear の単位で考えることができると考えている

<div style="text-align: center;">
    <img src="./fig/hoare-cbc.svg" alt="cbc-hoare" width="800">
</div>


## Element
* Element の説明
```AGDA
record Element {l : Level} (a : Set l) : Set l where
  inductive
  constructor cons
  field
    datum : a  -- `data` is reserved by Agda.
    next : Maybe (Element a)
```