Papers/2019/ryokka-sigss: slide/slide.md comparison

comparison slide/slide.md @ 11:17b7605a5deb

add figures, some slides

author	ryokka
date	Sun, 13 Jan 2019 23:42:16 +0900
parents	a87fec07fd78
children	e8fe28afe61e

comparison

equal deleted inserted replaced

-:a87fec07fd78
+:17b7605a5deb
 profile: 琉球大学 : 並列信頼研究室
 lang: Japanese
 <!-- 発表20分、質疑応答5分 -->
-## 研究目的
+## 研究背景
-<!-- 後回しだ！！！！！ -->
+- OS やアプリケーションなどの信頼性は重要な課題
-- OS やアプリケーションなどの信頼性は重要な課題である。
+- 信頼性を上げるために仕様を検証する必要
-- プログラムの信頼性を上げるためには仕様を検証する必要がある。
+- 仕様検証の手法として Floyd-Hoare Logic (以下 HoareLogic) がある
-- 使用の検証手法として Floyd-Hoare Logic (以下 HoareLogic) があり。
+- 事前条件(PreCondition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(PostCondition)を満たす
-- これはプログラムを Pre、Post Condition(事前、事後条件)、Command (関数)
+- 既存の言語ではあまり利用されていない(python の pyrefine ってコードチェッカーくらい...?)
-- 当研究室では信頼性の高い OS として GearsOS を開発している。
-- GearsOS では CodeGear、 DataGear という単位を用いてプログラムを記述する手法を提案している。
+## 背景
-- OS やアプリケーションなど、ソフトウェアの信頼性を高めることは重要である。
+- 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案
-- そのために当研究室では CodeGear 、 DataGear という単位を用いてプログラムを記述する手法を提案している。
+- CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む
-- CodeGear は処理の単位で、処理が終わると次の CodeGear へと継続を行う。
+- Gear 間の接続処理はメタ計算として定義
-- このとき、 CodeGear は通常の関数呼び出しとは異なり、呼び出し前の環境を持たずに継続をする。
+- メタ計算部分に検証を埋め込むことで通常処理に手を加えずに検証
-- DataGear はデータの単位で、 CodeGear の入力、出力変数となる。
+- 本研究では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する
-- また、当研究室では Gears の単位を用いて作られる OS である、 GearsOS を開発している。
-- 本研究では Gears OS の信頼性を高めるため、 Gears の単位を用いた検証手法を提案する。
+<p style="text-align:center;"><img src="./pic/cgdg-small.svg" alt=""  width="75%" height="75%"/></p>
-* 当研究室では検証しやすい単位として **CodeGear**、**DataGear** という単位を用いてプログラムを記述する手法を提案している
-* **CodeGear** とはプログラムを記述する際の処理の単位
-* **DataGear** は CodeGear で扱うデータの単位
-* これは関数型プログラミングに近い形になる
-* 本研究では関数型言語であり、 **証明支援系** 言語でもある **Agda** を用いて仕様を検証することにしている
-<!-- * 動作するプログラムは高い信頼性を持っていてほしい -->
-<!-- * そのために当研究室では CodeGear 、 DataGear を用いて記述する手法を提案している -->
-<!-- * 処理の単位である CodeGear を継続しプログラムを記述していく -->
-<!-- * メタ計算部分を切り替えることで CodeGear の処理を変更すること無くプログラムの検証をすることができる -->
-<!-- * 継続に関数を呼び出すときの前提条件(pre-condition)を追加することができ、Hoare Logic を用いた証明を Agda で記述できると考えている -->
-<!-- * 本研究では CodeGear, DataGear という単位を用いてプログラムを記述する手法の継続部分で Hoare Logic をベースにした証明手法を検討する -->
 ## Gears について
 - **Gears** は当研究室で提案しているプログラム記述手法
 - 計算の単位を **CodeGear** 、データの単位を **DataGear**
 - CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す
 - Output の DataGear は次の CodeGear の Input として接続される
 <!-- [fig1](file://./fig/cgdg.pdf) -->
 - CodeGear の接続処理は通常の計算とは異なるメタ計算として定義
 - メタ計算で信頼性の検証を行う
+<!-- ![cgdg](./pic/codeGear_dataGear.pdf){} -->
+<p style="text-align:center;"><img src="./pic/cgdg.svg" alt=""  width="30%" height="30%"/></p>
 ## CbC について
-- Gears の単位でプログラミングできる言語として CbC (Continuation based C) が存在
+- Gears の単位でプログラミングできる言語として当研究室で開発している **CbC** (Continuation based C) が存在
-- 現在の CbC では assert での検証ができる
+- これは C からループ制御構造と関数呼び出しを取り除き継続を導入したもの
+- 環境を継続に含めない
+- 現在の CbC ではメタ計算での検証
 - 将来的には証明も扱えるようにしたいが現段階では未実装
-- そのため Gears の単位を定理証明支援系の言語である **Agda** で記述できるようにし、 Agda 上で証明を行う
+- そのため Gears の単位を定理証明支援系の言語である **Agda** で記述し、 Agda で証明している
 ## Agda
 - Agda は定理証明支援系の言語
 - 依存型を持つ関数型言語
 - 型を明記する必要がある
 ## Agda のデータ型
 - データ型は代数的なデータ構造
 - **data** キーワードの後に、**名前 : 型**、 where 句
 - 次の行以降は**コンストラクタ名 : 型**
-- 型は**->**または**→**で繋げる事ができる
+- 型は**->**または**→**で繋げる
-- **PrimComm −> Comm**は**PrimComm** を受け取り、 **Comm**を返す型
+- 例えば、型**PrimComm −> Comm**は**PrimComm** を受け取り**Comm**を返す型
 - 再帰的な定義も可能
+```AGDA
-```AGDA
+data Comm : Set where
-data Comm : Set where
+Skip : Comm
-Skip : Comm
+Abort : Comm
-Abort : Comm
+PComm : PrimComm −> Comm
-PComm : PrimComm −> Comm
+Seq : Comm −> Comm −> Comm
-Seq : Comm −> Comm −> Comm
+If : Cond −> Comm −> Comm −> Comm
-If : Cond −> Comm −> Comm −> Comm
+While : Cond −> Comm −> Comm
-While : Cond −> Comm −> Comm
 ```
 <!-- - where は宣言した部分に束縛する -->
 ## Agda のレコード型
 - C 言語での構造体に近い
-- 複数のデータ型をまとめる
+- 複数のデータをまとめる
 - 関数内で構築できる
 - 構築時は**レコード名 {フィールド名 = 値}**
 - 複数ある場合は **{フィールド1 = 1 ; フィールド2 = 2}**のように **;** を使って列挙
+- (varn,vari の型 **ℕ** は Agda 上の 自然数、 データ型で zero : ℕ と succ : ℕ -> ℕ で定義されてる)
 ```AGDA
 record Env : Set where
 field
 varn : ℕ
 vari : ℕ
 ```
 ## Agda の関数
 - 関数にも型が必要
 - 関数は **関数名 = 値**
 - 関数ではパターンマッチがかける
 - **_** は任意の引数
+```AGDA
-```AGDA
+_-_ : ℕ → ℕ → ℕ
-_−_ : ℕ → ℕ → ℕ
+x - zero  = x
-x       − zero    = x
+zero - _  = zero
-zero    − _       = zero
+(suc x) - (suc y)  = x - y
-(suc x) − (suc y) = x − y
 ```
 ## Agda での証明
 - 関数の型に論理式
 - 関数自体にそれを満たす導出
 - 完成した関数は証明
 - **{}** は暗黙的(推論される)
 - 下のコードは自然数に 0 を足したとき値が変わらないことの証明
+```AGDA
-```AGDA
++zero : { y : ℕ } → y + zero  ≡ y
-+zero : {y : ℕ} → y + zero ≡ y
++zero {zero} = refl
-+zero {zero} = refl
++zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
-+zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
 ```
 ## Agda 上での HoareLogic
 * 現在 Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと
 それを Agda2 に書き写したものが存在している。
 * 今回はAgda2側の HoareLogic で使うコマンド定義の一部と、コマンドの証明に使うルールを借りて説明を行う。
 ## Agda での HoareLogic の理解
 * HoareLogic を用いて次のようなプログラム(while Program)を検証した。
 ```C
 n = 10;
 i = 0;
 while (n>0)
 {
 i++;
 n--;
 }
 ```
 * このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす
 * n==0のとき停止するため、終了時の変数の結果はi==10、n==0 になるはずである。
 ## HoareLogic
 ## Agda 上での HoareLogic(コマンド定義)
 * Env は while Program の変数である var n, i
 * **PrimComm** は代入時に使用される
 * **Cond** は Condition で Env を受け取って Boolean の値を返す
+```AGDA
-```AGDA
+record Env : Set where
-record Env : Set where
+field
-field
+varn : ℕ
-varn : ℕ
+vari : ℕ
-vari : ℕ
+PrimComm : Set
-PrimComm : Set
+PrimComm = Env → Env
-PrimComm = Env → Env
+Cond : Set
-Cond : Set
+Cond = (Env → Bool)
-Cond = (Env → Bool)
 ```
 ## Agda 上での HoareLogic(コマンド定義)
 * **Comm** は Agda のデータ型で定義した HoareLogic の Command
 * **Skip** は何も変更しない
 * **PComm** は変数を代入する
-* **Seq** は Command を次の Command に移す
+* **Seq** は Command を実行して次の Command に移す
 * **If** は Cond と2つの Comm を受け取り Cond の状態により実行する Comm を変える
 * **while** は Cond と Comm を受け取り Cond の中身が真である間 Comm を繰り返す
+```AGDA
-```AGDA
+data Comm : Set where
-data Comm : Set where
+Skip  : Comm
-Skip  : Comm
+Abort : Comm
-Abort : Comm
+PComm : PrimComm -> Comm
-PComm : PrimComm -> Comm
+Seq   : Comm -> Comm -> Comm
-Seq   : Comm -> Comm -> Comm
+If    : Cond -> Comm -> Comm -> Comm
-If    : Cond -> Comm -> Comm -> Comm
+While : Cond -> Comm -> Comm
-While : Cond -> Comm -> Comm
 ```
 ## Agda 上での HoareLogic(実際のプログラムの記述)
-* 先程の Comm を使ってwhile Program を記述した。
+* Command を使って while Program を記述した。
+* **$** は **()** の糖衣で行頭から行末までを ( ) で囲う
-```AGDA
+* 見やすさのため改行しているため 3~7 行はまとまっている
-program : Comm
+* Seq は Comm を2つ取って次の Comm に移行する
-program =
+```AGDA
-Seq ( PComm (λ env → record env {varn = 10}))
+program : Comm
-$ Seq ( PComm (λ env → record env {vari = 0}))
+program =
-$ While (λ env → lt zero (varn env ) )
+Seq ( PComm (λ env → record env {varn = 10}))
-(Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
+$ Seq ( PComm (λ env → record env {vari = 0}))
-$ PComm (λ env → record env {varn = ((varn env) - 1)} ))
+$ While (λ env → lt zero (varn env ) )
+(Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
+$ PComm (λ env → record env {varn = ((varn env) - 1)} ))
 ```
 ## Agda 上での HoareLogicの理解
-* 証明規則は HTProof にまとめられてる
+* 規則は HTProof にまとめられてる
-* **PrimRule** は代入を
+* **PrimRule** は **PComm** で行う代入を保証する
+* 3行目の pr の型 Axiom は PreCondition に PrimComm が適用されると PostCondition になることの記述
+* **_⇒_** は pre, post の Condition をとって post の Condition が成り立つときに True を返す関数
-```AGDA
+* SkipRule は PreCondition を変更しないことの保証
-data HTProof : Cond -> Comm -> Cond -> Set where
+* AbortRule は プログラムが停止するときのルール
-PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
+```AGDA
-(pr : Axiom bPre pcm bPost) ->
+data HTProof : Cond -> Comm -> Cond -> Set where
-HTProof bPre (PComm pcm) bPost
+PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
-SkipRule : (b : Cond) -> HTProof b Skip b
+(pr : Axiom bPre pcm bPost) ->
-AbortRule : (bPre : Cond) -> (bPost : Cond) ->
+HTProof bPre (PComm pcm) bPost
-HTProof bPre Abort bPost
+SkipRule : (b : Cond) -> HTProof b Skip b
+AbortRule : (bPre : Cond) -> (bPost : Cond) ->
+HTProof bPre Abort bPost
 -- 次のスライドに続く
 ```
+```AGDA
+Axiom : Cond -> PrimComm -> Cond -> Set
+Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true
+```
 ## Agda 上での HoareLogicの理解
+* **SeqRule** は Command を推移させる Seq の保証
+* **IfRule** は If の Command が正しく動くことを保証
+```AGDA
+-- HTProof の続き
+SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
+{cm2 : Comm} -> {bPost : Cond} ->
+HTProof bPre cm1 bMid ->
+HTProof bMid cm2 bPost ->
+HTProof bPre (Seq cm1 cm2) bPost
+IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
+{bPre : Cond} -> {bPost : Cond} ->
+{b : Cond} ->
+HTProof (bPre /\ b) cmThen bPost ->
+HTProof (bPre /\ neg b) cmElse bPost ->
+HTProof bPre (If b cmThen cmElse) bPost
+```
+## Agda 上での HoareLogicの理解
+* **WeakeningRule** は通常の Condition からループ不変条件(Loop Invaliant)に変換
+* Tautology は Condition と不変条件が等しく成り立つ
+* **WhileRule** はループ不変条件が成り立つ間 Comm を繰り返す
+```AGDA
+-- HTProof の続き
+WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
+{bPost' : Cond} -> {bPost : Cond} ->
+Tautology bPre bPre' ->
+HTProof bPre' cm bPost' ->
+Tautology bPost' bPost ->
+HTProof bPre cm bPost
+WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
+HTProof (bInv /\ b) cm bInv ->
+HTProof bInv (While b cm) (bInv /\ neg b)
+```
+```AGDA
+Tautology : Cond -> Cond -> Set
+Tautology pre post = ∀ (env : Env) →  (pre env) ⇒ (post env) ≡ true
+```
+## Agda 上での HoareLogic(証明)
+* **proof1** は while Program の証明
+* HTProof に 初期状態とコマンドで書かれた **program**  と終了状態を渡す
+* lemma1~5は rule それぞれの証明
 *
+```AGDA
-```AGDA
+proof1 : HTProof initCond program termCond
--- HTProof の続き
+proof1 =
-WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
+SeqRule {λ e → true} ( PrimRule empty-case )
-{bPost' : Cond} -> {bPost : Cond} ->
+$ SeqRule {λ e →  Equal (varn e) 10} ( PrimRule lemma1   )
-Tautology bPre bPre' ->
+$ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)}  lemma2 (
-HTProof bPre' cm bPost' ->
+WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
-Tautology bPost' bPost ->
+$ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
-HTProof bPre cm bPost
-SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
-{cm2 : Comm} -> {bPost : Cond} ->
-HTProof bPre cm1 bMid ->
-HTProof bMid cm2 bPost ->
-HTProof bPre (Seq cm1 cm2) bPost
-IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
-{bPre : Cond} -> {bPost : Cond} ->
-{b : Cond} ->
-HTProof (bPre /\ b) cmThen bPost ->
-HTProof (bPre /\ neg b) cmElse bPost ->
-HTProof bPre (If b cmThen cmElse) bPost
-WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
-HTProof (bInv /\ b) cm bInv ->
-HTProof bInv (While b cm) (bInv /\ neg b)
-```
-## Agda 上での HoareLogic(証明)
-```AGDA
-proof1 : HTProof initCond program termCond
-proof1 =
-SeqRule {λ e → true} ( PrimRule empty-case )
-$ SeqRule {λ e →  Equal (varn e) 10} ( PrimRule lemma1   )
-$ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)}  lemma2 (
-WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
-$ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
 $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
-```
+initCond : Cond
+initCond env = true
+termCond : {c10 : ℕ} → Cond
+termCond {c10} env = Equal (vari env) c10
+```
+<!-- program : Comm -->
+<!-- program =  -->
+<!--   Seq ( PComm (λ env → record env {varn = 10})) -->
+<!--   $ Seq ( PComm (λ env → record env {vari = 0})) -->
+<!--   $ While (λ env → lt zero (varn env ) ) -->
+<!--     (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -->
+<!--       $ PComm (λ env → record env {varn = ((varn env) - 1)} )) -->
+## 証明の一部
+- 基本的な証明方法は Condtition を変化させて次の Condition が成り立つように変形する
+- impl⇒
+```AGDA
+lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
+lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+begin
+(Equal (varn env) c10 ) ∧ true
+≡⟨ ∧true ⟩
+Equal (varn env) c10
+≡⟨ cond ⟩
+true
+∎ )
+```
+<!-- lemma2 :  {c10 : ℕ} → Tautology stmt2Cond whileInv -->
+<!-- lemma3 :   Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' -->
+<!-- lemma4 :  {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv -->
+<!-- lemma5 : {c10 : ℕ} →  Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond  -->
 ## Agda での Gears
 - Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数
 - CPS の関数は引数として継続を受け取って継続に計算結果を渡す
 - **名前 : 引数 -> (Code : fa -> t) -> t**
 - **t** は継続
 - **(Code : fa -> t)** は次の継続先
 - DataGear は Agda での CodeGear に使われる引数
+```AGDA
+_g-_ : {t : Set} → ℕ → ℕ → (Code : ℕ → t) → t
+x g- zero next = next x
+zero g- _  = next zero
+(suc x) g- (suc y)  = next (x g- y)
+```
 ## Gears をベースにした HoareLogic
 * 次に Gears をベースにした while Program をみる。
-* このプログラムは c10
+* このプログラムは自然数と継続先を受け取って t を返す
+```AGDA
-```AGDA
+{-# TERMINATING #-}
-whileTest : {l : Level} {t : Set l}  -> {c10 : ℕ } → (Code : (env : Env)  ->
+whileLoop : {l : Level} {t : Set l} -> Env -> (Code : Env -> t) -> t
-((vari env) ≡ 0) /\ ((varn env) ≡ c10) -> t) -> t
+whileLoop env next with lt 0 (varn env)
-whileTest {_} {_} {c10} next = next env proof2
+whileLoop env next | false = next env
-where
+whileLoop env next | true =
-env : Env
+whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
-env = record {vari = 0 ; varn = c10}
-proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
-proof2 = record {pi1 = refl ; pi2 = refl}
 ```
 ## Gears と HoareLogic をベースにした証明
 * ここでは
+```AGDA
-```AGDA
+proofGears : {c10 :  ℕ } → Set
-proofGears : {c10 : ℕ } → Set
+proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1
-proofGears {c10} = whileTest {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 ))))
+(λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 ))))
 ```
-<--!
+## まとめと今後の課題
-[論文目次]
+- HoareLogic の while を使った例題を作成、証明を行った
-まえがき
+- Gears を用いた HoareLogic ベースの検証方法を導入した
+- 証明が引数として渡される記述のため証明とプログラムを一体化できた
-現状
+- 今後の課題
+- RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで)
-Agda
-GearsOS
-CodeGear DataGear
-Gears と Agda
-Agda での HoareLogic
-Gears ベースの HoareLogic
-まとめと課題
--->

Mercurial > hg > Papers > 2019 > ryokka-sigss

comparison slide/slide.md @ 11:17b7605a5deb