# HG changeset patch
# User ryokka
# Date 1526821044 -32400
# Node ID 328bcfd300bdffb6ac84c61cee8e6e179b654700
# Parent 907f967f662e91f820d4875868bd29506784fbe6
fix slides
diff -r 907f967f662e -r 328bcfd300bd Slide/fig/cbc-hoare.xbb
--- a/Slide/fig/cbc-hoare.xbb Sat May 19 19:14:19 2018 +0900
+++ b/Slide/fig/cbc-hoare.xbb Sun May 20 21:57:24 2018 +0900
@@ -1,8 +1,8 @@
-%%Title: fig/cbc-hoare.pdf
+%%Title: cbc-hoare.pdf
%%Creator: extractbb 20180217
%%BoundingBox: 0 0 580 175
%%HiResBoundingBox: 0.000000 0.000000 580.000000 175.000000
%%PDFVersion: 1.3
%%Pages: 1
-%%CreationDate: Tue May 15 18:15:06 2018
+%%CreationDate: Sat May 19 20:23:56 2018
diff -r 907f967f662e -r 328bcfd300bd Slide/fig/hoare-logic.xbb
--- a/Slide/fig/hoare-logic.xbb Sat May 19 19:14:19 2018 +0900
+++ b/Slide/fig/hoare-logic.xbb Sun May 20 21:57:24 2018 +0900
@@ -1,8 +1,8 @@
-%%Title: fig/hoare-logic.pdf
+%%Title: hoare-logic.pdf
%%Creator: extractbb 20180217
%%BoundingBox: 0 0 580 76
%%HiResBoundingBox: 0.000000 0.000000 580.000000 76.000000
%%PDFVersion: 1.3
%%Pages: 1
-%%CreationDate: Tue May 15 18:15:06 2018
+%%CreationDate: Sat May 19 20:23:56 2018
diff -r 907f967f662e -r 328bcfd300bd Slide/fig/meta.xbb
--- a/Slide/fig/meta.xbb Sat May 19 19:14:19 2018 +0900
+++ b/Slide/fig/meta.xbb Sun May 20 21:57:24 2018 +0900
@@ -1,8 +1,8 @@
-%%Title: fig/meta.pdf
+%%Title: meta.pdf
%%Creator: extractbb 20180217
%%BoundingBox: 0 0 958 148
%%HiResBoundingBox: 0.000000 0.000000 958.000000 148.000000
%%PDFVersion: 1.3
%%Pages: 1
-%%CreationDate: Tue May 15 18:15:06 2018
+%%CreationDate: Sat May 19 20:23:56 2018
diff -r 907f967f662e -r 328bcfd300bd Slide/sigos.html
--- a/Slide/sigos.html Sat May 19 19:14:19 2018 +0900
+++ b/Slide/sigos.html Sun May 20 21:57:24 2018 +0900
@@ -86,7 +86,7 @@
@@ -100,10 +100,10 @@
- 研究目的
- CodeGear と DataGear の説明
- - Agda での記述
+ - Agda の記述
+ - Interface の説明
- Agda での CodeGear 、 DataGear 、 Interface の表現
- 実際に行なった証明
- - 証明の改善
- まとめ
@@ -117,11 +117,12 @@
保証をするためには仕様を検証する必要がある
仕様を検証するにはモデル検査と 定理証明 の２つの手法がある
- - モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認するもの
- - 定理証明 はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述できるもの
+ - モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているか
+ - 定理証明 はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述する
当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している
+ また、上記の単位で計算をノーマルレベル、メタレベルに分け、信頼性と拡張性をメタレベルで保証する GearsOS を開発している
@@ -129,11 +130,12 @@
プログラムの信頼性の保証
+
- - 本研究では 定理証明支援系 の言語 Agda をつかって仕様を検証した
- - データ構造を仕様と実装に分けて記述するため、モジュール化の仕組みである Interface を記述した
- - 今回は Agda で CodeGear 、DataGear、という単位と Interface を定義した
- - また、 CodeGear 、DataGear を用いて Agda 上に実装された Stack を Interface を通して呼び出し、その性質の一部について証明を行った
+ - CodeGear、 DataGear を使ったプログラミングは関数型プログラミングに近い形になる
+ - 本研究では関数型の 定理証明支援系 の言語 Agda を用いて仕様を検証することとした
+ - Agda で CodeGear 、DataGear、という単位と Interface を定義した
+ - CodeGear 、DataGear を用いて Agda 上に実装された Stack を Interface を通して呼び出し、その性質の一部について証明を行った
@@ -142,20 +144,55 @@
CodeGear と DataGear の定義
- - CodeGear とはプログラムを記述する際の処理の単位
+ - CodeGear とはプログラムを記述する際の処理の単位で、Agda では通常の関数で表現する
- DataGear は CodeGear で扱うデータの単位で、処理に必要なデータが全て入っている
- - CodeGear はメタ計算によって別の CodeGear へ接続される
+ - CodeGear はメタ計算によって次の CodeGear へ接続される
+ - メタ計算部分では並列処理などの様々な処理を記述ができる
+
+
+
+
+
+
+
+
+
+
+
Hoare Logic
+
+ - Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証する手法
+ - 前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) で変更する
+ - {P} が成り立つときに、 C を実行すると、実行後は必ず {Q} が成り立つとき、部分的に正当である
-
+
-
-
-
+
+
+
+
Hoare Logic と CodeGear、 DataGear
+
+ - Hoare Logic の状態と処理を CodeGear、 DataGear に当てはめる事ができる
+ - Pre-condition を input の DataGear , Post-Conditon を output の DataGear , Command は CodeGear そのもの
+ - Pre-conditon や Post-conditon をメタ計算部分で検証し、 CodeGear、 DataGear で書かれたプログラムに対して検証する
+
-
次のスライドからは Agda の記述について解説を行う
+
+
+
+
+
+
+
+
Agda での CodeGear、 DataGear の表現
+
+ - CodeGear は処理の単位なので、 Agda では通常関数として記述する
+ - DataGear は Agda の record を使用し記述する
+
Agda での型
- - Agda の 型は 関数名 : 型 のように : を使って定義される
- - ここでは Stack の実装である popSingleLinkedStack の型を例とする
- - この型は stack を受け取り、stack の先頭を取って、次の関数に渡すという関数の型
- - stack は空の可能性があるので Maybe a を返す
- - popSingleLinkedStack は Stack の pop のCodeGearで、継続に型 Maybe a を受けとる CodeGear ( (fa -> t) -> t) に渡す
+ - 型は 関数名 : 型 のように : を使って定義する
+ - a -> b という型は、「a を受け取り、 b を返す」という型
+ - a -> b -> c のような型は a -> (b -> c) と同じで、 「a を受け取り、 b を受け取り、 c を返す」 という型
+
+
+
+
+
+
+
Agda での型(例)
+
+ - CodeGear の型 は (code: a -> t) -> t のような形になる
+ - 例として通常の push (nomalPush) と 継続を用いた push (continuePush) の型を考える
+
+
+
-- 通常のstack
+nomalPush : Si -> a -> Si
+-- 継続を用いたstack
+continuePush : Si -> a -> (CodeGear : Si -> t) -> t
+
+
+
+ - nomalPush は 「stack と data を受け取り、 data が取り出された stack を返す」型
+ - continuePush は 「stack と data と 継続先の (Code : ) を受け取り、 継続先である tを返す」型
+ - t は明示されていない不定な型で、継続を表している
+
+
+
+
+
+
Agda での型(例2)
+
+ - 実際に Stack の pop 操作の 実装 である popSingleLinkedStack の型を見る
popSingleLinkedStack : SingleLinkedStack a ->
(Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+
+ - この型では stack と行き先の CodeGear を受け取り、次の CodeGear に継続する
+ - popSingleLinkedStack 継続に型 Maybe a を受けとる CodeGear ( (fa -> t) -> t) に渡している
+ - stack の中身は空の可能性があるので Maybe型の a を返す
+
+
@@ -181,7 +253,7 @@
Maybe
- Maybe はNothingかJustの２つの場合を持つ型で Agda の data として定義されている
- - Just か Nothing はパターンマッチで場合分けするNothing と Just a は Maybe を生成する constructor
+ - Just か Nothing は場合分けで Nothing と Just a は Maybe を生成する constructor
data Maybe a : Set where
@@ -193,11 +265,11 @@
-
data を用いた等式の証明
+
Agda でのデータ
- - x ≡ x は Agda では常に正しい論理式
- - data は data データ名 : 型
- - refl は左右の項が等しいことを表す x ≡ x を生成する項
+ - データは data データ名 : 型
+ - (x : A) は ある集合(a)に属する {A} という型を持った変数 x を表現
+ - refl は左右の項が等しいことを表す x ≡ x を生成
- x ≡ x を証明したい時には refl と書く
@@ -209,32 +281,30 @@
-
Agda での関数
+
refl を使った証明
- - Agda での関数定義は 関数名 = 関数の実装
- - ここでは popSingleLinkedStack の関数を例とする
- - 引数は 関数名 と = の間に記述する
- - stack と 次の CodeGear である cs を受け取り、 stack の中から data を取り出し、新しい stack に継続し、次の CodeGear へと stack 渡している
- - stack の top は Maybe a なので Nothing か Just が返ってくる
- - with で data のパターンマッチができる
+ - refl を使った例題 sym
-
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))
+sym : {x : Set} {y : Set} -> x ≡ y -> y ≡ x
+sym refl = refl
+
+ - x ≡ y ならば y ≡ x の証明
+ - 型は論理式として成り立っており、関数で証明を行っている
+ - 初めの x ≡ y は引数として与えられ、これは refl
+ - x ≡ y が成り立つ時、初めて y ≡ x は refl
+
+
Agda での record の定義
- - record は複数のデータをまとめて記述する型
- - record レコード名 を書き、その次の行の field 後に フィールド名:型名 と列挙する
+ - record 複数のデータをまとめて記述する型
- ここでは SingleLinkedStack の定義を例とする
- - 定義では top フィールドのみを定義しているが複数定義することもできる
- - top には Element 型の要素 a が定義されており、 Element 型は現在の data と次の data を指す next を定義している
record SingleLinkedStack (a : Set) : Set where
@@ -242,37 +312,96 @@
top : Maybe (Element a)
+
+ - record レコード名 、下に field 、さらに下に フィールド名:型名 を列挙
+ - フィールド名は accessor
+ - top は Maybe (Element a) 型
+
+
+
+
+
+
+
Element
+
+ - Element 型も record で定義されている
+ - このレコードは直積になっている
+ - datum は Element の要素自体で、 next は次の要素
+
+
+
record Element (a : Set) : Set where
+ field
+ datum : a
+ next : Maybe (Element a)
+
+
-
Agda での record の構築
+
Agda での関数
- - record の構築は関数側
- - record 後ろの {} 内部で フィールド名 = 値 で列挙する
- - 複数のレコードを記述するさいは ; で区切る
- - 例として pushSingleLinkedStack の関数部分を扱う
- - pushSingleLinkedStack では stack と data を受け取り、 CodeGear 中で Data を stack に入れ、新しいstack を継続し、次の CodeGear に継続している
+ - Agda での関数は 関数名 = 関数の実装
+ - ここでは popSingleLinkedStack の関数を例とする
+
+ - 関数名 と = の間に記述されてる stack 、 cg は引数
+ - stack の top は Maybe a なので Nothing か Just が返り、2つの場合が存在
+ - with と | を使うことで data の場合分けができる
+
+
-
pushSingleLinkedStack stack datum next =
- next record {top = Just (record {datum = datum;next =(top stack)})}
+popSingleLinkedStack : SingleLinkedStack a ->
+ (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+popSingleLinkedStack stack cg with (top stack)
+popSingleLinkedStack stack cg | Nothing = cg stack Nothing
+popSingleLinkedStack stack cg | Just d = cg record { top = (next d) } (Just (datum d))
+
Agda での record の作成
+
+ - record の作成は関数内で行う
+ - 例として pushSingleLinkedStack の関数部分を扱う
+
+
+
pushSingleLinkedStack : {t : Set} {a : Set} -> SingleLinkedStack a -> a -> (Code : SingleLinkedStack a -> t) -> t
+pushSingleLinkedStack stack datum next = next record {top = Just (record {datum = datum;next =(top stack)})}
+
+
+
+ - record 後ろの {} 内部で フィールド名 = 値 で列挙
+ - 複数のフィールドを作成する際は ; で区切る
+
+
+
+
+
+
Inteface
+
+ - Interface は GearsOS のモジュール化の仕組み
+ - ある Data Gear と それに対する操作(API) を行う Code Gear の集合を表現
+ - Interface を使うとデータ構造への操作を仕様と実装に分けて記述することができる
+
+
+
+
+
Agda での Interface の定義
- - Stack の仕様を実装とは別に記述するために record で Stack の Interface を記述した
+ - GearsOS の Interface を Agda で定義した
+
- ここでの push、 pop は仕様の型のみ記述され、実装は構築時に与える
- - t は継続を返す型を表し、次の CodeGear を指す
- - ここでの push 、 pop は pushSingleLinkedStack 、 popSingleLinkedStack に繋げる
+ - t は不定な型で継続を表し、次の CodeGear を指す
+ - StackMethods は Stack から interface を通して singleLinkedStack への操作を行う際の型を定義してる
-
record StackMethods {n m : Level } (a : Set n )
- {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
+record StackMethods (a : Set) {t : Set} (stackImpl : Set) : Set where
field
push : stackImpl -> a -> (stackImpl -> t) -> t
pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t
@@ -282,12 +411,39 @@
+
Agda での Interface の記述
+
+ - Stack を作成するとき仕様と実装を繋げている
+ - createSingleLinkedStack は中身のない Stack を作る
+
+
+
createSingleLinkedStack : {t : Set} {a : Set} -> Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+ stack = emptySingleLinkedStack ;
+ stackMethods = singleLinkedStackSpec
+ }
+
+
+
+ - singleLinkedStackSpec は実装側の push、 pop をまとめている
+
+
+
singleLinkedStackSpec : {t : Set} {a : Set} -> StackMethods a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+ push = pushSingleLinkedStack
+ ; pop = popSingleLinkedStack
+ }
+
+
+
+
+
証明の概要
- - 今回は Interface を通して、 任意の数 を stack に push し、データが入った stack に対して pop を行なう
- - このとき push した値と pop した値が等しくなることを証明する
- - また、どのような状態の Stack に push し、 pop をしても値が等しくなることを示したい
- - そのため、状態の不定な Stack を作成する関数を定義した
+ - 今回は 任意の数 を Stack に push し、直後にその Stack に対して pop を行ない、 push したデータと pop して取れたデータが等しくなることを証明する
+ - どのような状態の Stack に push し、 pop をしても値が等しくなって欲しい
+ - 状態の不定な Stack を作成する関数を定義した
@@ -296,9 +452,9 @@
状態が不定な Stack の定義
- - ここでは状態が不定な Stack を作成する関数 stackInSomeState を定義する
- - 不定なstackを入力(s : SingleLinkedStack a )で与える
- - stackInSomeState は stack を受け取り、状態の決まっていない stack を構築する
+ - 状態が不定な Stack を作成する関数 stackInSomeState
+ - 入力を使って任意の Stack を表す
+ - stackInSomeState は Stack を受け取り、状態の決まっていない Stack を作成
stackInSomeState : (s : SingleLinkedStack a ) -> Stack a ( SingleLinkedStack a )
@@ -309,50 +465,28 @@
-
Agda での Interface を含めた部分的な証明
+
Agda での Interface を含めた部分的な証明
- - 証明部分は型部分にラムダ式で与える
- - push->push->pop2では push を２回したときの値と、直後に pop を2回して取れた値が等しいことを型に記述している
+ - push->popでは push をし、直後に pop をして取れたデータが等しい
+ - Agda では不明な部分を ? と書くことができ、証明部分を ? としている
-
push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
- pushStack ( stackInSomeState s ) x ( \s1 -> pushStack s1 y ( \s2 ->
- pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-push->push->pop2 {l} {a} x y s = ?
+push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 )))
+push->pop {a} x s = ?
-
ラムダ式
+
push->pop の型
- - \s1 -> はラムダ式で push->push->pop2 の型では次の CodeGear 部分にラムダ式を使いStackを渡している
+ - ラムダ計算で結果を次の実行に渡している
+ - ラムダ計算は関数を抽象的に扱うもので、名前がなく、入力と出力だけ
+ - ここでは \s1 -> がラムダ計算で、受け取った Stack (s) に push を行い、更新された Stack (s1) を次の CodeGear に渡している
-
push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
- pushStack ( stackInSomeState s ) x ( \s1 ->* pushStack s1 y ( \s2 ->
- pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-
-
-
-
-
-
Agda での Interface を含めた部分的な証明
-
- - Agda では不明な部分を ? と書くことができる
- - ? 部分はコンパイルすると {}n のように番号が付き、Agda から内部に入る型を示してもらえる
-
-
-
push->push->pop2 {l} {a} x y s = { }0
-
-
-
-- Goal
-?0 : pushStack (stackInSomeState s) x
-(λ s1 →
- pushStack s1 y
- (λ s2 → pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))
+push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 )))
@@ -361,194 +495,45 @@
Agda での Interface を含めた部分的な証明
- - ここでは最終的に (Just x ≡ x1) ∧ (Just y ≡ y1) が返ってくる必要がある
- - (x ≡ x1) と (y ≡ y1) の２つが同時に成り立つ必要がある
- - そこで ∧ の部分を record で定義した
+ - ? 部分はコンパイルすると {}n のように番号が付き、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 という証明を行うため ∧ を定義する
- - これには異なる２つのものを引数にとり、それらがレコードに同時に存在することが示せれば良い
- - ∧ は 型 a と 型b をもつ2つの要素を左右にとり、 それらが同時に存在することを示すレコード型
-
-
-
record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
- field
- pi1 : a
- pi2 : b
+push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 )))
+push->pop {a} x s = { }0
-
-
-
-
Agda での Interface を含めた部分的な証明
-
- - 定義した ∧ を関数部分で構築する
- - ここでは pi1 、 pi2 の両方を ? としておく
-
-
-
push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
- pushStack ( stackInSomeState s ) x ( \s1 -> pushStack s1 y ( \s2 ->
- pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-push->push->pop2 {l} {a} x y s = record { pi1 = { }0 ; pi2 = { }1 }
-
-
-
?0 : Just x ≡
-Just
-(Element.datum
- (.stack.element (stack (stackInSomeState s)) x
- (λ s1 →
- pushStack
- (record
- { stack = s1 ; stackMethods = stackMethods (stackInSomeState s) })
- y
- (λ s2 →
- pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))))
-
-
-
-
-
-
Agda での Interface を含めた部分的な証明
-
- - ∧ で定義された左右に x ≡ x1 と y ≡ y1 が入る
- - x ≡ x1、 y ≡ y1 は共に refl で証明できる
- - pi1、pi2 は両方 refl が入ることで証明ができる
- - また、型に書かれた順で値が取り出されている為、最後のラムダ式で stack の性質である FIFO 通りに値が取れていることが分かる
- - これにより証明の目的であった「どのような状態の Stack に push し、 pop をしても値が等しくなる」ことを証明することができた
-
-
-
push->push->pop2 : {l : Level } {a : Set l} (x y : a ) (s : SingleLinkedStack a ) ->
- pushStack ( stackInSomeState s ) x ( \s1 -> pushStack s1 y ( \s2 ->
- pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
-push->push->pop2 {l} {a} x y s = record { pi1 = refl ; pi2 = refl }
+?0 : pushStack (stackInSomeState s) x
+(λ s1 → popStack s1 (λ s2 → _≡_ (Just x)))
-
手証明での限界
+
Agda での Interface を含めた部分的な証明
- - 現在 Binary Tree に対して近い証明を書いている
- - これは 「Tree に対して node を put し、 get した時取れる node の値は put した node と等しい」というもの
- - Tree に対する操作では root Node から Node を辿る Loop があり、それを展開しながら証明を書く
- - Agda 側が put した node と get した node が等しいことを分かってくれず、証明が完成していない…
- - 今後は新しい証明規則を導入して証明を行おうと考えている
+ - { }0 部分には x≡x1 が入り、これは refl
-
-
-
-
Hoare Logic
-
- - Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証するための手法
- - 前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) によって変更するといったもの
- - この {P} C {Q} でプログラムを部分的に表すことができる
- - {P} が成り立つときに、 C を実行すると、実行後は必ず {Q} が成り立つとき、部分的に正当である
-
+
push->pop : {a : Set } (x : a ) (s : SingleLinkedStack a ) -> pushStack (stackInSomeState s) x (\s1 -> popStack s1 (\s2 x1 -> (Just x ≡ x1 )))
+push->pop {a} x s = refl
+
-
-
-
-
-
-
-
-
Hoare Logic と CbC
-
-
- - Hoare Logic の状態と処理を CodeGear、 DataGear の単位で考えることができると考えている
- - Pre-condition を input DataGear , Post-Conditon を output DataGear , Command は CodeGear そのものとして扱えると考えている。
-
-
-
-
-
+
とすることで証明することができた
-
Hoare Logic での例 (Binary Tree)
-
-
-
- - この例では今後の証明に使おうとしている BinaryTree での put, get を例にする。
- - 初めに Node を put するべき位置を調べる “findNode” を行い root から ノードを辿っている。ここでは辿ったノードを Stack に保存する
- - 次に put すべき位置から木を再構成する”replaceNode”を行い、 Stack に保存したノードを辿り、木を再構築していく
-
-
-
-
-
-
-
ここでは findNode に注目する。
-
-
-
-
-
Hoare Logic での例 (Binary Tree : findNode)
-
- - findNode では引数として受け取ったノードと木の現在見ているノードを比較して ノードを入れる位置を決定している
- - また、Tree を再構築するために辿った node を Stack に保存している
- - この時 Hoare Logic 上での {P} 、 {Q} は Tree と Stack の総量 になると考えている
- - {P} が 元のTree と 中身のないStack で、 {Q} が 中身のないTree と 全てのNodeが入ったStack となる
-
- - このように C で不変な変数を見つけることでループなどの処理も部分的に正当であると証明することができる
-
-
-
-
-
-
-
-
-
-
まとめと今後の方針
-
+
まとめと今後の方針
- 本研究では CodeGear、DataGear を Agda で定義することができた
- また Agda で Interface の記述及び Interface を含めた証明を行うことができた
- これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた
- また、CbC での Interface 記述では考えられていなかった細かな記述が明らかになった
- - 今後の方針としては 継続を用いた Agda で Hoare Logic を表現し、その Hoare Logic をベースとして証明が行えるかを検討する
+ - RedBlackTree では Stack と異なり一つの操作に複数の CodeGear が入っているため Hoare Logic を使っての証明や、関数を展開しての証明などを行う
+ - SynchronisedQueue の証明では並列処理シミュレーションを Agda で行うことと、動機機構などを含めての証明を行う
-
-
-
-
-
Element
-
-
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)
-
-
+
+
-
+
+
+
-
-
-
-