プログラムの信頼性の保証
+-
+
- 今回は 定理証明 をつかって仕様を検証する +
- 定理証明には定理証明支援系の言語 Agda を使用する
+
-
+
- Agda では型でプログラムの性質を論理式で記述し、型に対応する関数部分で論理式を解くことで証明を記述できる + +
+ - 今回は Agda を用いて CodeGear 、DataGear、Interfaceを定義した +
- この単位を用いて実装された Stack に Interface を実装し、性質の一部を証明した
CodeGear と DataGear
-
-
- CodeGear とはプログラムを記述する際の処理の単位である。 -
- DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。 +
- CodeGear とはプログラムを記述する際の処理の単位である +
- DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている
- CodeGear はメタ計算によって CodeGear へ接続される
- メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる -
- Agda 上で CodeGear 、 DataGear という単位を定義した
@@ -124,25 +142,14 @@
-
+
+
-
ラムダ式
+ラムダ式
- ラムダ式は関数内で無名の関数を定義することができる -
- \s1 -> はラムダ式で pushStack の次の CodeGear 部分にラムダ式を使いStackを継続している +
- \s1 -> はラムダ式で push->push->pop2 の型では次の CodeGear 部分にラムダ式を使いStackを渡している
push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
@@ -296,17 +329,23 @@
-今後の課題
+まとめと今後の課題
- - 本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。
- - これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。
- - また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。
- - 今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。また RedBlackTree の挿入、削除の性質に関する証明も行おうと考えている。
+ - 本研究では CodeGear、DataGear を Agda に定義できた
+ - また Agda で Interface の記述及び Interface を含めた一部の証明を行えた
+ - これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた
+
+ - 今後の課題としては 継続を用いた Agda で Hoare Logic を表現し、その Hoare Logic をベースとして証明を行えるかを確認する
+ - また RedBlackTree の挿入、削除の性質に関する証明も行おうと考えている
diff -r 22f582c4908d -r 989de96fe049 slide/slide.md
--- a/slide/slide.md Thu Feb 22 00:23:06 2018 +0900
+++ b/slide/slide.md Thu Feb 22 03:18:45 2018 +0900
@@ -1,4 +1,4 @@
-title: 「Agda による継続を用いたプログラムの検証」
+title: Agda による継続を用いたプログラムの検証
author: 外間 政尊
profile: @並列信頼研
lang: Japanese
@@ -7,37 +7,40 @@
## プログラムの信頼性の保証
* 動作するプログラムの信頼性を保証したい
-* プログラムの仕様を検証するには **モデル検査** と **定理証明** の２つの手法がある
+
+* 信頼性の保証をするためにはプログラムの仕様を検証する必要がある
+* プログラムの仕様を検証するにはモデル検査と **定理証明** の２つの手法がある
* モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認する
- * 定理証明 はプログラムの性質を論理式で記述しそれが常に正しいことを証明する
-* また、当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している
+ * 定理証明 はプログラムの性質を論理式で記述しそれが常に正しいことを証明する
+* また、当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している
+
+## プログラムの信頼性の保証
+* 今回は **定理証明** をつかって仕様を検証する
+* 定理証明には定理証明支援系の言語 Agda を使用する
+ * Agda では型でプログラムの性質を論理式で記述し、型に対応する関数部分で論理式を解くことで証明を記述できる
+
+* 今回は Agda を用いて CodeGear 、DataGear、Interfaceを定義した
+* この単位を用いて実装された Stack に Interface を実装し、性質の一部を証明した
## CodeGear と DataGear
-* CodeGear とはプログラムを記述する際の処理の単位である。
-* DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。
+* CodeGear とはプログラムを記述する際の処理の単位である
+* DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている
* CodeGear はメタ計算によって CodeGear へ接続される
* メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる
-* Agda 上で CodeGear 、 DataGear という単位を定義した
-## Agda とは
-* 定理証明支援系の関数型言語
-* 型を明示する必要がある
-* また、インデントも意味を持つ
-* 型に命題を入れ、関数部分に証明を記述する事ができる
-
-
-## Agda の型、関数
-* 例として singleLinkedStack の pop を使う
+## Agda の型
+* 例として popSingleLinkedStack を使う
+* singleLinkedStack は Stack の実装部分で push、 pop の
* Agda の 型は **関数名 : 型** で定義される
* Agda の 項、関数部分は **関数名 = 値**
* なにかを受け取って計算して次の関数に継続する型(**-> (fa -> t) -> t**)
-* これはstackを受け取り、stackの先頭を取ってという処理を行い、次の関数に渡すという関数の型
+
* このような形で CodeGear を Agda で定義できる
```AGDA
@@ -46,7 +49,7 @@
```
## Maybe
-* **Maybe** はNothingかJustを返す型でAgda の dataとして定義されている
+* **Maybe** はNothingかJustを返す型でAgda の **data** として定義されている
* ここでは Just か Nothing をパターンマッチで返す
* 要素にも型を書く必要がある
@@ -56,9 +59,11 @@
Just : a -> Maybe a
```
-## refl
-* data は **data データ名 :** と書く
-* 等しいという data として **refl** が定義されている
+## Agda でのデータの定義
+* Agda でのデータの定義の例として **refl** 定義を使用する
+* data は **data データ名 : 型** と書く
+* **refl** は左右の項が等しいことを表している
+
```AGDA
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
@@ -66,8 +71,9 @@
```
## Agdaの関数
-* 例として popSingleLinkedStack の関数を使う
-* 関数での引数は **関数名 a b :** のように書く
+* 例として popSingleLinkedStack を使う
+* Agdaでの関数の定義は **関数名 = 関数の実装** の書く
+
```AGDA
popSingleLinkedStack : -> SingleLinkedStack a ->
@@ -78,13 +84,14 @@
```
## record
-* record は複数のデータを纏めて記述する型で、他の言語のオブジェクトのように **レコード名.フィールド名** でアクセスできる
-* SingleLinkedStack を例にとる
+* record は複数のデータを纏めて記述する型
* **record レコード名** と書き、その次の行に **field** と書く
* その下の行に **フィールド名:型名** と列挙する
* SingleLinkedStack では top というフィールドに Maybe のかかっている Element 型の要素aが定義されている
* Element では record で data と次の要素 next を定義している
+
+
```AGDA
record SingleLinkedStack (a : Set) : Set where
field
@@ -98,16 +105,17 @@
* 複数書くときは **;** で区切る
```Agda
-pushSingleLinkedStack2 : {n m : Level } {t : Set m } {Data : Set n} ->
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} ->
SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
-pushSingleLinkedStack2 stack datum next =
+pushSingleLinkedStack stack datum next =
next record {top = Just (record {datum = datum;next =(top stack)})}
```
## Agda での Interface の定義
-* stack の色々な実装を抽象的に表すために record を使い **StackMethods** をつくった
+* singleLinkedStack の色々な実装を抽象的に表すために record を使い **StackMethods** をつくった
* 実装時は関数の中で record を構築している
* push、 pop は実装によらないAPI
+
* push、 pop に singlelinkedstack の実装が入る
```AGDA
@@ -118,11 +126,16 @@
pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t
```
-## Agda での Interface を含めた部分的な証明
-* stackInSomeState で不定な Stack を作成し、そこに push し、直後に pop した値が push した値と等しいことを示している
-* Agda 中では不明な部分を **?** と書くことができる
-* **?** 部分には値が入る
-* 証明部分はラムダ式で与える
+
+## 証明の概要
+* 今回は singleLinkedStack の実装を抽象的に表す Interface を通し、 **任意の数** を push し pop したとき、
+push した値と pop した値が等しくなることを証明する
+* このとき、どのような状態の Stack に push し、 pop をしても値が等しくなることを示したい
+* そのため、**状態の不定な** Stack を作成する関数を作成した
+
+## 不定な Stack の定義
+* 不定な Stack を作成する stackInSomeState という関数を作成した
+* stackInSomeState は stack を受け取り、状態の決まっていない stack を record を作成する
```AGDA
stackInSomeState : {l m : Level } {D : Set l} {t : Set m }
@@ -130,16 +143,22 @@
stackInSomeState s = record { stack = s ; stackMethods = singleLinkedStackSpec }
```
+## Agda での Interface を含めた部分的な証明
+* push を２回行い、直後に pop を2回した値が push した値がpopした後の値と等しいことを示している
+* Agda 中では不明な部分を **?** と書くことができ、**?**部分には証明が入る
+* 証明部分はラムダ式で与える
+* 型部分に注目する
+
```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 ) ) ))
+ pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
push->push->pop2 {l} {D} x y s = ?
```
## ラムダ式
* ラムダ式は関数内で無名の関数を定義することができる
-* **\s1 ->** はラムダ式で pushStack の次の CodeGear 部分にラムダ式を使いStackを継続している
+* **\s1 ->** はラムダ式で push->push->pop2 の型では次の CodeGear 部分にラムダ式を使いStackを渡している
```AGDA
push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
@@ -149,15 +168,16 @@
## Agda での Interface を含めた部分的な証明
-* 証明部分に書いた ? はコンパイル後に **{ }0** に変わり、中に入る型が表示される
-* x、y はMaybe なので Justで返ってくる
-* push した x、 y と x1、 y1 が共に等しいことを証明したい
-* そこで **∧** の部分をrecordで定義した
+
+* ? 部分はコンパイル時に Agda から内部に入る型を示してもらえる
+
+* ここでは最終的に **(Just x ≡ x1) ∧ (Just y ≡ y1)** が返ってくる事がわかる
+
+* (Just x ≡ x1)と(Just y ≡ 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
```
@@ -170,7 +190,7 @@
```
## Agda での Interface を含めた部分的な証明(∧)
-* a と b の証明から aかつb を作るコンストラクタ
+* a と b の証明から a かつ b を作るために
* 直積を表す型を定義する
```AGDA
@@ -189,11 +209,13 @@
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 の挿入、削除の性質に関する証明も行おうと考えている。
+## まとめと今後の課題
+* 本研究では CodeGear、DataGear を Agda に定義できた
+* また Agda で Interface の記述及び Interface を含めた一部の証明を行えた
+* これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた
+
+* 今後の課題としては 継続を用いた Agda で Hoare Logic を表現し、その Hoare Logic をベースとして証明を行えるかを確認する
+* また RedBlackTree の挿入、削除の性質に関する証明も行おうと考えている
## Hoare Logic