プログラムの仕様を検証するには モデル検査 と 定理証明 の２つの手法がある
- モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認する
- 定理証明 はプログラムの性質を論理式で記述しそれが常に正しいことを証明する
@@ -103,12 +103,6 @@
- また、当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している
-
-
-
-
-
-
@@ -118,168 +112,131 @@
CodeGear とはプログラムを記述する際の処理の単位である。
DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータが全て入っている。
CodeGear はメタ計算によって CodeGear へ接続される
-
接続はメタ計算で行われ、メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる
-
CodeGear は入力として DataGear を受け取り、 DataGear に変更を加えて次に指定された CodeGear へ継続する
+
メタ計算を切り替えることで処理に変更を加えることなくプログラムの性質を検証できる
+
Agda 上で CodeGear 、 DataGear という単位を定義した
-
+
-
Continuation based C (CbC)
+
Agda とは
- - 当研究室で開発している言語
- - 基本的な構文は C 言語と同じ
- - CodeGear、 DataGear という単位を用いてプログラムを記述する
- - CbC では 通常計算とメタ計算を分離している
- - CodeGear を継続し、 DataGear を変更しながらプログラムが進んでいく
- - CodeGear は関数の定義前に__codeがつく
- - 関数末尾の goto により次の CodeGear に継続する
+ - 定理証明支援系
+ - 関数型言語
+ - 型を明示する必要がある
+ - インデントも意味を持つ
+ - 型システムを用いて証明を記述できる
-
__code cg0(int a, int b){
- goto cg1(a+b);
-}
-__code cg1(int c){
- goto cg2(c);
-}
+
+
+
Agda の型、関数
+
+ - 例として singleLinkedStack の pop を使う
+ - Agda の 型は 関数名:型 で定義される
+ - Agda の 項、関数部分は 関数名 = 値
+ - なにかを受け取って計算して次の関数に継続する型(-> (fa -> t) -> t)
+ - これはstackを受け取り、stackの先頭を取ってという処理を行い、次の関数に渡すという関数の型
+ - このような形で CodeGear を Agda で定義できる
+
+
+
popSingleLinkedStack : -> SingleLinkedStack a
+ -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
-
Context
+
Maybe
- - CodeGear や DataGear をリストとして、 Context と呼ばれる Meta DataGear の中で定義している
- - しかし Context は Meta DataGear のため、通常レベルである CodeGear で直接扱うのは避けたい
- - その為、 stub CodeGear という Meta CodeGear を定義している。
- - stub CodeGear は Context を通して必要なデータを取り出し、次の CodeGear に接続する
- - stub CodeGear は CodeGear 毎に生成される
+ - Maybe はNothingかJustを返す型でAgda の dataとして定義されている
+ - ここでは Just か Nothing をパターンマッチで返す
+ - 要素にも型を書く必要がある
-
-
-
-
Interface
-
- - CbC で実装していくにつれて stub CodeGear の記述が煩雑になることがわかった
- - そこで Interface というモジュール化の仕組みを導入した
- - Interface は CodeGear とそこで扱われている DataGear の集合を抽象的に表現した Meta DataGear として定義されている
- - __code next(…) は継続を表していて …部分は後続の引数に相当する
-
-
-
typedef struct Stack<Type, Impl>{
- // DataGear
- union Data* stack;
- union Data* data;
- union Data* data1;
-
- // CodeGear
- __code whenEmpty(...);
- __code clear(Impl* stack,__code next(...));
- __code push(Impl* stack,Type* data, __code next(...));
- // 省略
- __code next(...);
-} Stack;
+data Maybe a : Set where
+ Nothing : Maybe a
+ Just : a -> Maybe a
-
Interface
+
refl
- - Interface を表す DataGear は次のような関数で生成される
- - stack->push のようにしてコード中で使うことができる
+ - data は data データ名 : と書く
+ - 等しいという data として refl が定義されている
-
Stack* createSingleLinkedStack(struct Context* context) {
- struct Stack* stack = new Stack();
- struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack();
- stack->stack = (union Data*)singleLinkedStack;
- singleLinkedStack->top = NULL;
- stack->push = C_pushSingleLinkedStack;
- stack->pop = C_popSingleLinkedStack;
- // 省略
- return stack;
+data _≡_ {a} {A : Set a} (x : A) : A → Set a where
+ refl : x ≡ x
-
Agda
+
Agdaの関数
- - Agda とは定理証明支援器で、型システムを用いて証明を記述できる。
- - Agda では関数の型を明示する必要がある
+ - 例として popSingleLinkedStack の関数を使う
+ - ラムダ式 とは関数内で定義できる名前のない関数
+ - \ -> で定義される
+ - ラムダ式を使って CodeGear を継続することができる
+ - 関数での引数は 関数名 a b : のように書く
+ - {変数} のように記述すると暗黙的な意味になり省略してもよい
-
-- Booleanの定義(データの定義例)
-data Bool : Set where
- true : Bool
- false : Bool
-
--- Bool値を反転する関数の例
-not : Bool → Bool
-not true = false
-not false = true
-
--- xor(複数の引数を取る例)
-xor : Bool → Bool → Bool
-xor true true = false
-xor false false = false
-xor _ _ = true
+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))
-
AGDA
+
record
- - Agda 上で CodeGear、 DataGear の単位と継続を定義した
- - DataGear はレコード型として定義し、 CodeGear は通常の関数。
+ - record は複数のデータを纏めて記述する型で、他の言語のオブジェクトのように レコード名.フィールド名 でアクセスできる
+ - SingleLinkedStack を例にとる
+ - record レコード名 と書き、その次の行に field と書く
+ - その下の行に フィールド名:型名 と列挙する
+ - SingleLinkedStack では top というフィールドに Maybe のかかっている Element 型の要素aが定義されている
+ - Element では record で data と次の要素 next を定義している
-
// CbC
-__code cg0(int a, int b){
- goto cg1(a+b);
-}
-
-
-
-- agda DataGear
-record dg0 : Set where
+record SingleLinkedStack (a : Set) : Set where
field
- a : Int
- b : Int
-
--- agda CodeGear define
-data CodeGear (A B : Set) : Set where
- cg : (A -> B) -> CodeGear A B
-
--- agda CodeGear example
-cg0 : CodeGear dg0 dg1
-cg0 = cg (\d -> goto cg1 (record {c = (dg0.a d) + (dg0.b d)}))
+ top : Maybe (Element a)
-
Agda での証明
+
pushSingleLinkedStackの定義とrecordの構築
- - 型で論理を書き、関数部分で導出
+ - pushSingleLinkedStack の型では stack と data を受け取り、 CodeGear 中で Data を stack に入れ、新しいstack を継続し、次の CodeGear に継続している
+ - 関数側では record の構築を行う
+ - record の後ろの {} 内部で フィールド名 = 値 の形で列挙する
+ - 複数書くときは ; で区切る
-
ex : 1 + 2 ≡ 3
-ex = refl
+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)})}
@@ -288,94 +245,108 @@
Agda での Interface の定義
- - Agda上でも CbC の Interface と同様のものを定義した。
+ - stack の色々な実装を抽象的に表すために record を使い StackMethods をつくった
+ - 実装時は関数の中で record を構築している
+ - push、 pop は実装によらないAPI
+ - push、 pop に singlelinkedstack の実装が入る
-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
- -- 省略
-open StackMethods
-
-record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
- field
- stack : si
- stackMethods : StackMethods {n} {m} a {t} si
- pushStack : a -> (Stack a si -> t) -> t
- pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
- popStack : (Stack a si -> Maybe a -> t) -> t
- popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
- -- 省略
-
-
-singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
-singleLinkedStackSpec = record {
- push = pushSingleLinkedStack
- ; pop = popSingleLinkedStack
- -- 省略
- }
-
-createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
-createSingleLinkedStack = record {
- stack = emptySingleLinkedStack ;
- stackMethods = singleLinkedStackSpec
- }
+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 中では不明な部分を ? と書くことができる
+ - ? 部分には値が入る
+ - 証明部分は ラムダ式で与える
+
-
+
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 }
+
-
-
-
+
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 = ?
+
-
Agda での Interface を含めた部分的な証明(Stack の例)
-
+
Agda での Interface を含めた部分的な証明
- - 不定な Stack を作成し、そこに push し、直後に pop した値が push した値と等しいことを示している
+ - 証明部分に書いた ? はコンパイル後に { }0 に変わり、中に入る型が表示される
+ - x、y はMaybe なので Justで返ってくる
+ - push した x、 y と x1、 y1 が共に等しいことを証明したい
+ - そこで ∧ の部分をrecordで定義した
-
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 }
+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
+
+-- Goal
+?0 : pushStack (stackInSomeState s) x
+(λ s1 →
+ pushStack s1 y
+ (λ s2 → pop2Stack s2 (λ s3 y1 x1 → (Just x ≡ x1) ∧ (Just y ≡ y1))))
-実際の証明
-push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
+
+
+
+
Agda での Interface を含めた部分的な証明(∧)
+
+ - a と b の証明から aかつb を作るコンストラクタ
+ - 直積を表す型を定義する
+
+
+
record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
+ field
+ pi1 : a
+ pi2 : b
+
+
+
+
+
+
Agda での Interface を含めた部分的な証明
+
+ - ∧でまとめたpi1、pi2は refl で証明することができた
+
+
+
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 の挿入、削除の性質に関する証明も行おうと考えている。
+
-
今後の課題
-
- - 本研究では Agda での Interface の記述及び Interface を含めた一部の証明を行った。
- - これにより、 Interface を経由しても一部の性質は実装と同様の働きをすることが証明できた。
- - また、これにより CbC での Interface 記述では考えられていなかった細かな記述が明らかになった。
- - 今後の課題としては Hoare Logic を継続を用いた Agda で表現し、その Hoare Logic をベースとして証明を行えるかを確認する。
+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)
+
-
+