# HG changeset patch # User ryokka # Date 1581355886 -32400 # Node ID e8655e0264b831ac5f5115c4582ae81f367eae61 # Parent bf3288c36d7e93f3a11a7460f92deb10cfd9b93a fix paper, slide diff -r bf3288c36d7e -r e8655e0264b8 paper/abstract.tex --- a/paper/abstract.tex Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/abstract.tex Tue Feb 11 02:31:26 2020 +0900 @@ -2,24 +2,24 @@ OS やアプリケーションの信頼性は重要である。 信頼性を上げるにはプログラムが仕様を満たしていることを検証する必要がある。 -プログラムの検証手法として、Floyd–Hoare logic (以下 Hoare Logic)が知られている。 +プログラムの検証手法として、Floyd–Hoare Logic (以下 Hoare Logic)が知られている。 Hoare Logic は事前条件が成り立っているときにある関数を実行して、それが停止する際に事後条件を満たすことを確認することで、検証を行う。 -Hoare Logic はシンプルなアプローチであるが限定されたコマンド群やwhile programにしか適用されないことが多く、 +Hoare Logic はシンプルなアプローチであるが限定されたコマンド群や while programにしか適用されないことが多く、 複雑な通常のプログラミング言語には向いていない。 当研究室では信頼性の高い言語として Continuation based C (CbC)を開発している。 CbC では CodeGear、DataGear という単位を用いてプログラムを記述する。 CodeGearを Agda で継続渡しの記述を用いた関数として記述する。ここで -AgdaはCurry Howard対応にもどつく定理証明系であり、それ自身が関数型プログラング言語でもある。 +Agda は Curry Howard 対応にもどつく定理証明系であり、それ自身が関数型プログラング言語でもある。 Agda では条件を命題として記述することができるので、 継続に事前条件や事後条件をもたせることができる。 -既存の言語では条件はassertなどで記述することになるが、その証明をそのプログラミング言語内で行うことはできない。 +既存の言語では条件は assert などで記述することになるが、その証明をそのプログラミング言語内で行うことはできない。 Agdaでは証明そのもの、つまり命題に対する推論をλ項として記述することができるので、 -Hoare Logicの証明そのものを Meta Code Gearとして記述できる。これは既存の言語では不可能であった。 -ポイントは、プログラムそのものを Agda baseのCode Gearで記述できることである。 -Code Gearは入力と出力のみを持ち関数呼び出しせずにgoto的に継続実行する。この形式がそのまま +Hoare Logicの証明そのものを Meta CodeGearとして記述できる。これは既存の言語では不可能であった。 +ポイントは、プログラムそのものを Agda baseのCodeGearで記述できることである。 +CodeGearは入力と出力のみを持ち関数呼び出しせずにgoto的に継続実行する。この形式がそのまま Hoare Logicのコマンドを自然に定義する。 Hoare Logicの証明には３つの条件が必要である。一つは @@ -40,8 +40,8 @@ OS and application reliability are important. To increase reliability, verifications of program with specifications are necessary. -Floyd-Hoare logic (hereafter Hoare Logic) is a welknown program verification method. -Hoare Logic verifies the postonditions of a function are satisfied when the postconditions are satifiles. +Floyd-Hoare logic (hereafter Hoare Logic) is a wellknown program verification method. +Hoare Logic verifies the postonditions of a function are satisfied when the postconditions are satisfied. It also checks the halt condition of the program. Hoare Logic is a useful simple approach but often only applies to a limited set of commands and while programs. It is not generaly suitable for complex ordinary programming languages. @@ -56,9 +56,9 @@ In existing languages, conditions are described in asserts, etc., but the proof cannot be done in that programming language. Since Agda can describe the proof itself, that is, the inference among the propositions, as λ terms, -The proof of Hoare Logic itself can be described as Meta Code Gear. This was not possible with existing languages. -The point is that the program itself can be described with Code Gear of Agda base. -Code Gear has only input and output, and executes continuously in a goto manner without calling a function. This format is +The proof of Hoare Logic itself can be described as Meta CodeGear. This was not possible with existing languages. +The point is that the program itself can be described with CodeGear of Agda base. +CodeGear has only input and output, and executes continuously in a goto manner without calling a function. This format is naturally define Hoare Logic commands. Hoare Logic's proof requires three conditions. One, diff -r bf3288c36d7e -r e8655e0264b8 paper/agda.tex --- a/paper/agda.tex Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/agda.tex Tue Feb 11 02:31:26 2020 +0900 @@ -41,6 +41,8 @@ 値にコンストラクタとその型を列挙する。 \coderef{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である。 +%%　Agda では $\mathbb{N}$ のような utf8 の文字を扱う事ができる。なんで？ +%% \lstinputlisting[label=agda-nat, caption=自然数を表すデータ型 Nat の定義] {src/nat.agda.replaced} @@ -102,12 +104,13 @@ \lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced} -\section{Agda の関数での停止性} -Agda では停止性の検出機能が存在し、プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る。 +また Agda では停止性の検出機能が存在し、プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る。 \verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない。 +\coderef{term} で書かれた、\verb/loop/ と \verb/stop/ は任意の自然数を受け取り、0になるまでループして0を返す関数である。 +\verb/loop/ では $\mathbb{N}$ の数を受け取り、 \verb/loop/ 自身を呼び出しながら 数を減らす関数 pred を呼んでいる。しかし、\verb/loop/の記述では関数が停止すると言えないため、定義するには\verb/{-# TERMINATING #-}/のタグが必要である。 +\verb/stop/ では自然数がパターンマッチで分けられ、\verb/zero/のときは \verb/zero/を返し、 \verb/suc n/ のときは \verb/suc/ を外した \verb/n/ で stop を実行するため停止する。 -ここでは停止する関数と停止しない関数の例\coderef{termination}を扱う。 -%% \lstinputlisting[label=termination, caption=停止する関数、停止しない関数] {src/terminating.agda.replaced} +\lstinputlisting[label=term, caption=停止しない関数 loop、停止する関数 stop] {src/termination.agda.replaced} このように再帰的な定義の関数が停止するときは、何らかの値が減少する必要がある。 @@ -118,8 +121,9 @@ ここでの \verb/+zero/ は右から \verb/zero/ を足しても $\equiv$ の両辺は等しいことを証明している。 これは、引数として受けている \verb/y/ が \verb/Nat/ なので、 \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある。 -\verb/y = zero/ の時は両辺が \verb/zero/ とできて、左右の項が等しいということを表す \verb/refl/ で証明することができる。 -\verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという \verb/cong/ を使って、y の値を 1 減らしたのちに再帰的に \verb/+zero y/ +\verb/y = zero/ の時は $zero \equiv zero$ とできて、左右の項が等しいということを表す \verb/refl/ で証明することができる。 +\verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという +\verb/cong/ を使って、y の値を 1 減らしたのち、再帰的に \verb/+zero y/ を用いて証明している。 \lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced} @@ -127,6 +131,9 @@ %% +zero : { y : ℕ } → y + zero ≡ y %% +zero {zero} = refl %% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) +%% +%% -- cong : ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y +%% -- cong f refl = refl %% \end{lstlisting} また、他にも $\lambda$ 項部分で等式を変形する構文がいくつか存在している。 diff -r bf3288c36d7e -r e8655e0264b8 paper/conclusion.tex --- a/paper/conclusion.tex Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/conclusion.tex Tue Feb 11 02:31:26 2020 +0900 @@ -32,13 +32,12 @@ また、Meta DataGear で DataGear の関係等の制約条件を扱うことで、 常に制約を満たすデータを作成することができる。 -予めそのようなデータをプログラムを使用することで、検証を行う際の記述が減ると思われる。 +予めそのようなデータをプログラムを使用することで、検証を行う際の記述減らすことができると考えている。 これも同様に Binary Tree や RedBlack Tree などのデータ構造に適用し、 検証の一助になると考えている。 その他の課題としては、 CbC で開発されている GearsOS に存在する並列構文の検証や、 +検証を行った Agda 上の CbC 記述から +ノーマルレベルの CbC プログラムの生成などが挙げられる。 -Agda の CbC 記述から -検証された CbC プログラムの生成などが挙げられる。 - diff -r bf3288c36d7e -r e8655e0264b8 paper/hoare.tex --- a/paper/hoare.tex Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/hoare.tex Tue Feb 11 02:31:26 2020 +0900 @@ -89,7 +89,7 @@ 比較しやすいように \coderef{c-while} を \coderef{c-while2} に再掲した。 -\begin{lstlisting}[caption= while Loop (再掲),label=c-while-2] +\begin{lstlisting}[caption= while Loop (再掲),label=c-while2] n = 10; i = 0; @@ -125,8 +125,13 @@ -- record { varn = 0 ; vari = 10 } \end{lstlisting} -\section{While Program の部分正当性} -ここでは先程記述した \coderef{agda-hoare-prog} の部分正当性の検証を行う。 +\section{while program の部分正当性} +ここでは先程記述した \coderef{agda-hoare-prog} の検証を行う。 +Hoare Logic ではコマンドに対応した仕様が存在しており、それらを組み合わせた形で +仕様を記述する必要がある。 +この仕様を記述する際、部分正当性が成り立っている必要がある。 +部分正当性とは Hoare Logic のコマンドが実行される前には事前条件が成り立っていて、 +コマンドが停止したとき事後条件が成り立っていることである。 \coderef{hoare-rule} の \verb/HTProof/ は Agda 上での Hoare Logic でのコマンドに対応した性質を型としてまとめたものである。 \verb/HTProof/ では Pre-Condition とコマンド、Post-Condition を受け取って定義される Agda のデータである。 @@ -152,8 +157,7 @@ \lstinputlisting[caption=Axiom と Tautology,label=axiom-taut]{src/axiom-taut.agda.replaced} - -\coderef{hoare-rule}を使って \coderef{c-while}の WhileProgram の仕様を構成する。 +\coderef{hoare-rule}を使って \coderef{c-while}の while program の仕様を構成する。 \lstinputlisting[caption=Agda での Hoare Locig の構成,label=hoare-rule]{src/agda-hoare-rule.agda.replaced} @@ -164,8 +168,9 @@ それぞれの Condition は Rule の後に記述されている \verb/{}/ に囲まれた部分で、 \verb/initCond/のみ無条件で \verb/true/ を返す Condition になっている。 -それぞれの Rule の中にそこで証明する必要のある補題が \verb/lemma/ で埋められている。 -\verb/lemma1/ から \verb/lemma5/ の証明は概要のみを示し、全体は付録に載せる。 +それぞれの Rule の中にそれぞれの部分正当性を検証するための証明存在しており、 +それぞれ \verb/lemma/ で埋められている。 +\verb/lemma1/ から \verb/lemma5/ の証明は概要のみを示し、全体は付録に載せることにする。 これらの lemma は HTProof の Rule に沿って必要なものを記述されており、 \verb/lemma1/ では PreCondition と PostCondition が存在するときの代入の保証、 @@ -174,7 +179,7 @@ \verb/lemma4/ では While Loop を抜けたときの Condition の整合性、 \verb/lemma5/ では While Loop を抜けた後のループ不変条件からCondition への変換と termCond への移行の整合性を保証している。 -\lstinputlisting[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]{src/agda-hoare-while.agda.replaced} +\lstinputlisting[caption=while loop の検証用記述,label=agda-hoare-while]{src/agda-hoare-while.agda.replaced} %% \begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while] %% proof1 : HTProof initCond program termCond %% proof1 = @@ -186,18 +191,17 @@ %% $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 %% \end{lstlisting} -proof1 は\coderef{agda-hoare-prog}の program と似た形をとっている。 -Hoare　Logic では Comannd に対応する証明規則があるため、仕様はプログラムに対応している。 +Hoare Logic ではコマンドに対応した仕様が存在するため、 \verb/proof1/ は\coderef{agda-hoare-prog}の program に近い記述になる。 \section{Hoare Logic での健全性} \coderef{agda-hoare-while} では Agda での Hoare Logic を用いた仕様の構成を行った。 -この仕様で実際に正しく動作するかどうか(健全性)を検証する必要がある。 +ここでは、\coderef{agda-hoare-while} で構成した仕様が +実際に正しく動作するかどうか(健全性)の検証を行う。 -\coderef{agda-hoare-satisfies} は Hoare Logic 上での部分正当性を確かめるための関数である。 - \verb/SemComm/ では Comm を受け取って成り立つ関係を返す。 - \verb/Satisfies/ では Pre Condition と コマンド、 Post Condition を受け取って、 - Pre Condition から Post Condition を正しく導けるという仕様を返す。 +\coderef{agda-hoare-satisfies} の \verb/SemComm/ では各 Comm で成り立つ関係を返す。 +\verb/Satisfies/ では 事前条件 と コマンド、 事後条件 を受け取って、 +これらが、正しく Comm で成り立つ関係を構築する。 \lstinputlisting[caption= State Sequence の部分正当性,label=agda-hoare-satisfies]{src/agda-hoare-satisfies.agda.replaced} @@ -229,7 +233,7 @@ %% SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2 %% \end{lstlisting} -これらの仕様を検証することでそれぞれの コマンド に対する部分正当性を示す。 +実行する際、これらの関係を満たしていることで健全性が証明できる。 \coderef{agda-hoare-soundness} の \verb/Soundness/ では \verb/HTProof/ を受け取り、 \verb/Satisfies/ に合った証明を返す。 \verb/Soundness/ では \verb/HTProof/ に記述されている Rule でパターンマッチを行い、対応する証明を適応している。 diff -r bf3288c36d7e -r e8655e0264b8 paper/master_paper.pdf Binary file paper/master_paper.pdf has changed diff -r bf3288c36d7e -r e8655e0264b8 paper/master_paper.tex --- a/paper/master_paper.tex Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/master_paper.tex Tue Feb 11 02:31:26 2020 +0900 @@ -19,6 +19,7 @@ \usepackage{type1cm} \usepackage[usenames]{color} \usepackage{ulem} +\usepackage{lstlinebgrd} \jtitle{Continuation based C での Hoare Logic を用いた仕様記述と検証} %% \etitle{Hoare Logic based Specification and Verification in Continuation based C} @@ -115,7 +116,6 @@ \input{agda.tex} \input{hoare.tex} \input{cbc_agda.tex} -%% \input{tree.tex} \input{cbc_hoare.tex} \input{conclusion.tex} diff -r bf3288c36d7e -r e8655e0264b8 paper/reference.bib --- a/paper/reference.bib Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/reference.bib Tue Feb 11 02:31:26 2020 +0900 @@ -116,7 +116,7 @@ @misc{agda-alpa-old, title = {Example - Hoare Logic}, howpublished = {\url{http://ocvs.cfv.jp/Agda/readmehoare.html}}, - note = {Accessed: 2020/2/9(Sun)}, + note = {Accessed: 2019/1/16(Wed)}, } @misc{agda-alpa, diff -r bf3288c36d7e -r e8655e0264b8 paper/src/RedBlackTree.agda.replaced --- a/paper/src/RedBlackTree.agda.replaced Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/src/RedBlackTree.agda.replaced Tue Feb 11 02:31:26 2020 +0900 @@ -51,7 +51,7 @@ -- -- put new node at parent node, and rebuild tree to the top -- -{-# TERMINATING #-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html +{-@$\#$@ TERMINATING @$\#$@-} -- https://agda.readthedocs.io/en/v2.5.3/language/termination-checking.html replaceNode : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t replaceNode {n} {m} {t} {a} {k} tree s n0 next = popSingleLinkedStack s ( \s parent @$\rightarrow$@ replaceNode1 s parent) @@ -97,7 +97,7 @@ ... | EQ = rotateNext tree s (Just n1) parent ... | _ = rotateNext tree s (Just n1) parent -{-# TERMINATING #-} +{-@$\#$@ TERMINATING @$\#$@-} insertCase5 : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Maybe (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ Node a k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t insertCase5 {n} {m} {t} {a} {k} tree s n0 parent grandParent next = pop2SingleLinkedStack s (\ s parent grandParent @$\rightarrow$@ insertCase51 tree s n0 parent grandParent next) where @@ -140,7 +140,7 @@ colorNode : {n : Level } {a k : Set n} @$\rightarrow$@ Node a k @$\rightarrow$@ Color @$\rightarrow$@ Node a k colorNode old c = record old { color = c } -{-# TERMINATING #-} +{-@$\#$@ TERMINATING @$\#$@-} insertNode : {n m : Level } {t : Set m } {a k : Set n} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ SingleLinkedStack (Node a k) @$\rightarrow$@ Node a k @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t insertNode {n} {m} {t} {a} {k} tree s n0 next = get2SingleLinkedStack s (insertCase1 n0) where diff -r bf3288c36d7e -r e8655e0264b8 paper/src/agda-hoare-interpret.agda.replaced --- a/paper/src/agda-hoare-interpret.agda.replaced Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/src/agda-hoare-interpret.agda.replaced Tue Feb 11 02:31:26 2020 +0900 @@ -1,4 +1,4 @@ -{-# TERMINATING #-} +{-@$\#$@ TERMINATING @$\#$@-} interpret : Env @$\rightarrow$@ Comm @$\rightarrow$@ Env interpret env Skip = env interpret env Abort = env diff -r bf3288c36d7e -r e8655e0264b8 paper/src/agda-hoare-rule.agda.replaced --- a/paper/src/agda-hoare-rule.agda.replaced Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/src/agda-hoare-rule.agda.replaced Tue Feb 11 02:31:26 2020 +0900 @@ -19,9 +19,9 @@ IfRule : {cmThen : Comm} @$\rightarrow$@ {cmElse : Comm} @$\rightarrow$@ {bPre : Cond} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@ {b : Cond} @$\rightarrow$@ - HTProof (bPre /\ b) cmThen bPost @$\rightarrow$@ - HTProof (bPre /\ neg b) cmElse bPost @$\rightarrow$@ + HTProof (bPre @$\wedge$@ b) cmThen bPost @$\rightarrow$@ + HTProof (bPre @$\wedge$@ neg b) cmElse bPost @$\rightarrow$@ HTProof bPre (If b cmThen cmElse) bPost WhileRule : {cm : Comm} @$\rightarrow$@ {bInv : Cond} @$\rightarrow$@ {b : Cond} @$\rightarrow$@ - HTProof (bInv /\ b) cm bInv @$\rightarrow$@ - HTProof bInv (While b cm) (bInv /\ neg b) + HTProof (bInv @$\wedge$@ b) cm bInv @$\rightarrow$@ + HTProof bInv (While b cm) (bInv @$\wedge$@ neg b) diff -r bf3288c36d7e -r e8655e0264b8 paper/src/agda-hoare-soundness.agda.replaced --- a/paper/src/agda-hoare-soundness.agda.replaced Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/src/agda-hoare-soundness.agda.replaced Tue Feb 11 02:31:26 2020 +0900 @@ -16,99 +16,51 @@ hyp1 = Soundness pr1 hyp2 : Satisfies bMid cm2 bPost hyp2 = Soundness pr2 - sMid : State - sMid = proj@$\_{1}$@ q2 - r1 : SemComm cm1 s1 sMid @$\times$@ SemComm cm2 sMid s2 - r1 = proj@$\_{2}$@ q2 - r2 : SemComm cm1 s1 sMid - r2 = proj@$\_{1}$@ r1 - r3 : SemComm cm2 sMid s2 - r3 = proj@$\_{2}$@ r1 - r4 : SemCond bMid sMid - r4 = hyp1 s1 sMid q1 r2 - in hyp2 sMid s2 r4 r3 + in hyp2 (proj@$\_{1}$@ q2) s2 (hyp1 s1 (proj@$\_{1}$@ q2) q1 (proj@$\_{1}$@ (proj@$\_{2}$@ q2))) (proj@$\_{2}$@ (proj@$\_{2}$@ q2)) Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse) s1 s2 q1 q2 - = let hypThen : Satisfies (bPre /\ b) cmThen bPost + = let hypThen : Satisfies (bPre @$\wedge$@ b) cmThen bPost hypThen = Soundness pThen - hypElse : Satisfies (bPre /\ neg b) cmElse bPost + hypElse : Satisfies (bPre @$\wedge$@ neg b) cmElse bPost hypElse = Soundness pElse - rThen : RelOpState.comp - (RelOpState.delta (SemCond b)) - (SemComm cmThen) s1 s2 @$\rightarrow$@ - SemCond bPost s2 - rThen = @$\lambda$@ h @$\rightarrow$@ - let t1 : SemCond b s1 @$\times$@ SemComm cmThen s1 s2 - t1 = (proj@$\_{2}$@ (RelOpState.deltaRestPre - (SemCond b) - (SemComm cmThen) s1 s2)) h - t2 : SemCond (bPre /\ b) s1 - t2 = (proj@$\_{2}$@ (respAnd bPre b s1)) - (q1 , proj@$\_{1}$@ t1) - in hypThen s1 s2 t2 (proj@$\_{2}$@ t1) - rElse : RelOpState.comp - (RelOpState.delta (NotP (SemCond b))) - (SemComm cmElse) s1 s2 @$\rightarrow$@ - SemCond bPost s2 + rThen : RelOpState.comp (RelOpState.delta (SemCond b)) + (SemComm cmThen) s1 s2 @$\rightarrow$@ SemCond bPost s2 + rThen = @$\lambda$@ h @$\rightarrow$@ hypThen s1 s2 ((proj@$\_{2}$@ (respAnd bPre b s1)) (q1 , proj@$\_{1}$@ t1)) + (proj@$\_{2}$@ ((proj@$\_{2}$@ (RelOpState.deltaRestPre (SemCond b) (SemComm cmThen) s1 s2)) h)) + rElse : RelOpState.comp (RelOpState.delta (NotP (SemCond b))) + (SemComm cmElse) s1 s2 @$\rightarrow$@ SemCond bPost s2 rElse = @$\lambda$@ h @$\rightarrow$@ - let t10 : (NotP (SemCond b) s1) @$\times$@ - (SemComm cmElse s1 s2) + let t10 : (NotP (SemCond b) s1) @$\times$@ (SemComm cmElse s1 s2) t10 = proj@$\_{2}$@ (RelOpState.deltaRestPre - (NotP (SemCond b)) (SemComm cmElse) s1 s2) - h - t6 : SemCond (neg b) s1 - t6 = proj@$\_{2}$@ (respNeg b s1) (proj@$\_{1}$@ t10) - t7 : SemComm cmElse s1 s2 - t7 = proj@$\_{2}$@ t10 - t8 : SemCond (bPre /\ neg b) s1 - t8 = proj@$\_{2}$@ (respAnd bPre (neg b) s1) - (q1 , t6) - in hypElse s1 s2 t8 t7 + (NotP (SemCond b)) (SemComm cmElse) s1 s2) h + in hypElse s1 s2 (proj@$\_{2}$@ (respAnd bPre (neg b) s1) + (q1 , (proj@$\_{2}$@ (respNeg b s1) (proj@$\_{1}$@ t10)))) (proj@$\_{2}$@ t10) in when rThen rElse q2 Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2 - = proj@$\_{2}$@ (respAnd bInv (neg b) s2) t20 + = proj@$\_{2}$@ (respAnd bInv (neg b) s2) + (lem1 (proj@$\_{1}$@ q2) s2 (proj@$\_{1}$@ t15) , proj@$\_{2}$@ (respNeg b s2) (proj@$\_{2}$@ t15)) where - hyp : Satisfies (bInv /\ b) cm' bInv + hyp : Satisfies (bInv @$\wedge$@ b) cm' bInv hyp = Soundness pr - n : $mathbb{N}$ - n = proj@$\_{1}$@ q2 - Rel1 : $mathbb{N}$ @$\rightarrow$@ Rel State (Level.zero) + Rel1 : @$\mathbb{N}$@ @$\rightarrow$@ Rel State (Level.zero) Rel1 = @$\lambda$@ m @$\rightarrow$@ RelOpState.repeat m (RelOpState.comp (RelOpState.delta (SemCond b)) (SemComm cm')) - t1 : RelOpState.comp - (Rel1 n) - (RelOpState.delta (NotP (SemCond b))) s1 s2 - t1 = proj@$\_{2}$@ q2 - t15 : (Rel1 n s1 s2) @$\times$@ (NotP (SemCond b) s2) + t15 : (Rel1 (proj@$\_{1}$@ q2) s1 s2) @$\times$@ (NotP (SemCond b) s2) t15 = proj@$\_{2}$@ (RelOpState.deltaRestPost - (NotP (SemCond b)) (Rel1 n) s1 s2) - t1 - t16 : Rel1 n s1 s2 - t16 = proj@$\_{1}$@ t15 - t17 : NotP (SemCond b) s2 - t17 = proj@$\_{2}$@ t15 - lem1 : (m : $mathbb{N}$) @$\rightarrow$@ (ss2 : State) @$\rightarrow$@ Rel1 m s1 ss2 @$\rightarrow$@ - SemCond bInv ss2 - lem1 $mathbb{N}$.zero ss2 h - = substId1 State (proj@$\_{2}$@ h) (SemCond bInv) q1 - lem1 ($mathbb{N}$.suc n) ss2 h - = let hyp2 : (z : State) @$\rightarrow$@ Rel1 n s1 z @$\rightarrow$@ + (NotP (SemCond b)) (Rel1 (proj@$\_{1}$@ q2)) s1 s2) (proj@$\_{2}$@ q2) + lem1 : (m : @$\mathbb{N}$@) @$\rightarrow$@ (ss2 : State) @$\rightarrow$@ Rel1 m s1 ss2 @$\rightarrow$@ SemCond bInv ss2 + lem1 zero ss2 h = substId1 State (proj@$\_{2}$@ h) (SemCond bInv) q1 + lem1 (suc n) ss2 h + = let hyp2 : (z : State) @$\rightarrow$@ Rel1 (proj@$\_{1}$@ q2) s1 z @$\rightarrow$@ SemCond bInv z hyp2 = lem1 n - s20 : State - s20 = proj@$\_{1}$@ h - t21 : Rel1 n s1 s20 - t21 = proj@$\_{1}$@ (proj@$\_{2}$@ h) - t22 : (SemCond b s20) @$\times$@ (SemComm cm' s20 ss2) - t22 = proj@$\_{2}$@ (RelOpState.deltaRestPre - (SemCond b) (SemComm cm') s20 ss2) + t22 : (SemCond b (proj@$\_{1}$@ h)) @$\times$@ (SemComm cm' (proj@$\_{1}$@ h) ss2) + t22 = proj@$\_{2}$@ (RelOpState.deltaRestPre (SemCond b) (SemComm cm') (proj@$\_{1}$@ h) ss2) (proj@$\_{2}$@ (proj@$\_{2}$@ h)) - t23 : SemCond (bInv /\ b) s20 - t23 = proj@$\_{2}$@ (respAnd bInv b s20) - (hyp2 s20 t21 , proj@$\_{1}$@ t22) - in hyp s20 ss2 t23 (proj@$\_{2}$@ t22) - t20 : SemCond bInv s2 @$\times$@ SemCond (neg b) s2 - t20 = lem1 n s2 t16 , proj@$\_{2}$@ (respNeg b s2) t17 + t23 : SemCond (bInv @$\wedge$@ b) (proj@$\_{1}$@ h) + t23 = proj@$\_{2}$@ (respAnd bInv b (proj@$\_{1}$@ h)) + (hyp2 (proj@$\_{1}$@ h) (proj@$\_{1}$@ (proj@$\_{2}$@ h)) , proj@$\_{1}$@ t22) + in hyp (proj@$\_{1}$@ h) ss2 t23 (proj@$\_{2}$@ t22) diff -r bf3288c36d7e -r e8655e0264b8 paper/src/agda-hoare-write.agda.replaced --- a/paper/src/agda-hoare-write.agda.replaced Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/src/agda-hoare-write.agda.replaced Tue Feb 11 02:31:26 2020 +0900 @@ -1,10 +1,14 @@ --- 通常の CodeGear -whileLoop' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t +-- Nomal CodeGear +whileLoop' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc) + @$\rightarrow$@ (n @$\equiv$@ varn env) + @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) + @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t whileLoop' zero env refl _ exit = exit env whileLoop' (suc n) env refl next _ = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) --- Hoare Logic ベースの CodeGear -whileLoopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ (pre : varn env + vari env @$\equiv$@ c10 env) +-- Hoare Logic base CodeGear +whileLoopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) + @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ (pre : varn env + vari env @$\equiv$@ c10 env) @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ (pred n @$\equiv$@ varn env) @$\rightarrow$@ (post : varn env + vari env @$\equiv$@ c10 env) @$\rightarrow$@ t) @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ (fin : vari env @$\equiv$@ c10 env) @$\rightarrow$@ t) @$\rightarrow$@ t whileLoopPwP' zero env refl refl next exit = exit env refl diff -r bf3288c36d7e -r e8655e0264b8 paper/src/agda-mcg.agda.replaced --- a/paper/src/agda-mcg.agda.replaced Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/src/agda-mcg.agda.replaced Tue Feb 11 02:31:26 2020 +0900 @@ -1,5 +1,5 @@ whileTestPwP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ - ((env : Envc ) @$\rightarrow$@ (mdg : (vari env @$\equiv$@ 0) /\ (varn env @$\equiv$@ c10 env)) @$\rightarrow$@ t) @$\rightarrow$@ t + ((env : Envc ) @$\rightarrow$@ (mdg : (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env)) @$\rightarrow$@ t) @$\rightarrow$@ t whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where env : Envc env = whileTestP c10 ( @$\lambda$@ env @$\rightarrow$@ env ) diff -r bf3288c36d7e -r e8655e0264b8 paper/src/agda-mdg.agda.replaced --- a/paper/src/agda-mdg.agda.replaced Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/src/agda-mdg.agda.replaced Tue Feb 11 02:31:26 2020 +0900 @@ -5,6 +5,6 @@ whileTestStateP : whileTestState @$\rightarrow$@ Envc @$\rightarrow$@ Set -whileTestStateP s1 env = (vari env @$\equiv$@ 0) /\ (varn env @$\equiv$@ c10 env) +whileTestStateP s1 env = (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) whileTestStateP s2 env = (varn env + vari env @$\equiv$@ c10 env) whileTestStateP sf env = (vari env @$\equiv$@ c10 env) diff -r bf3288c36d7e -r e8655e0264b8 paper/src/cbc-condition.agda.replaced --- a/paper/src/cbc-condition.agda.replaced Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/src/cbc-condition.agda.replaced Tue Feb 11 02:31:26 2020 +0900 @@ -4,6 +4,6 @@ sf : whileTestState whileTestStateP : whileTestState @$\rightarrow$@ Envc @$\rightarrow$@ Set -whileTestStateP s1 env = (vari env @$\equiv$@ 0) /\ (varn env @$\equiv$@ c10 env) +whileTestStateP s1 env = (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) whileTestStateP s2 env = (varn env + vari env @$\equiv$@ c10 env) whileTestStateP sf env = (vari env @$\equiv$@ c10 env) diff -r bf3288c36d7e -r e8655e0264b8 paper/src/gears-while.agda.replaced --- a/paper/src/gears-while.agda.replaced Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/src/gears-while.agda.replaced Tue Feb 11 02:31:26 2020 +0900 @@ -1,13 +1,13 @@ whileTest : {l : Level} {t : Set l} @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ (Code : (env : Env) @$\rightarrow$@ - ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t + ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t whileTest {_} {_} {c10} next = next env proof2 where env : Env env = record {vari = 0 ; varn = c10} - proof2 : ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10) + proof2 : ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10) proof2 = record {pi1 = refl ; pi2 = refl} -conversion1 : {l : Level} {t : Set l } @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10) +conversion1 : {l : Level} {t : Set l } @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((vari env) @$\equiv$@ 0) @$\wedge$@ ((varn env) @$\equiv$@ c10) @$\rightarrow$@ (Code : (env1 : Env) @$\rightarrow$@ (varn env1 + vari env1 @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t conversion1 env {c10} p1 next = next env proof4 where @@ -23,7 +23,7 @@ c10 @$\blacksquare$@ -{-# TERMINATING #-} +{-@$\#$@ TERMINATING @$\#$@-} whileLoop : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((varn env) + (vari env) @$\equiv$@ c10) @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t whileLoop env proof next with ( suc zero @$\leq$@? (varn env) ) whileLoop env proof next | no p = next env diff -r bf3288c36d7e -r e8655e0264b8 paper/src/zero.agda --- a/paper/src/zero.agda Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/src/zero.agda Tue Feb 11 02:31:26 2020 +0900 @@ -1,3 +1,6 @@ +zero : { y : ℕ } → y + zero ≡ y +zero {zero} = refl -+zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) ++zero {suc y} = cong suc ( +zero {y} ) + +-- cong : ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y +-- cong f refl = refl diff -r bf3288c36d7e -r e8655e0264b8 paper/src/zero.agda.replaced --- a/paper/src/zero.agda.replaced Mon Feb 10 17:26:24 2020 +0900 +++ b/paper/src/zero.agda.replaced Tue Feb 11 02:31:26 2020 +0900 @@ -1,3 +1,6 @@ +zero : { y : @$\mathbb{N}$@ } @$\rightarrow$@ y + zero @$\equiv$@ y +zero {zero} = refl -+zero {suc y} = cong ( @$\lambda$@ x @$\rightarrow$@ suc x ) ( +zero {y} ) ++zero {suc y} = cong suc ( +zero {y} ) + +-- cong : @$\forall$@ (f : A @$\rightarrow$@ B) {x y} @$\rightarrow$@ x @$\equiv$@ y @$\rightarrow$@ f x @$\equiv$@ f y +-- cong f refl = refl diff -r bf3288c36d7e -r e8655e0264b8 slide/slide.html --- a/slide/slide.html Mon Feb 10 17:26:24 2020 +0900 +++ b/slide/slide.html Tue Feb 11 02:31:26 2020 +0900 @@ -135,25 +135,6 @@
-

Gears について

- -

- - - - -
- -
-

Agda のデータ型