+
+
+
+
+ |
+
+ GearsOSのAgdaによる記述と検証
+
+ |
+
+
+ |
+
+ Masataka Hokama, Shinji Kono
+ 琉球大学
+
+
+ |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
本発表の流れ
+
+ - 研究目的
+ - CodeGear と DataGear の説明
+ - Agda での記述
+ - Agda での CodeGear 、 DataGear 、 Interface の表現
+ - 実際に行なった証明
+ - 証明の改善
+ - まとめ
+
+
+
+
+
+
+
プログラムの信頼性の保証
+
+ - 動作するプログラムの信頼性を保証したい
+ - 保証をするためには仕様を検証する必要がある
+ - 仕様を検証するにはモデル検査と 定理証明 の２つの手法がある
+
+ - モデル検査 はプログラムの持つ状態を数え上げて仕様を満たしているかを確認するもの
+ - 定理証明 はプログラムの性質を論理式で記述し、型を生成する関数を定義することで証明を記述できるもの
+
+
+ - 当研究室では検証しやすい単位として CodeGear、DataGear という単位を用いてプログラムを記述する手法を提案している
+
+
+
+
+
+
+
プログラムの信頼性の保証
+
+ - 本研究では 定理証明支援系 の言語 Agda をつかって仕様を検証した
+ - データ構造を仕様と実装に分けて記述するため、モジュール化の仕組みである Interface を記述した
+ - 今回は Agda で CodeGear 、DataGear、という単位と Interface を定義した
+ - また、 CodeGear 、DataGear を用いて Agda 上に実装された Stack を Interface を通して呼び出し、その性質の一部について証明を行った
+
+
+
+
+
+
+
CodeGear と DataGear の定義
+
+ - CodeGear とはプログラムを記述する際の処理の単位
+ - DataGear は CodeGear で扱うデータの単位で、処理に必要なデータが全て入っている
+ - CodeGear はメタ計算によって別の CodeGear へ接続される
+
+
+
+
+
+
+
+
+
+
+
次のスライドからは Agda の記述について解説を行う
+
+
+
+
+
+
Agda での型
+
+ - Agda の 型は 関数名 : 型 のように : を使って定義される
+ - ここでは Stack の実装である popSingleLinkedStack の型を例とする
+ - この型は stack を受け取り、stack の先頭を取って、次の関数に渡すという関数の型
+ - stack は空の可能性があるので Maybe a を返す
+ - popSingleLinkedStack は Stack の pop のCodeGearで、継続に型 Maybe a を受けとる CodeGear ( (fa -> t) -> t) に渡す
+
+
+
popSingleLinkedStack : SingleLinkedStack a ->
+ (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+
+
+
+
+
+
+
Maybe
+
+ - Maybe はNothingかJustの２つの場合を持つ型で Agda の data として定義されている
+ - Just か Nothing はパターンマッチで場合分けするNothing と Just a は Maybe を生成する constructor
+
+
+
data Maybe a : Set where
+ Nothing : Maybe a
+ Just : a -> Maybe a
+
+
+
+
+
+
+
data を用いた等式の証明
+
+ - x ≡ x は Agda では常に正しい論理式
+ - data は data データ名 : 型
+ - refl は左右の項が等しいことを表す x ≡ x を生成する項
+ - x ≡ x を証明したい時には refl と書く
+
+
+
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
+ refl : x ≡ x
+
+
+
+
+
+
+
Agda での関数
+
+ - Agda での関数定義は 関数名 = 関数の実装
+ - ここでは popSingleLinkedStack の関数を例とする
+ - 引数は 関数名 と = の間に記述する
+ - stack と 次の CodeGear である cs を受け取り、 stack の中から data を取り出し、新しい stack に継続し、次の CodeGear へと stack 渡している
+ - stack の top は Maybe a なので Nothing か Just が返ってくる
+ - with で data のパターンマッチができる
+
+
+
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 の定義
+
+ - record は複数のデータをまとめて記述する型
+ - record レコード名 を書き、その次の行の field 後に フィールド名:型名 と列挙する
+ - ここでは SingleLinkedStack の定義を例とする
+ - 定義では top フィールドのみを定義しているが複数定義することもできる
+ - top には Element 型の要素 a が定義されており、 Element 型は現在の data と次の data を指す next を定義している
+
+
+
record SingleLinkedStack (a : Set) : Set where
+ field
+ top : Maybe (Element a)
+
+
+
+
+
+
+
Agda での record の構築
+
+ - record の構築は関数側
+ - record 後ろの {} 内部で フィールド名 = 値 で列挙する
+ - 複数のレコードを記述するさいは ; で区切る
+ - 例として pushSingleLinkedStack の関数部分を扱う
+ - pushSingleLinkedStack では stack と data を受け取り、 CodeGear 中で Data を stack に入れ、新しいstack を継続し、次の CodeGear に継続している
+
+
+
pushSingleLinkedStack stack datum next =
+ next record {top = Just (record {datum = datum;next =(top stack)})}
+
+
+
+
+
+
+
Agda での Interface の定義
+
+ - Stack の仕様を実装とは別に記述するために record で Stack の Interface を記述した
+ - ここでの push、 pop は仕様の型のみ記述され、実装は構築時に与える
+ - t は継続を返す型を表し、次の CodeGear を指す
+ - ここでの push 、 pop は pushSingleLinkedStack 、 popSingleLinkedStack に繋げる
+
+
+
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
+
+
+
+
+
+
+
証明の概要
+
+ - 今回は Interface を通して、 任意の数 を stack に push し、データが入った stack に対して pop を行なう
+ - このとき push した値と pop した値が等しくなることを証明する
+ - また、どのような状態の Stack に push し、 pop をしても値が等しくなることを示したい
+ - そのため、状態の不定な Stack を作成する関数を定義した
+
+
+
+
+
+
+
状態が不定な Stack の定義
+
+ - ここでは状態が不定な Stack を作成する関数 stackInSomeState を定義する
+ - 不定なstackを入力(s : SingleLinkedStack a )で与える
+ - stackInSomeState は stack を受け取り、状態の決まっていない stack を構築する
+
+
+
stackInSomeState : (s : SingleLinkedStack a ) -> Stack a ( SingleLinkedStack a )
+stackInSomeState s = record { stack = s ; stackMethods = singleLinkedStackSpec }
+
+
+
+
+
+
+
Agda での Interface を含めた部分的な証明
+
+ - 証明部分は型部分にラムダ式で与える
+ - push->push->pop2では push を２回したときの値と、直後に pop を2回して取れた値が等しいことを型に記述している
+
+
+
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 = ?
+
+
+
+
+
+
+
ラムダ式
+
+ - \s1 -> はラムダ式で push->push->pop2 の型では次の CodeGear 部分にラムダ式を使いStackを渡している
+
+
+
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))))
+
+
+
+
+
+
+
Agda での Interface を含めた部分的な証明
+
+ - ここでは最終的に (Just x ≡ x1) ∧ (Just y ≡ y1) が返ってくる必要がある
+ - (x ≡ x1) と (y ≡ y1) の２つが同時に成り立つ必要がある
+ - そこで ∧ の部分を record で定義した
+
+
+
-- 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
+
+
+
+
+
+
+
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 }
+
+
+
+
+
+
+
手証明での限界
+
+ - 現在 Binary Tree に対して近い証明を書いている
+ - これは 「Tree に対して node を put し、 get した時取れる node の値は put した node と等しい」というもの
+ - Tree に対する操作では root Node から Node を辿る Loop があり、それを展開しながら証明を書く
+ - Agda 側が put した node と get した node が等しいことを分かってくれず、証明が完成していない…
+ - 今後は新しい証明規則を導入して証明を行おうと考えている
+
+
+
+
+
+
+
Hoare Logic
+
+ - Hoare Logic は Tony Hoare によって提案されたプログラムの部分的な正当性を検証するための手法
+ - 前の状態を{P}(Pre-Condition)、後の状態を{Q}(Post-Condition)とし、前状態を C (Command) によって変更するといったもの
+ - この {P} C {Q} でプログラムを部分的に表すことができる
+ - {P} が成り立つときに、 C を実行すると、実行後は必ず {Q} が成り立つとき、部分的に正当である
+
+
+
+
+
+
+
+
+
+
+
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 をベースとして証明が行えるかを検討する
+
+
+
+
+
+
+
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)
+
+
+
+
+
+
+
+ 
+