Mercurial > hg > Papers > 2020 > ryokka-master
changeset 19:046b2b20d6c7 default tip
fix
line wrap: on
line diff
--- a/paper/Makefile Mon Feb 17 17:14:00 2020 +0900 +++ b/paper/Makefile Mon Mar 09 11:25:49 2020 +0900 @@ -19,6 +19,7 @@ platex $(TARGET).tex $(BIBTEX) $(TARGET) platex $(TARGET).tex + platex $(TARGET).tex %.xbb: %.pdf $(BB) $<
--- a/paper/agda.tex Mon Feb 17 17:14:00 2020 +0900 +++ b/paper/agda.tex Mon Mar 09 11:25:49 2020 +0900 @@ -9,13 +9,15 @@ また、Agda での証明について説明する。 \section{関数型言語としての Agda} -Agda \cite{agda} は純粋関数型言語である。 -Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱う。 +Agda \cite{agda} は純粋な関数型の言語である。 -Agda の記述ではインデントが意味を持ち、スペースの有無もチェックされる。 -コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される。 -また、\verb/_/でそこに入りうるすべての値を示すことができ、 -\verb/?/でそこに入る値や型を不明瞭なままにしておくことができる。 +Agda では C 言語や Python 言語などの手続き型言語との違いがいくつか存在する。 +そのうちの一つとして、Agda では変数への再代入が許されていない事が挙げられる。 +また、for 文や if 文といった構文は用意されておらず、前者は再帰呼び出し、 +後者はパターンマッチと呼ばれる構文で記述されることが多い。 + +Agda では型が明示される必要があり、データのみではなく関数にも型を記述する必要がある。 +Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱うことができる。 Agda のプログラムは全てモジュール内部に記述される。 そのため、各ファイルのトップレベルにモジュールを定義する必要がある。 @@ -31,6 +33,12 @@ \lstinputlisting[label=agda-import, caption=モジュールのインポートとオプション] {src/AgdaImport.agda.replaced} +Agda の記述ではインデントが意味を持ち、スペースの有無もチェックされる。 + +コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される。 +また、\verb/_/でそこに入りうるすべての値を示すことができ、 +\verb/?/でそこに入る値や型を不明瞭なままにしておくことができる。 + \section{Agda のデータ} Agda 型をデータや関数に記述する必要がある。 @@ -55,9 +63,9 @@ %% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる。 Agda には C 言語における構造体に相当するレコード型というデータも存在する、 -例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する。\coderef{agda-record}のようになる。 +例えば \verb/vari/ と \verb/varn/、 \verb/c10/ の3つの自然数からなるレコード \verb/Envc/ を定義すると\coderef{agda-record}のようになる。 \lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/env.agda.replaced} -レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する。 +レコードを構築する際は \coderef{agda-record} の makeEnv のように \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する。 複数の値を列挙するには \verb/;/ で区切る必要がある。 @@ -73,7 +81,7 @@ %% 変数 \verb/x/ を取って true を返す関数 \verb/f/は\tabref{agda-function}のようになる。 例として任意の自然数$\mathbb{N}$を受け取り、\verb/+1/した値を返す関数は\coderef{agda-function}のように定義できる。 \lstinputlisting[label=agda-function, caption=Agda における関数定義] {src/agda-func.agda.replaced} - +この \verb/+1/ に\verb/+1 zero/ のように値を与えて評価すると、 \verb/suc zero/ が返ってくる。 引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。 @@ -84,15 +92,18 @@ パターンマッチでは全てのコンストラクタのパターンを含む必要がある。 例えば、自然数$\mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある。 -なお、コンストラクタをいくつか指定した後に変数で受けることもでき、その変数では指定されたもの以外を受けることができる。 -例えば\coderef{agda-pattern}の減算では初めのパターンで2つ目の引数が\verb/zero/のすべてのパターンが入る。 + +パターンマッチでは複数のパターンをまとめて受けることもできる。 +例えば\coderef{agda-pattern}の減算では初めのパターンで \verb/n/ として最初の引数を受け取っている。 +この場合は先頭の引数である \verb/n/ に入りうる \verb/zero/ または \verb/suc n/ の２つのパターンを同時に受け、 +２つ目の引数が \verb/zero/ であれば そのまま \verb/n/ を返している。 \lstinputlisting[label=agda-pattern, caption=自然数の減算によるパターンマッチの例] {src/agda-pattern.agda.replaced} -Agda には$\lambda$計算が存在している。$\lambda$計算とは関数内で生成できる無名の関数であり、 +Agda には$\lambda$計算が存在している。ここでの $\lambda$計算とは関数内で生成できる無名の関数であり、 \verb/\arg1 arg2 → function/ または $\lambda$\verb/arg1 arg2 → function/ のように書くことができる。 -\coderef{agda-function} で例とした \verb/+1/ をラムダ計算で書くと\coderef{agda-lambda}の\verb/$\lambda$+1/ように書くことができる。この二つの関数は同一の動作をする。 +\coderef{agda-function} で例とした \verb/+1/ をラムダ計算で書くと\coderef{agda-lambda}の\verb/$\lambda$+1/ように書くことができる。\verb/+1/ と \verb/$\lambda$+1/ は同様の動作をする。 \lstinputlisting[label=agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda.replaced} @@ -116,7 +127,7 @@ \section{定理証明支援器としての Agda} -Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。 +Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。これは Curry-Howard 対応\cite{10.5555/64805}に基づくものである。 証明の例として Code \coderef{proof} を見る。 ここでの \verb/+zero/ は右から \verb/zero/ を足しても $\equiv$ の両辺は等しいことを証明している。 これは、引数として受けている \verb/y/ が \verb/Nat/ なので、 \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある。 @@ -214,7 +225,7 @@ %% -- +-suc {zero} {y} = refl %% -- +-suc {suc x} {y} = cong suc (+-suc {x} {y}) %% \end{lstlisting} -Agda ではこのような形で等式を変形しながら証明を行う事ができる。 +Agda ではこのように等式を変形しながら証明を行う事ができる。 %% 例として先程の \verb/+-comm/ を rewrite で証明した \verb/rewrite-+-comm/ を \coderef{agda-rewrite} を載せる。
--- a/paper/cbc.tex Mon Feb 17 17:14:00 2020 +0900 +++ b/paper/cbc.tex Mon Mar 09 11:25:49 2020 +0900 @@ -52,9 +52,10 @@ \end{figure} -例として CodeGear が DataGear から値を取得する際に使われる Meta CodeGear である stub CodeGear について説明する。 +例として CodeGear が DataGear から値を取得する際に使われる、 stub CodeGear について説明する。 + CbC では CodeGear を実行する際、ノーマルレベルの計算からは見えないが必要な DataGear を Context と呼ばれる Meta DataGear を通して取得することになる。これはユーザーが直接データを扱える状態では信頼性が高いとは言えないと考えるからである。 -そのために、 Meta CodeGear を用いて Context から必要な DataGear を取り出し、 CodeGear に接続する stub CodeGear という Meta CodeGear が定義されている。 +そのために、 Meta CodeGear として Context から必要な DataGear を取り出し、 CodeGear に接続する stub CodeGear という Meta CodeGear を定義している。 Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。 例えば stub CodeGear では Context と呼ばれる接続可能な CodeGear、 DataGear のリストや、DataGear のメモリ空間等を持った Meta DataGear を扱っている。
--- a/paper/cbc_agda.tex Mon Feb 17 17:14:00 2020 +0900 +++ b/paper/cbc_agda.tex Mon Mar 09 11:25:49 2020 +0900 @@ -47,18 +47,6 @@ \verb/whileTestStateP/ でそれぞれの Meta DataGear を返している。 ここでは \verb/(vari env ≡ 0) /\ (varn env ≡ c10 env)/ などのデータを Meta DataGear として扱う。 -%% \coderef{agda-mdg} は大小関係を持った Tree 型データ構造の例である。 - -%% \lstinputlisting[label=agda-mdg, caption= Agda における Meta DataGear] {src/tree.agda.replaced} - -%% \verb/nomal-tree/ データ型では leaf か node で別れていて、 node には左右として\verb/nomal-tree/型を再帰的に保持している。この \verb/nomal-tree/ でデータの順序等を考える場合はデータを構築する関数側で成約を考えたプログラムを記述する必要がある。 - -%% \verb/meta-tree/では node が左右の \verb/meta-tree/ を持っているところまでは同じだが、 -%% node の場合に暗黙的な変数として \verb/l/ \verb/r/ という自然数を持っており、 -%% 成約として \verb/l/ $\leq$ \verb/key/、\verb/key/ $\leq$ \verb/r/ のデータの関係を受け取る。 - -%% 付帯した制約が守られなければエラーとなるため、より信頼性の高いデータとなる。 - Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear である。 Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返す CodeGear である。 @@ -73,30 +61,4 @@ この Meta CodeGear では次の CodeGear に mdg を渡しており、 CodeGear 内で Meta DataGear の性質が正しいことを検証して次の CodeGear に遷移することがわかる。 -Meta CodeGear はこのような形で記述される。 - - -%% \section{CbC 上での HoareLogic の実現} -%% CbC 上の Hoare Logic は引数として事前条件、次の CodeGear に渡す値に事後条件を含めることで記述する。 -%% その際に事前条件が CodeGear で変更され、事後条件を導く形になる。 -%% CbC 上でも While Program を実装し、Hoare Logic ベースの検証を行う。 -%% まずは、Condition について確認する。 -%% \coderef{cbc-condition} は While Program の Condition を記述したものである。 -%% \lstinputlisting[label=cbc-condition, caption= CbC ベースの Hoare Logic] {src/cbc-condition.agda.replaced} - -%% \verb/whileTestStateP/ では \verb/s1/ が初期状態、 \verb/s2/ がループ内不変条件、 \verb/fs/ が最終状態に対応している。 - -%% これらの Condition を用いて While Program の CbC 記述を行う。 - -%% \coderef{cbc-hoare} は while Program の CbC 記述である。 - -%% \lstinputlisting[label=cbc-hoare, caption= CbC ベースの Hoare Logic] {src/cbc-hoare.agda.replaced} - -%% \verb/whileTestPCallwP'/ が \coderef{} - -%% Hoare Logic の記述を行い、部分的な整合性を示すことができている。 -%% 全体の検証を行うためには接続されているすべての CodeGear が実行されたときの健全性(Soundness)が担保される必要がある。 -%% そのため、検証用の Meta CodeGear を記述する。 -%% 例として while プログラムの健全性を担保するプログラムをみる。 -%% %% コード -%% このコードでは CodeGear をつなげて終了状態まで実行したとき最後の事後条件が成り立っているため、これらの実行が正しく終了することを示すことができる。 +Meta CodeGear はMeta DataGear を含んだ形で記述される。
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/cbc_hoare.tex Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,234 @@ +\chapter{CbC と Hoare Logic} +\label{c:cbc_hoare} + +\secref{c:hoare} では Agda 上での Hoare Logic を用いて検証を行った。 +\secref{c:cbc_agda} では CbC の CodeGear、 DataGear という記述の Agda への対応を示し、CbC で書かれたプログラムが検証できることを確認した。 + +本章では CbC での CodeGear、 DataGear という記述と Hoare Logic を対応させ、Hoare Logic をベースとした CbC の検証手法を定義する。 +さらに Hoare Logic で例とした while program に対して同様に検証を行う。 + +\section{CbC での while program の記述} +検証を始める前に CbC 上で while program を実装する。 + +\ref{cbc-hoare-whileprog} は CbC 上での while progam に相当する CodeGear である。 +ここでは 変数 i、 n、入力として受ける c10 を record 型でまとめて \verb/Envc/ としている。 + +\lstinputlisting[label=cbc-hoare-whileprog, caption=CbC 上での while program] {src/agda-hoare-whileprog.agda.replaced} + +\verb/whileTestP/ は代入を行う CodeGear で、継続に構築した \verb/Env/ を渡している。 + +ループ部分はループの判断をする CodeGear と ループを行う CodeGear の２つに分けて記述している。 +\verb/whileLoopP'/ はループを判別する CodeGear で、varn の値が zero かそうでないかでループを終えるか続けるかを判断している。 +\verb/loopP/ はループを行う CodeGear で 継続先に \verb/whileLoopP/と更に \verb/whileLoopP/ の継続先に自身である \verb/loopP/を記述することでループさせている。 +このままでは停止しないため \verb/{-# TERMINATING #-}/ をつけている。 + +停止する記述は、\verb/loopP'/として \coderef{cbc-hoare-term}のように記述するとよい。 + +\lstinputlisting[label=cbc-hoare-term, caption=停止するループ loopP'] {src/agda-hoare-term.agda.replaced} + +\verb/whileTestPCall/ は実際に CodeGear を組み合わせたプログラムである。while program の \verb/n/ の値 10 を入れて\verb/whileTestPCall 10/のように実行すると、record { c10 = 10 ; varn = 0 ; vari = 10 }が帰ってくる。 +\verb/loopP'/ でも同様の実行ができる。 + + + +\section{CbC での Hoare Logic の記述} +Hoare Logic では事前条件、計算、事後条件があり、 +計算によって事前条件から事後条件を導くことで部分的な正当性を導くことができた。 +Hoare Logic の事前条件や事後条件は変数の大小関係や同値関係などで表される。 +Agda 上では関係もデータとして扱うことができるため、 +関係を引数とした CodeGear を用いてプログラムを記述することで HoareLogic と同様の構造にすることができる。 + +CbC での Hoare Logic は \figref{fig:hoare-cgdg} が示すように、 +事前条件(Pre Condition) が Proof で成立しており、 CodeGear で変更し、事後条件(Post Condition)が成り立つことを Proof で検証している。 + +\begin{figure}[htpb] + \begin{center} + \scalebox{0.2}{\includegraphics{fig/hoare_cg_dg.pdf}} + \end{center} + \caption{CodeGear、DataGear での Hoare Logic} + \label{fig:hoare-cgdg} +\end{figure} + + +\ref{cbc-hoare-write} は通常の CodeGear と Hoare Logic ベースの CodeGear を例としている。 +通常の CodeGear である \verb/whileLoop'/ と Hoare Logic ベースの CodeGear である \verb/whileLoopPwP'/ は同じ動作をする。 + +\lstinputlisting[label=cbc-hoare-write, caption=CbC 上での Hoare Logic, escapechar=@] {src/agda-hoare-write.agda.replaced} + +\verb/whileLoopPwP'/ では引数として事前条件 pre と継続先の関数を受け取っており、継続先の関数が受け取る引数 post や fin などの条件がこの関数においての事後条件となる。 + +また、Hoare Logic では HTProof というコマンドと対応した公理が存在していたが、 +CbC では各 CodeGear に対応した事前、事後条件を Meta DataGear とした Meta CodeGear を記述する必要がある。 + + +\section{CbC 上での Hoare Logic を用いた仕様記述} +\label{cbc-add-condition} +Hoare Logic では用意されたシンプルなコマンドを用いてプログラムを記述したが、 +CbC 上では CodeGear という単位でプログラムを記述する。 +そのため Hoare Logic のコマンドと同様に CodeGear を使った仕様記述を行う必要がある。 + +while program には初めの $n = 10$、 $i = 0$ を代入する条件、 +while loop 中に成り立っている条件を $n + i = 10$、 +while loop が終了したとき成り立っている条件を $i = 10$ +の3つの状態があった。 + +\coderef{cbc-condition} は while program の3つの状態を記述したものである。 +\lstinputlisting[label=cbc-condition, caption= CbC ベースの Hoare Logic] {src/cbc-condition.agda.replaced} +%% whileTestStateP : whileTestState → Envc → Set +%% whileTestStateP s1 env = (vari env ≡ 0) ∧ (varn env ≡ c10 env) +%% whileTestStateP s2 env = (varn env + vari env ≡ c10 env) +%% whileTestStateP sf env = (vari env ≡ c10 env) + +\verb/whileTestStateP/ では \verb/s1/ が初期状態、 \verb/s2/ がループ内不変条件、 \verb/fs/ が最終状態に対応している。 +\verb/s1/、 \verb/s2/、 \verb/s3/ は それぞれ \verb/whileTestState/ で定義された識別子である。 + +これらの状態を使って、CbC 上の Hoare Logic を使って while program を作成していく。 + +\coderef{cbc-hoare-prim} は代入部分の Meta CodeGear である。 +代入では事前条件がなく、事後条件として \verb/s1/ の \verb/(vari env ≡ 0) ∧ (varn env ≡ c10 env)/ が成り立つ。 +\lstinputlisting[label=cbc-hoare-prim, caption=CbC 上の Hoare Logic での 代入] {src/cbc-hoare-prim.agda.replaced} +%% whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t +%% whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where +%% env : Envc +%% env = whileTestP c10 ( λ env → env ) + +\coderef{cbc-hoare-loop} はループを行うコードである。 +\verb/whileLoopP'/はループを続ける、終えるの判断を行う Meta CodeGear で、ループを続けている間、 \verb/varn/ の値を減らし、 \verb/vari/ の値を増やしている。 +ループは \verb/varn/ が \verb/suc n/の間続き、その間の条件である\verb/s2/、つまり \verb/(varn env + vari env ≡ c10 env)/ の状態が成り立つ。 \verb/varn/ が \verb/zero/ になると最後の \verb/loopPwP'/ に \verb/fs/ である \verb/(vari env ≡ c10 env)/を渡し、ループを終える。 + +\verb/loopPwP'/ は実際にループをする Meta CodeGear で、回って来た際に \verb/varn/ が \verb/suc n/の間は \verb/whileLoopPwP'/ を実行し、その継続先の Meta CodeGear に自身である \verb/loopPwP'/を入れてループを行う。 +\verb/varn/ \verb/zero/のケースはその前の \verb/whileLoopPwP'/が \verb/zero/ で \verb/sf/ の最終状態を返してくるため、 \verb/loopPwP'/ でも同様に \verb/sf/ である \verb/(vari env ≡ c10 env)/ を返し、ループが終了する。 + +\lstinputlisting[label=cbc-hoare-loop, caption=CbC 上の Hoare Logic での while loop] {src/cbc-hoare-loop.agda.replaced} + + +これらの Meta CodeGear を使い仕様を記述する。 +\lstinputlisting[label=cbc-hoare-while, caption=CbC 上の Hoare Logic] {src/cbc-hoare-while.agda.replaced} +%% whileTestPCallwP' : (c : ℕ ) → Set +%% whileTestPCallwP' c = whileTestPwP {_} {_} c (λ env s → loopPwP' (varn env) env refl (conv env s) ( λ env s → vari env ≡ c10 env ) ) where +%% conv : (env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env +%% conv e record { pi1 = refl ; pi2 = refl } = +zero + + +\verb/whileTestPCallwP'/ は\coderef{cbc-hoare-prim}や\coderef{cbc-hoare-loop}で解説した Meta CodeGear を組み合わせた仕様である。 + +\verb/whileTestPwP/ では任意の自然数 \verb/c/ を受け取り、 +vari、 varn、 c10 の 3つの変数を保持する DataGear である env にそれぞれ代入を行い、 +env と env に意図した代入が行われていることを示す Meta DataGear \verb/s/ を次の関数に渡している。 +この Meta DataGear \verb/s/ は \verb/whileTestPwP/ の事後条件に当たる。 + +%% \verb/loopPwP'/ は\coderef{cbc-hoare-loop}で解説した \verb/whileTestPwP/ に変更された env と Condition である \verb/s/ を受け取り、ループする Meta CodeGear である。 +%% \verb/loopPwP'/ では無限ループを避けるためループに自然数の減少を絡め有限回で停止するよう工夫をした。 +%% また、while program と同様にループ内ではそのままの条件だとループさせることが難しいため \verb/conv/ を使ってループ内不変条件へと変化させている。 + +この仕様では \verb/whileTestPwP/ と \verb/loopPwP'/ を続けて実行したとき、最後のラムダ式に入っている最終状態 \verb/vari env ≡ c10 env/ が必ず成り立つ。 + +\verb/whileTestPCallwP'/ を検証するには、\coderef{whileTestCallwP} のように $\mathbb{N}$を受け取って \verb/whileTestPCallwP'/ $\mathbb{N}$ が成り立つ型を記述し、実際に導出部分で定義する必要がある。 +\coderef{whileTestCallwP} の \verb/{!!}/ は Agda の \verb/?/ と同義で中に入る値が不明な状態である。 + +\lstinputlisting[label=whileTestCallwP, caption=接続途中の CbC 上での CodeGear の条件接続] {src/cbc-hoare-soundness.agda.replaced} +%% whileCallwP : (c : ℕ) → whileTestPCallwP' c +%% whileCallwP c = whileTestPwP {_} {_} c +%% (λ env s → loopPwP' (c10 env) env (sym (pi2 s)) (conv env s) {!!}) + + +\verb/whileTestPwP/は代入のため単純に Agda が計算できる。しかし、 \verb/loopPwP'/ は実際の値が入るまで計算をすすめることができず、条件を接続することができなかった。 + +そのため\coderef{loophelper}で、 loop を簡約する補助定理 \verb/loopHelper/ を記述した。 + +\lstinputlisting[label=loophelper, caption=loopPwP'の補助定理 loopHelper] {src/cbc-hoare-loophelper.agda.replaced} +%% loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁)) +%% loopHelper zero env eq refl rewrite eq = refl +%% loopHelper (suc n) env eq refl rewrite eq = loopHelper n (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env)) + +\verb/loopHelper/ では \verb/loopPwP'/ が必ず停止し、 +\verb/vari env ≡ c10 env/ が成り立つことを証明している。 + +\verb/loopHelper/ を使い \verb/loopPwP/ のループでの停止性を示すことができたため、 \coderef{whileTestCallwP} のすべての条件が繋げられる。 + +\coderef{helperCallwP} は完成した CbC 上での Hoare Logic ベースの +\lstinputlisting[label=helperCallwP, caption=完成した CbC 上での CodeGear の条件接続] {src/cbc-hoare-helperCall.agda.replaced} + +これにより、すべての条件を接続した仕様である \coderef{helperCallwP} を構築できた。 + +\section{CbC 上での Hoare Logic を用いた検証の健全性} +本章では CbC 上の Hoare Logic での健全性を含めた検証する。 + +CbC 上での Hoare Logic の健全性では、 +仕様を含んだ Meta CodeGear が正しく接続できることと、 +各 CodeGear が事前条件から事後条件へ遷移することを満たしている必要がある。 + +また、各 CodeGear が正しく停止することも重要である。 + +\ref{cbc-add-condition} の \coderef{helperCallwP} では仕様が正しく接続でき、それぞれの CodeGear が停止することも分かっている。 + +ここでは CodeGear が正しく条件を遷移させることができることを示す必要がある。 + + + +健全性を含めた検証のために \verb/implies/ という data を導入する。 + +\coderef{implies} は \verb/implies/ の定義である。 +implies の型は A と B の条件を受け取り、 \verb/A implies B/ の形で型として記述する。 +このとき proof として \verb/A → B/ が存在すれば \verb/A implies B/ が証明でき、 +A から B へと正しく遷移できることが示せる。 + +\lstinputlisting[label=implies, caption=implies] {src/implies.agda.replaced} + %% data _implies_ (A B : Set ) : Set (succ Zero) where + %% proof : ( A → B ) → A implies B + +この \verb/implies/ を用いて while program で使用している CodeGear が事前条件から正しく事後条件に遷移することを証明する。 + +例として、代入を行う CodeGear である whileTestP の検証を行う。 +\coderef{whileTestPSemSound}は whileTestP の検証の CodeGear である。 +\verb/whileTestP/ を実行したときに、常に真の命題 $\top$ と代入を終えたときの事後条件にあたる +\verb/(vari env ≡ 0) ∧ (varn env ≡ c10 env)/ を implies に入れた型を記述している。 + +\lstinputlisting[label=whileTestPSemSound, caption=代入を行う whileTestP の健全性]{src/whileTestSemSound.agda.replaced} + +%% whileTestPSemSound : (c : ℕ ) (output : Envc ) +%% → output ≡ whileTestP c (λ e → e) +%% → ⊤ implies ((vari output ≡ 0) ∧ (varn output ≡ c)) +%% whileTestPSemSound c output refl = proof (λ _ → record { pi1 = refl ; pi2 = refl }) + + +証明では\verb/(/ $\top$ \verb/→ (vari env ≡ 0) ∧ (varn env ≡ c10 env) )/を示す必要があり、 +ここでは proof の引数に入っている \verb/(λ _ → record { pi1 = refl ; pi2 = refl })/ が対応する。 + +同様に他の CodeGear に対しても健全性の証明を行う。 + +\coderef{whileConvPSemSound}の whileConvPSemSound は制約を緩める conversion の健全性の証明である。 + +\lstinputlisting[label=whileConvPSemSound, caption=条件を変更する Conversion の健全性]{src/whileConvPSemSound.agda.replaced} +%% whileConvPSemSound : {l : Level} → (input : Envc) → ((vari input ≡ 0) ∧ (varn input ≡ c)) implies (varn input + vari input ≡ c10 input) +%% whileConvPSemSound input = proof λ x → (conversion input x) where +%% conversion : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env +%% conversion e record { pi1 = refl ; pi2 = refl } = +zero + +\coderef{whileLoopPSemSound}の whileLoopPSemSound は ループを行う CodeGear の 健全性の証明である。 + +\lstinputlisting[label=whileLoopPSemSound, caption= while loop をする loopPP の健全性]{src/whileLoopPSemSound.agda.replaced} +%% whileLoopPSemSound : {l : Level} → (input output : Envc ) +%% → (varn input + vari input ≡ c10 input) +%% → output ≡ loopPP (varn input) input refl +%% → (varn input + vari input ≡ c10 input) implies (vari output ≡ c10 output) +%% whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre + +\coderef{loopPPSemHelper}は loopPP の証明のための補助定理で、ループの判定を行う whileLoopPSem とループを行う loopPPSem に分かれている。 + +whileLoopPSem は行き先としてループの継続である next とループの終了を行う exit の２つの Meta CodeGear を持つ。 +whileLoopPSem では現在の \verb/Envc/ の値を確認し、それぞれの状態が正しく状態を遷移しているかを確認する。 + +loopPPSem は実際に while loop する Meta CodeGear で、 ループの終了である exit の Meta CodeGear しか持たない。 +これは loopPPSem では最終的にループが終了したときの遷移が示せれば良いためである。 + +loopPPSem は loopPPSemInduct という別の MetaCodeGear を使ってループをしており、 +このループが \verb/varn/ の値だけループを繰り返すことを記述しており、停止性を明示している。 + +\lstinputlisting[label=loopPPSemHelper, caption= loopPP を証明するための補助定理 loopPPSem と whileLoopPSem]{src/whileLoopPSem.agda.replaced} + +これで while program で使用されている CodeGear すべてが正しく遷移することを証明できた。 + +これらの CodeGear は仕様記述ですべての CodeGear と条件が接続できており、 +\verb/implies/ で証明した対応する遷移が正しいことから、 +CbC の Hoare Logic をベースとして書かれた while program は健全であると言える。
--- a/paper/conclusion.tex Mon Feb 17 17:14:00 2020 +0900 +++ b/paper/conclusion.tex Mon Mar 09 11:25:49 2020 +0900 @@ -2,33 +2,30 @@ \label{c:conclusion} 本論文では Continuation based C プログラムに対して -Hoare Logic をベースにした仕様記述と検証を行った。 -また、CbC での Hoare Logic では仕様を含めた記述のまま、 -実際にコードが実行できることを確認した。 +Hoare Logic をベースにした仕様記述を行った。 +また、 implies を用いて状態遷移を記述することで CbC 上での Hoare Logic の健全性を示すことができた。 実際に、 Hoare Logic ベースの記述を行うことで、 検証のメタ計算に使われる Meta DataGear や、 -CodeGear の概念が明確となった。 -また、 CbC 上での Pre Condition、 +CodeGear の概念、 CbC 上での Pre Condition、 Post Conditionの記述方法が明確になった。 -元の Hoare Logic ではコマンドのみでのプログラム記述と検証を行っていたが、 +また、検証時に任意の回数ループする Meta CodeGear が存在するとき、 +任意の自然数回ループしても正しく次の状態に遷移できることを証明することで、 +証明が記述できることが判明した。 + +さらに、本来の Hoare Logic では決められたコマンドのみでのプログラム記述と検証を行っていたが、 CodeGear をベースにすることでより柔軟な単位でのプログラム記述し、 実際に検証を行えることが分かった。 -以前は検証時に無限ループでなくてもループが存在すると、 Agda が導出時に step での実行を行うため、 -ループ回数分 step を実行する必要があったが、ループに対する簡約を記述することで、 -有限回のループを抜けて証明が記述できることが判明した。 -今後、ループ構造に対する証明は同様に解決できると考えられるため、 -より多くの証明が可能となると期待している。 \section{今後の課題} 今後の課題として、他のループが発生するプログラムの検証が挙げられる。 同様に検証が行えるのであれば、共通で使えるライブラリのような形でまとめることで、 より容易な検証ができるようになるのではないかと考えている。 + 現在、検証が行われていないループが存在するプログラムとして、 -Binary Tree や RedBlack Tree などのデータ構造が存在するため、 -それらのループに対して今回の手法を適用して検証を行いたい。 +Binary Tree や RedBlack Tree などのデータ構造が挙げられる。 また、Meta DataGear で DataGear の関係等の制約条件を扱うことで、 常に制約を満たすデータを作成することができる。 @@ -36,8 +33,17 @@ これも同様に Binary Tree や RedBlack Tree などのデータ構造に適用し、 検証の一助になると考えている。 -その他の課題としては、 -CbC で開発されている GearsOS に存在する並列構文の検証や、 -検証を行った Agda 上の CbC 記述から -ノーマルレベルの CbC プログラムの生成などが挙げられる。 + +CodeGear の健全性に関しては、 コマンドが限定されていた Hoare Logic とは異なり、 +\verb/implies/ を用いて CodeGear に対してそれぞれの遷移系を記述する必要がある。 +これらの遷移系は Meta CodeGear として記述できているため、仕様記述から変換できる形になることが期待できる。 + +現在の CbC では、検証の記述を Agda で記述しているため、実際の実行に向く記述ではない。 +そのため、検証を行った Agda 上の CbC 記述から Agda を用いて、 +より高速に実行できる CbC プログラムの生成を行う必要がある。 + +また、 CbC で開発、検証したいと考えている GearsOS には並列構文が存在しており、 +どのように並列動作に対しての検証も課題として挙げられる。 + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/escape_agda.rb Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,43 @@ +#!/usr/bin/env ruby +# coding: utf-8 + +Suffix = '.agda.replaced' +EscapeChar = '@' +FileName = ARGV.first + +ReplaceTable = { + '→' => 'rightarrow', + '->' => 'rightarrow', + '⊔' => 'sqcup', + '∷' => 'text{::}', + '∙' => 'circ', + '≡' => 'equiv', + '×' => 'times', + '⟨' => 'langle', + '⟩' => 'rangle', + 'ℕ' => 'mathbb{N}', + '₁' => '_{1}', + '₂' => '_{2}', + '∎' => 'blacksquare', + 'λ' => 'lambda', + '∧' => 'wedge', + '/\\' => 'wedge', + '⇒' => 'Rightarrow', + '¬' => 'neg', + '≤' => 'leq', + '⊥' => 'bot', + '∀' => 'forall', + '#' => '\#', + '⊤' => 'top', + '≈' => 'thickapprox', + '≟' => 'stackrel{?}{=}', +} + + +code = File.read(FileName) +ReplaceTable.each do |k, v| + escaped_str = EscapeChar + "$\\#{v}$" + EscapeChar + code = code.gsub(k, escaped_str) +end + +File.write(FileName.sub(/.agda$/, Suffix), code)
--- a/paper/hoare.tex Mon Feb 17 17:14:00 2020 +0900 +++ b/paper/hoare.tex Mon Mar 09 11:25:49 2020 +0900 @@ -5,22 +5,22 @@ Hoare Logic では事前条件が成り立つとき、何らかの計算(以下コマンド)を実行した後に 事後条件が成り立つことを検証する。 -事前条件を P 、 何らかの計算を C 、 事後条件を Q としたとき、 +事前条件を P 、 コマンドを C 、 事後条件を Q としたとき、 \[\{P\}\ C \ \{Q\}\] といった形で表される。 +この3つ組は Hoare Triple と呼ばれる。 -Hoare Logic ではプログラムの部分的な正当性を検証することができ、 -事後条件のあとに別のコマンドをつなげてプログラムを構築することで、 -プログラムに対する検証を行える。 +Hoare Triple の事後条件を受け取り異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。 - +Hoare Logic の検証では、「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。 +これらを満たし、事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。 本章は Agda で実装された Hoare Logic について解説し、 -実際に Hoare Logic を用いた検証を行う。 +Hoare Logic を用いた検証と健全性について説明する。 \section{Hoare Logic} -現在 Agda 上での Hoare Logic は初期の Agda\cite{agda-alpa} で実装されたものとそれを現在の Agda に対応させたもの \cite{agda2-hoare}が存在している。 +現在 Agda 上での Hoare Logic は初期の Agda \cite{agda-alpa} で実装されたものとそれを現在の Agda に対応させたもの \cite{agda2-hoare}が存在している。 ここでは現在 Agda に対応した Hoare Logic を使用する。 @@ -82,7 +82,6 @@ While : Cond -> Comm -> Comm \end{lstlisting} - Agda 上の Hoare Logic で使われるプログラムは \verb/Comm/ 型の関数となる。 プログラムはコマンド \verb/Comm/を \verb/Seq/ でつないでいき、最終的な状態にたどり着くと値を返して止まる。 @@ -111,36 +110,43 @@ %% (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) %% $ PComm (λ env → record env {varn = ((varn env) - 1)} )) %% \end{lstlisting} -この Comm を Agda 上で実行するため、 \coderef{agda-hoare-interpret} の \verb/interpret/ 関数を作成した。 +この program は Comm 型のデータで作られた構文木と考えられる。 + +この構文木を解釈し、 Agda 上で実行するには、 \coderef{agda-hoare-interpret} の \verb/interpret/ 関数を用いる。 \lstinputlisting[caption=Agda での Hoare Logic interpreter ,label=agda-hoare-interpret]{src/agda-hoare-interpret.agda.replaced} -\coderef{agda-hoare-interpret}は 初期状態の \verb/Env/ と 実行する コマンド の並びを受けとって、実行後の \verb/Env/ を返すものとなっている。 -\verb/interpret/ 関数は停止性を考慮していないため、 \verb/{-# TERMINATING #-}/ タグを付けている。 +\verb/interpret/は 初期状態の \verb/Env/ と 実行する コマンド の並びを受けとって、実行後の \verb/Env/ を返す関数である。 +この関数に初期の環境である \verb/Env/ と実行するコマンド \verb/Comm/ を渡すとコマンドに対応した処理を行い、実行後の環境が \verb/Env/ として返ってくる。 +Agda には Termnation Checker\cite{Abel98foetus} が付いており、停止性が明確でないとエラーを出す。 +\verb/interpret/ は明確に停止する条件がないため、 Agda でのコンパイル時にエラーが出る。 -\coderef{agda-hoare-run}のように \verb/interpret/ に \verb/vari = 0 , varn = 0/ の \verb/record/ を渡し、 実行する \verb/Comm/ を渡して 評価すると \verb/record { varn = 0 ; vari = 10 }/ のような \verb/Env/ が返ってくる。 -\verb/interpret/ で実行される コマンド は \coderef{agda-hoare-prog} で記述した While Loop するコマンドである +今回は停止条件を考えないために \verb/{-# TERMINATING #-}/ タグを付けることでエラーを抑制している。 +\coderef{agda-hoare-run}のように \verb/interpret/ に \verb/vari = 0 , varn = 10/ の \verb/record/ を渡し、\coderef{agda-hoare-prog} で記述した program を代入した。 \begin{lstlisting}[caption=Agda での Hoare Logic の実行 ,label=agda-hoare-run] test : Env -test = interpret ( record { vari = 0 ; varn = 0 } ) program --- record { varn = 0 ; vari = 10 } +test = interpret ( record { vari = 0 ; varn = 10 } ) program \end{lstlisting} -\section{while program の部分正当性} -ここでは先程記述した \coderef{agda-hoare-prog} の検証を行う。 +実際にこの \verb/test/ 関数の評価を行うと \verb/record {vari = 10 ; varn = 0 }/ の \verb/Env/ が値として返る。 +これにより、program として記述したコマンドベースのプログラムが Agda 上で実行できていることが分かる。 + + +\section{while program の仕様記述} +先程記述した \coderef{agda-hoare-prog} の \verb/program/ ではコマンドベースの実行のみで事前、事後条件が存在していなかった。 +ここではコマンドの事前、事後条件を接続した形で \verb/program/を記述していく。 +事前条件や事後条件が接続された Hoare Logic ではコマンドに対応した仕様が存在しており、それらを組み合わせた形で 仕様を記述する必要がある。 -この仕様を記述する際、部分正当性が成り立っている必要がある。 -部分正当性とは Hoare Logic のコマンドが実行される前には事前条件が成り立っていて、 -コマンドが停止したとき事後条件が成り立っていることである。 +この仕様を記述する際、事前の条件から必ず事後の条件が導かれている必要がある。 \coderef{hoare-rule} の \verb/HTProof/ は Agda 上での Hoare Logic でのコマンドに対応した性質を型としてまとめたものである。 -\verb/HTProof/ では Pre-Condition とコマンド、Post-Condition を受け取って定義される Agda のデータである。 +\verb/HTProof/ では 事前条件 とコマンド、事後条件 を受け取って定義される Agda のデータである。 \coderef{agda-hoare} のコマンドで定義された \verb/Skip/、 \verb/Abort/、 \verb/PComm/、 \verb/Seq/、\verb/If/、\verb/While/、に対応した証明のための命題が存在している。 -\verb/PrimRule/ は Pre-Condition と PrimComm、 Post-Condition、 +\verb/PrimRule/ は 事前条件 と PrimComm、 事後条件、 \coderef{axiom-taut} の \verb/Axiom/ を引数として \verb/PComm/の入った \verb/HTProof/ を返す。 \verb/SkipRule/ は Condition を受け取ってそのままの Condition を返す HTProof を返す。 @@ -165,17 +171,17 @@ 全体の仕様は Code \ref{agda-hoare-while}の \verb/proof1/ の様になる。 \verb/proof1/ では型で initCond、 Code \ref{agda-hoare-prog}のprogram、 termCond を記述しており、 -\verb/initCond/ から \verb/program/ を実行し \verb/termCond/ に行き着く Hoare Logic の証明になる。 +\verb/initCond/ から \verb/program/ を実行し \verb/termCond/ に行き着く Hoare Logic の仕様記述になる。 それぞれの Condition は Rule の後に記述されている \verb/{}/ に囲まれた部分で、 \verb/initCond/のみ無条件で \verb/true/ を返す Condition になっている。 -それぞれの Rule の中にそれぞれの部分正当性を検証するための証明存在しており、 +それぞれの Rule の中にそれぞれのを検証するための証明存在しており、 それぞれ \verb/lemma/ で埋められている。 -\verb/lemma1/ から \verb/lemma5/ の証明は概要のみを示し、全体は付録に載せることにする。 +\verb/lemma1/ から \verb/lemma5/ の証明は概要のみを示し、全体は付録\coderef{prim-proof}に載せることにする。 これらの lemma は HTProof の Rule に沿って必要なものを記述されており、 -\verb/lemma1/ では PreCondition と PostCondition が存在するときの代入の保証、 +\verb/lemma1/ では 事前条件が成り立つとき代入を行うと代入後の事後条件が成り立つ証明、 \verb/lemma2/ では While Loop に入る前の Condition からループ不変条件への変換の証明、 \verb/lemma3/ では While Loop 内での PComm の代入の証明、 \verb/lemma4/ では While Loop を抜けたときの Condition の整合性、 @@ -196,14 +202,21 @@ Hoare Logic ではコマンドに対応した仕様が存在するため、 \verb/proof1/ は\coderef{agda-hoare-prog}の program に近い記述になる。 -\section{Hoare Logic での健全性} +\section{Hoare Logic の健全性} \coderef{agda-hoare-while} では Agda での Hoare Logic を用いた仕様の構成を行った。 -ここでは、\coderef{agda-hoare-while} で構成した仕様が -実際に正しく動作するかどうか(健全性)の検証を行う。 +ここでは、\coderef{agda-hoare-while} で構成した仕様が健全であるか検証する。 + +ここでの健全性はコマンドの仕様である HTProof がすべてつながっていて、 +事前条件が成り立っているとき、コマンドが停止すると事後条件が成り立つことと、 +コマンドは条件を意図した通りに遷移させることができることの両方を検証することで、 +その両方が検証できたとき、この実行は正しいというものである。 \coderef{agda-hoare-satisfies} の \verb/SemComm/ では各 Comm で成り立つ関係を返す。 +Hoare Logic のすべてのコマンドの事前条件から事後条件への遷移が記述されており、 \verb/Satisfies/ では 事前条件 と コマンド、 事後条件 を受け取って、 -これらが、正しく Comm で成り立つ関係を構築する。 +\verb/Comm/ がでの実行が \verb/SemComm/ を満たすことを示している。 + +詳しい記述は、現在の Agda に直した Hoare Logic の定義\cite{agda2-hoare} の RelOp.agda に記述されている。 \lstinputlisting[caption= State Sequence の部分正当性,label=agda-hoare-satisfies]{src/agda-hoare-satisfies.agda.replaced} @@ -235,11 +248,11 @@ %% 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 でパターンマッチを行い、対応する証明を適応している。 -\verb/Soundness/ のコードは量が多いため部分的に省略し、全文は付録に載せることにする。 +\verb/Soundness/ のコードは量が多いため部分的に省略し、全文は現在の Agda に直した Hoare Logic の定義\cite{agda2-hoare} の Soundness.agda を確認してほしい。 \lstinputlisting[caption=Agda での Hoare Logic の健全性,label=agda-hoare-soundness]{src/agda-hoare-soundness.agda.replaced} @@ -253,7 +266,6 @@ PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht \end{lstlisting} - \coderef{agda-hoare-prim-proof} では \coderef{agda-hoare-prog} の \verb/program/ の Hoare Logic での命題である。 この証明では初期状態\verb/initCond/と実行するコマンド群\verb/program/を受け取り終了状態として \verb/termCond/ が \verb/true/ であることを示す。 @@ -265,5 +277,6 @@ proofOfProgram c10 input output ic sem = PrimSoundness (proof1 c10) input output ic sem \end{lstlisting} -この証明は実際に構築した仕様である \verb/proof1/ を \verb/\verb/PrimSoundness/ に入力として渡すことで満たすことができる。 -ここまで記述することで Agda 上の Hoare Logic を用いた \verb/while program/ を検証することができた。 +この証明は実際に構築した仕様である \verb/proof1/ を \verb/PrimSoundness/ に入力として渡すことで満たすことができる。 +\coderef{agda-hoare-prim-proof} で、 Agda 上の Hoare Logic を用いた \verb/while program/ を検証することができた。 +ここで書かれた健全性の検証の全体は付録の\coderef{prim-proof} に載せる。
--- a/paper/introduction.tex Mon Feb 17 17:14:00 2020 +0900 +++ b/paper/introduction.tex Mon Mar 09 11:25:49 2020 +0900 @@ -1,4 +1,3 @@ -% sigos のやつ \chapter{プログラミング言語の検証} \label{chapter:intro} 現在の OS やアプリケーションの検証では、実装と別に検証用の言語で記述された実装と証明を持つのが一般的である。 @@ -7,7 +6,7 @@ また、別のアプローチとして ATS2\cite{ats2} や Rust\cite{rust} などの低レベル記述向けの言語を 実装に用いる手法が存在している。 -証明支援向けのプログラミング言語としては Agda\cite{agda}、 Coq\cite{coq} などが存在しているが、 +定理証明支援向けのプログラミング言語としては Agda\cite{agda}、 Coq\cite{coq} などが存在しているが、 これらの言語自体は実行速度が期待できるものではない。 そこで、当研究室では検証と実装が同一の言語で行う Continuation based C\cite{kaito-lola} (CbC) という言語を開発している。 @@ -18,14 +17,3 @@ 本研究では Agda 上で CodeGear、DataGear という単位を用いてプログラムを記述し、 メタ計算部分で Hoare Logic を元にした検証を行った。 - - -%現代の OS では拡張性と信頼性を両立させることが要求されている。 -%時代と主に進歩するハードウェア、サービスに対して OS 自体が拡張される必要がある。 -%しかし、OSには非決定的な実行を持っており、その信頼性を保証するには従来のテストとデバッグでは不十分であり、テスト仕切れない部分が残ってしまう。 -%これに対処するために証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。 -% 証明やモデル検査を用いて OS の検証する方法は様々なものが検討されている。 -% 型付きアセンブラ\cite{Yang:2010:SLI:1806596.1806610} -% 従来の研究ではPython\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} や Haskell\cite{Chen:2015:UCH:2815400.2815402}\cite{Klein:2009:SFV:1629575.1629596}による記述した OS を検証する研究も存在する。 -% また SPIN などのモデル検査を OS の検証に用いた例もである。 -% 本研究室では信頼性をノーマルレベルの掲載に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を開発している。
--- a/paper/master_paper.tex Mon Feb 17 17:14:00 2020 +0900 +++ b/paper/master_paper.tex Mon Mar 09 11:25:49 2020 +0900 @@ -7,7 +7,10 @@ \usepackage{listings} \usepackage{comment} \usepackage{url} +%% \usepackage{otf} \usepackage[deluxe, multi]{otf} +%% \usepackage{redeffont} + %% \usepackage{cite} %% \usepackage{listings} \usepackage{amssymb} @@ -131,5 +134,6 @@ %付録 \addcontentsline{toc}{chapter}{付録} \appendix +\input{sources.tex} \end{document}
--- a/paper/reference.bib Mon Feb 17 17:14:00 2020 +0900 +++ b/paper/reference.bib Mon Mar 09 11:25:49 2020 +0900 @@ -15,7 +15,15 @@ address = {New York, NY, USA}, keywords = {dependent types, programming}, } - + +@book{10.5555/64805, +author = {Girard, Jean-Yves and Taylor, Paul and Lafont, Yves}, +title = {Proofs and Types}, +year = {1989}, +isbn = {0521371813}, +publisher = {Cambridge University Press}, +address = {USA} +} @article{atton-ipsj, author="比嘉 健太 and 河野 真治", @@ -91,7 +99,7 @@ isbn = {978-1-97000-127-3}, publisher = {Association for Computing Machinery and Morgan \&\#38; Claypool}, address = {New York, NY, USA}, -} +} @article{10.1145/363235.363259, author = {Hoare, C. A. R.}, @@ -121,7 +129,7 @@ @misc{agda-alpa, title = {Agda1}, - howpublished = {\url{https://sourceforge.net/projects/agda/}}, + howpublished = {\url{https://sourceforge.net/projects/agda}}, note = {Accessed: 2020/2/9(Sun)}, } @@ -133,8 +141,8 @@ @misc{coq-old, title = {Welcome! | The Coq Proof Assistant}, - howpublished = {\url{https://coq.inria.fr/}}, - note = {Accessed: 2020/2/9(Sun)}, + howpublished = {\url{https://coq.inria.fr}}, + note = {Accessed: 2019/1/16(Wed)}, } @@ -193,10 +201,18 @@ publisher = {ACM}, address = {New York, NY, USA}, } + + +@misc{Abel98foetus, + author = {Andreas Abel}, + title = {foetus – Termination Checker for Simple Functional Programs }, + year = {1998} +} + @misc{cr-ryukyu, - title = {whileTestPrim.agda - 並列信頼研 mercurial repository}, - howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/file/tip/whileTestPrim.agda}}, + title = {Hoare Logic - 並列信頼研 mercurial repository}, + howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/}}, note = {Accessed: 2020/2/9(Sun)} } @@ -261,3 +277,14 @@ note = {Accessed: 2020/2/9(Sun)} } + +@article{村井-哲也1995KJ00002088318, + title={様相論理1}, + author={村井 哲也 and 深海 悟}, + journal={日本ファジィ学会誌}, + volume={7}, + number={1}, + pages={3-18}, + year={1995}, + doi={10.3156/jfuzzy.7.1_3} +} \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/Hoare.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,79 @@ +module Hoare + (PrimComm : Set) + (Cond : Set) + (Axiom : Cond -> PrimComm -> Cond -> Set) + (Tautology : Cond -> Cond -> Set) + (_and_ : Cond -> Cond -> Cond) + (neg : Cond -> Cond ) + where + +data Comm : Set where + Skip : Comm + Abort : Comm + PComm : PrimComm -> Comm + Seq : Comm -> Comm -> Comm + If : Cond -> Comm -> Comm -> Comm + While : Cond -> Comm -> Comm + +-- Hoare Triple +data HT : Set where + ht : Cond -> Comm -> Cond -> HT + +{- + prPre pr prPost + ------------- ------------------ ---------------- + bPre => bPre' {bPre'} c {bPost'} bPost' => bPost +Weakening : ---------------------------------------------------- + {bPre} c {bPost} + +Assign: ---------------------------- + {bPost[v<-e]} v:=e {bPost} + + pr1 pr2 + ----------------- ------------------ + {bPre} cm1 {bMid} {bMid} cm2 {bPost} +Seq: --------------------------------------- + {bPre} cm1 ; cm2 {bPost} + + pr1 pr2 + ----------------------- --------------------------- + {bPre /\ c} cm1 {bPost} {bPre /\ neg c} cm2 {bPost} +If: ------------------------------------------------------ + {bPre} If c then cm1 else cm2 fi {bPost} + + pr + ------------------- + {inv /\ c} cm {inv} +While: --------------------------------------- + {inv} while c do cm od {inv /\ neg c} +-} + + +data HTProof : Cond -> Comm -> Cond -> Set where + PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} -> + (pr : Axiom bPre pcm bPost) -> + HTProof bPre (PComm pcm) bPost + SkipRule : (b : Cond) -> HTProof b Skip b + AbortRule : (bPre : Cond) -> (bPost : Cond) -> + HTProof bPre Abort bPost + 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 + 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 and b) cmThen bPost -> + HTProof (bPre and neg b) cmElse bPost -> + HTProof bPre (If b cmThen cmElse) bPost + WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> + HTProof (bInv and b) cm bInv -> + HTProof bInv (While b cm) (bInv and neg b) +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/Hoare.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,79 @@ +module Hoare + (PrimComm : Set) + (Cond : Set) + (Axiom : Cond @$\rightarrow$@ PrimComm @$\rightarrow$@ Cond @$\rightarrow$@ Set) + (Tautology : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Set) + (_and_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond) + (neg : Cond @$\rightarrow$@ Cond ) + where + +data Comm : Set where + Skip : Comm + Abort : Comm + PComm : PrimComm @$\rightarrow$@ Comm + Seq : Comm @$\rightarrow$@ Comm @$\rightarrow$@ Comm + If : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Comm @$\rightarrow$@ Comm + While : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Comm + +-- Hoare Triple +data HT : Set where + ht : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Cond @$\rightarrow$@ HT + +{- + prPre pr prPost + ------------- ------------------ ---------------- + bPre => bPre' {bPre'} c {bPost'} bPost' => bPost +Weakening : ---------------------------------------------------- + {bPre} c {bPost} + +Assign: ---------------------------- + {bPost[v<-e]} v:=e {bPost} + + pr1 pr2 + ----------------- ------------------ + {bPre} cm1 {bMid} {bMid} cm2 {bPost} +Seq: --------------------------------------- + {bPre} cm1 ; cm2 {bPost} + + pr1 pr2 + ----------------------- --------------------------- + {bPre @$\wedge$@ c} cm1 {bPost} {bPre @$\wedge$@ neg c} cm2 {bPost} +If: ------------------------------------------------------ + {bPre} If c then cm1 else cm2 fi {bPost} + + pr + ------------------- + {inv @$\wedge$@ c} cm {inv} +While: --------------------------------------- + {inv} while c do cm od {inv @$\wedge$@ neg c} +-} + + +data HTProof : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Cond @$\rightarrow$@ Set where + PrimRule : {bPre : Cond} @$\rightarrow$@ {pcm : PrimComm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@ + (pr : Axiom bPre pcm bPost) @$\rightarrow$@ + HTProof bPre (PComm pcm) bPost + SkipRule : (b : Cond) @$\rightarrow$@ HTProof b Skip b + AbortRule : (bPre : Cond) @$\rightarrow$@ (bPost : Cond) @$\rightarrow$@ + HTProof bPre Abort bPost + WeakeningRule : {bPre : Cond} @$\rightarrow$@ {bPre' : Cond} @$\rightarrow$@ {cm : Comm} @$\rightarrow$@ + {bPost' : Cond} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@ + Tautology bPre bPre' @$\rightarrow$@ + HTProof bPre' cm bPost' @$\rightarrow$@ + Tautology bPost' bPost @$\rightarrow$@ + HTProof bPre cm bPost + SeqRule : {bPre : Cond} @$\rightarrow$@ {cm1 : Comm} @$\rightarrow$@ {bMid : Cond} @$\rightarrow$@ + {cm2 : Comm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@ + HTProof bPre cm1 bMid @$\rightarrow$@ + HTProof bMid cm2 bPost @$\rightarrow$@ + HTProof bPre (Seq cm1 cm2) bPost + IfRule : {cmThen : Comm} @$\rightarrow$@ {cmElse : Comm} @$\rightarrow$@ + {bPre : Cond} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@ + {b : Cond} @$\rightarrow$@ + HTProof (bPre and b) cmThen bPost @$\rightarrow$@ + HTProof (bPre and neg b) cmElse bPost @$\rightarrow$@ + HTProof bPre (If b cmThen cmElse) bPost + WhileRule : {cm : Comm} @$\rightarrow$@ {bInv : Cond} @$\rightarrow$@ {b : Cond} @$\rightarrow$@ + HTProof (bInv and b) cm bInv @$\rightarrow$@ + HTProof bInv (While b cm) (bInv and neg b) +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/HoareSoundness.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,197 @@ +{-# OPTIONS --universe-polymorphism #-} + +open import Level +open import Data.Nat.Base +open import Data.Product +open import Data.Bool.Base +open import Data.Empty +open import Data.Sum +open import Relation.Binary +open import Relation.Nullary +open import Relation.Binary.Core +open import Relation.Binary.PropositionalEquality +open import RelOp +open import utilities + +module HoareSoundness + (Cond : Set) + (PrimComm : Set) + (neg : Cond -> Cond) + (_/\_ : Cond -> Cond -> Cond) + (Tautology : Cond -> Cond -> Set) + (State : Set) + (SemCond : Cond -> State -> Set) + (tautValid : (b1 b2 : Cond) -> Tautology b1 b2 -> + (s : State) -> SemCond b1 s -> SemCond b2 s) + (respNeg : (b : Cond) -> (s : State) -> + Iff (SemCond (neg b) s) (¬ SemCond b s)) + (respAnd : (b1 b2 : Cond) -> (s : State) -> + Iff (SemCond (b1 /\ b2) s) + ((SemCond b1 s) × (SemCond b2 s))) + (PrimSemComm : ∀ {l} -> PrimComm -> Rel State l) + (Axiom : Cond -> PrimComm -> Cond -> Set) + (axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) -> + (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) -> + SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2) where + +open import Hoare PrimComm Cond Axiom Tautology _/\_ neg + +open import RelOp +module RelOpState = RelOp State + +NotP : {S : Set} -> Pred S -> Pred S +NotP X s = ¬ X s + +_\/_ : Cond -> Cond -> Cond +b1 \/ b2 = neg (neg b1 /\ neg b2) + +when : {X Y Z : Set} -> (X -> Z) -> (Y -> Z) -> + X ⊎ Y -> Z +when f g (inj₁ x) = f x +when f g (inj₂ y) = g y + +-- semantics of commands +SemComm : Comm -> Rel State (Level.zero) +SemComm Skip = RelOpState.deltaGlob +SemComm Abort = RelOpState.emptyRel +SemComm (PComm pc) = PrimSemComm pc +SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2) +SemComm (If b c1 c2) + = RelOpState.union + (RelOpState.comp (RelOpState.delta (SemCond b)) + (SemComm c1)) + (RelOpState.comp (RelOpState.delta (NotP (SemCond b))) + (SemComm c2)) +SemComm (While b c) + = RelOpState.unionInf + (λ (n : ℕ) -> + RelOpState.comp (RelOpState.repeat + n + (RelOpState.comp + (RelOpState.delta (SemCond b)) + (SemComm c))) + (RelOpState.delta (NotP (SemCond b)))) + +Satisfies : Cond -> Comm -> Cond -> Set +Satisfies bPre cm bPost + = (s1 : State) -> (s2 : State) -> + SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2 + +Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> + HTProof bPre cm bPost -> Satisfies bPre cm bPost +Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2 + = axiomValid bPre cm bPost pr s1 s2 q1 q2 +Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2 + = substId1 State {Level.zero} {State} {s1} {s2} (proj₂ q2) (SemCond bPost) q1 +Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 () +Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost) + s1 s2 q1 q2 + = let hyp : Satisfies bPre' cm bPost' + hyp = Soundness pr + r1 : SemCond bPre' s1 + r1 = tautValid bPre bPre' tautPre s1 q1 + r2 : SemCond bPost' s2 + r2 = hyp s1 s2 r1 q2 + in tautValid bPost' bPost tautPost s2 r2 +Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2) + s1 s2 q1 q2 + = let hyp1 : Satisfies bPre cm1 bMid + hyp1 = Soundness pr1 + hyp2 : Satisfies bMid cm2 bPost + hyp2 = Soundness pr2 + sMid : State + sMid = proj₁ q2 + r1 : SemComm cm1 s1 sMid × SemComm cm2 sMid s2 + r1 = proj₂ q2 + r2 : SemComm cm1 s1 sMid + r2 = proj₁ r1 + r3 : SemComm cm2 sMid s2 + r3 = proj₂ r1 + r4 : SemCond bMid sMid + r4 = hyp1 s1 sMid q1 r2 + in hyp2 sMid s2 r4 r3 +Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse) + s1 s2 q1 q2 + = let hypThen : Satisfies (bPre /\ b) cmThen bPost + hypThen = Soundness pThen + hypElse : Satisfies (bPre /\ neg b) cmElse bPost + hypElse = Soundness pElse + rThen : RelOpState.comp + (RelOpState.delta (SemCond b)) + (SemComm cmThen) s1 s2 -> + SemCond bPost s2 + rThen = λ h -> + let t1 : SemCond b s1 × SemComm cmThen s1 s2 + t1 = (proj₂ (RelOpState.deltaRestPre + (SemCond b) + (SemComm cmThen) s1 s2)) h + t2 : SemCond (bPre /\ b) s1 + t2 = (proj₂ (respAnd bPre b s1)) + (q1 , proj₁ t1) + in hypThen s1 s2 t2 (proj₂ t1) + rElse : RelOpState.comp + (RelOpState.delta (NotP (SemCond b))) + (SemComm cmElse) s1 s2 -> + SemCond bPost s2 + rElse = λ h -> + let t10 : (NotP (SemCond b) s1) × + (SemComm cmElse s1 s2) + t10 = proj₂ (RelOpState.deltaRestPre + (NotP (SemCond b)) (SemComm cmElse) s1 s2) + h + t6 : SemCond (neg b) s1 + t6 = proj₂ (respNeg b s1) (proj₁ t10) + t7 : SemComm cmElse s1 s2 + t7 = proj₂ t10 + t8 : SemCond (bPre /\ neg b) s1 + t8 = proj₂ (respAnd bPre (neg b) s1) + (q1 , t6) + in hypElse s1 s2 t8 t7 + in when rThen rElse q2 +Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2 + = proj₂ (respAnd bInv (neg b) s2) t20 + where + hyp : Satisfies (bInv /\ b) cm' bInv + hyp = Soundness pr + n : ℕ + n = proj₁ q2 + Rel1 : ℕ -> Rel State (Level.zero) + Rel1 = λ m -> + 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₂ q2 + t15 : (Rel1 n s1 s2) × (NotP (SemCond b) s2) + t15 = proj₂ (RelOpState.deltaRestPost + (NotP (SemCond b)) (Rel1 n) s1 s2) + t1 + t16 : Rel1 n s1 s2 + t16 = proj₁ t15 + t17 : NotP (SemCond b) s2 + t17 = proj₂ t15 + lem1 : (m : ℕ) -> (ss2 : State) -> Rel1 m s1 ss2 -> + SemCond bInv ss2 + lem1 ℕ.zero ss2 h + = substId1 State (proj₂ h) (SemCond bInv) q1 + lem1 (ℕ.suc n) ss2 h + = let hyp2 : (z : State) -> Rel1 n s1 z -> + SemCond bInv z + hyp2 = lem1 n + s20 : State + s20 = proj₁ h + t21 : Rel1 n s1 s20 + t21 = proj₁ (proj₂ h) + t22 : (SemCond b s20) × (SemComm cm' s20 ss2) + t22 = proj₂ (RelOpState.deltaRestPre + (SemCond b) (SemComm cm') s20 ss2) + (proj₂ (proj₂ h)) + t23 : SemCond (bInv /\ b) s20 + t23 = proj₂ (respAnd bInv b s20) + (hyp2 s20 t21 , proj₁ t22) + in hyp s20 ss2 t23 (proj₂ t22) + t20 : SemCond bInv s2 × SemCond (neg b) s2 + t20 = lem1 n s2 t16 , proj₂ (respNeg b s2) t17
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/HoareSoundness.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,197 @@ +{-@$\#$@ OPTIONS --universe-polymorphism @$\#$@-} + +open import Level +open import Data.Nat.Base +open import Data.Product +open import Data.Bool.Base +open import Data.Empty +open import Data.Sum +open import Relation.Binary +open import Relation.Nullary +open import Relation.Binary.Core +open import Relation.Binary.PropositionalEquality +open import RelOp +open import utilities + +module HoareSoundness + (Cond : Set) + (PrimComm : Set) + (neg : Cond @$\rightarrow$@ Cond) + (_@$\wedge$@_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond) + (Tautology : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Set) + (State : Set) + (SemCond : Cond @$\rightarrow$@ State @$\rightarrow$@ Set) + (tautValid : (b1 b2 : Cond) @$\rightarrow$@ Tautology b1 b2 @$\rightarrow$@ + (s : State) @$\rightarrow$@ SemCond b1 s @$\rightarrow$@ SemCond b2 s) + (respNeg : (b : Cond) @$\rightarrow$@ (s : State) @$\rightarrow$@ + Iff (SemCond (neg b) s) (@$\neg$@ SemCond b s)) + (respAnd : (b1 b2 : Cond) @$\rightarrow$@ (s : State) @$\rightarrow$@ + Iff (SemCond (b1 @$\wedge$@ b2) s) + ((SemCond b1 s) @$\times$@ (SemCond b2 s))) + (PrimSemComm : @$\forall$@ {l} @$\rightarrow$@ PrimComm @$\rightarrow$@ Rel State l) + (Axiom : Cond @$\rightarrow$@ PrimComm @$\rightarrow$@ Cond @$\rightarrow$@ Set) + (axiomValid : @$\forall$@ {l} @$\rightarrow$@ (bPre : Cond) @$\rightarrow$@ (pcm : PrimComm) @$\rightarrow$@ (bPost : Cond) @$\rightarrow$@ + (ax : Axiom bPre pcm bPost) @$\rightarrow$@ (s1 s2 : State) @$\rightarrow$@ + SemCond bPre s1 @$\rightarrow$@ PrimSemComm {l} pcm s1 s2 @$\rightarrow$@ SemCond bPost s2) where + +open import Hoare PrimComm Cond Axiom Tautology _@$\wedge$@_ neg + +open import RelOp +module RelOpState = RelOp State + +NotP : {S : Set} @$\rightarrow$@ Pred S @$\rightarrow$@ Pred S +NotP X s = @$\neg$@ X s + +_\/_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond +b1 \/ b2 = neg (neg b1 @$\wedge$@ neg b2) + +when : {X Y Z : Set} @$\rightarrow$@ (X @$\rightarrow$@ Z) @$\rightarrow$@ (Y @$\rightarrow$@ Z) @$\rightarrow$@ + X ⊎ Y @$\rightarrow$@ Z +when f g (inj@$\_{1}$@ x) = f x +when f g (inj@$\_{2}$@ y) = g y + +-- semantics of commands +SemComm : Comm @$\rightarrow$@ Rel State (Level.zero) +SemComm Skip = RelOpState.deltaGlob +SemComm Abort = RelOpState.emptyRel +SemComm (PComm pc) = PrimSemComm pc +SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2) +SemComm (If b c1 c2) + = RelOpState.union + (RelOpState.comp (RelOpState.delta (SemCond b)) + (SemComm c1)) + (RelOpState.comp (RelOpState.delta (NotP (SemCond b))) + (SemComm c2)) +SemComm (While b c) + = RelOpState.unionInf + (@$\lambda$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ + RelOpState.comp (RelOpState.repeat + n + (RelOpState.comp + (RelOpState.delta (SemCond b)) + (SemComm c))) + (RelOpState.delta (NotP (SemCond b)))) + +Satisfies : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Cond @$\rightarrow$@ Set +Satisfies bPre cm bPost + = (s1 : State) @$\rightarrow$@ (s2 : State) @$\rightarrow$@ + SemCond bPre s1 @$\rightarrow$@ SemComm cm s1 s2 @$\rightarrow$@ SemCond bPost s2 + +Soundness : {bPre : Cond} @$\rightarrow$@ {cm : Comm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@ + HTProof bPre cm bPost @$\rightarrow$@ Satisfies bPre cm bPost +Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2 + = axiomValid bPre cm bPost pr s1 s2 q1 q2 +Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2 + = substId1 State {Level.zero} {State} {s1} {s2} (proj@$\_{2}$@ q2) (SemCond bPost) q1 +Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 () +Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost) + s1 s2 q1 q2 + = let hyp : Satisfies bPre' cm bPost' + hyp = Soundness pr + r1 : SemCond bPre' s1 + r1 = tautValid bPre bPre' tautPre s1 q1 + r2 : SemCond bPost' s2 + r2 = hyp s1 s2 r1 q2 + in tautValid bPost' bPost tautPost s2 r2 +Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2) + s1 s2 q1 q2 + = let hyp1 : Satisfies bPre cm1 bMid + 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 +Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse) + s1 s2 q1 q2 + = let hypThen : Satisfies (bPre @$\wedge$@ b) cmThen bPost + hypThen = Soundness pThen + 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 @$\wedge$@ 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 + rElse = @$\lambda$@ h @$\rightarrow$@ + 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 @$\wedge$@ neg b) s1 + t8 = proj@$\_{2}$@ (respAnd bPre (neg b) s1) + (q1 , t6) + in hypElse s1 s2 t8 t7 + in when rThen rElse q2 +Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2 + = proj@$\_{2}$@ (respAnd bInv (neg b) s2) t20 + where + 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 = @$\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 = 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$@ + 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) + (proj@$\_{2}$@ (proj@$\_{2}$@ h)) + t23 : SemCond (bInv @$\wedge$@ 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/RelOp.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,81 @@ +{-# OPTIONS --universe-polymorphism #-} + +open import Level +open import Data.Empty +open import Data.Product +open import Data.Nat.Base +open import Data.Sum +open import Data.Unit +open import Relation.Binary +open import Relation.Binary.Core +open import Relation.Nullary +open import utilities + +module RelOp (S : Set) where + +data Id {l} {X : Set} : Rel X l where + ref : {x : X} -> Id x x + +-- substId1 | x == y & P(x) => P(y) +substId1 : ∀ {l} -> {X : Set} -> {x y : X} -> + Id {l} x y -> (P : Pred X) -> P x -> P y +substId1 ref P q = q + +-- substId2 | x == y & P(y) => P(x) +substId2 : ∀ {l} -> {X : Set} -> {x y : X} -> + Id {l} x y -> (P : Pred X) -> P y -> P x +substId2 ref P q = q + +-- for X ⊆ S (formally, X : Pred S) +-- delta X = { (a, a) | a ∈ X } +delta : ∀ {l} -> Pred S -> Rel S l +delta X a b = X a × Id a b + +-- deltaGlob = delta S +deltaGlob : ∀ {l} -> Rel S l +deltaGlob = delta (λ (s : S) → ⊤) + +-- emptyRel = \varnothing +emptyRel : Rel S Level.zero +emptyRel a b = ⊥ + +-- comp R1 R2 = R2 ∘ R1 (= R1; R2) +comp : ∀ {l} -> Rel S l -> Rel S l -> Rel S l +comp R1 R2 a b = ∃ (λ (a' : S) → R1 a a' × R2 a' b) + +-- union R1 R2 = R1 ∪ R2 +union : ∀ {l} -> Rel S l -> Rel S l -> Rel S l +union R1 R2 a b = R1 a b ⊎ R2 a b + +-- repeat n R = R^n +repeat : ∀ {l} -> ℕ -> Rel S l -> Rel S l +repeat ℕ.zero R = deltaGlob +repeat (ℕ.suc m) R = comp (repeat m R) R + +-- unionInf f = ⋃_{n ∈ ω} f(n) +unionInf : ∀ {l} -> (ℕ -> Rel S l) -> Rel S l +unionInf f a b = ∃ (λ (n : ℕ) → f n a b) +-- restPre X R = { (s1,s2) ∈ R | s1 ∈ X } +restPre : ∀ {l} -> Pred S -> Rel S l -> Rel S l +restPre X R a b = X a × R a b + +-- restPost X R = { (s1,s2) ∈ R | s2 ∈ X } +restPost : ∀ {l} -> Pred S -> Rel S l -> Rel S l +restPost X R a b = R a b × X b + +deltaRestPre : (X : Pred S) -> (R : Rel S Level.zero) -> (a b : S) -> + Iff (restPre X R a b) (comp (delta X) R a b) +deltaRestPre X R a b + = (λ (h : restPre X R a b) → a , (proj₁ h , ref) , proj₂ h) , + λ (h : comp (delta X) R a b) → proj₁ (proj₁ (proj₂ h)) , + substId2 + (proj₂ (proj₁ (proj₂ h))) + (λ z → R z b) (proj₂ (proj₂ h)) + +deltaRestPost : (X : Pred S) -> (R : Rel S Level.zero) -> (a b : S) -> + Iff (restPost X R a b) (comp R (delta X) a b) +deltaRestPost X R a b + = (λ (h : restPost X R a b) → b , proj₁ h , proj₂ h , ref) , + λ (h : comp R (delta X) a b) → + substId1 (proj₂ (proj₂ (proj₂ h))) (R a) (proj₁ (proj₂ h)) , + substId1 (proj₂ (proj₂ (proj₂ h))) X (proj₁ (proj₂ (proj₂ h)))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/RelOp.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,81 @@ +{-@$\#$@ OPTIONS --universe-polymorphism @$\#$@-} + +open import Level +open import Data.Empty +open import Data.Product +open import Data.Nat.Base +open import Data.Sum +open import Data.Unit +open import Relation.Binary +open import Relation.Binary.Core +open import Relation.Nullary +open import utilities + +module RelOp (S : Set) where + +data Id {l} {X : Set} : Rel X l where + ref : {x : X} @$\rightarrow$@ Id x x + +-- substId1 | x == y & P(x) => P(y) +substId1 : @$\forall$@ {l} @$\rightarrow$@ {X : Set} @$\rightarrow$@ {x y : X} @$\rightarrow$@ + Id {l} x y @$\rightarrow$@ (P : Pred X) @$\rightarrow$@ P x @$\rightarrow$@ P y +substId1 ref P q = q + +-- substId2 | x == y & P(y) => P(x) +substId2 : @$\forall$@ {l} @$\rightarrow$@ {X : Set} @$\rightarrow$@ {x y : X} @$\rightarrow$@ + Id {l} x y @$\rightarrow$@ (P : Pred X) @$\rightarrow$@ P y @$\rightarrow$@ P x +substId2 ref P q = q + +-- for X ⊆ S (formally, X : Pred S) +-- delta X = { (a, a) | a ∈ X } +delta : @$\forall$@ {l} @$\rightarrow$@ Pred S @$\rightarrow$@ Rel S l +delta X a b = X a @$\times$@ Id a b + +-- deltaGlob = delta S +deltaGlob : @$\forall$@ {l} @$\rightarrow$@ Rel S l +deltaGlob = delta (@$\lambda$@ (s : S) @$\rightarrow$@ @$\top$@) + +-- emptyRel = \varnothing +emptyRel : Rel S Level.zero +emptyRel a b = @$\bot$@ + +-- comp R1 R2 = R2 ∘ R1 (= R1; R2) +comp : @$\forall$@ {l} @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l +comp R1 R2 a b = ∃ (@$\lambda$@ (a' : S) @$\rightarrow$@ R1 a a' @$\times$@ R2 a' b) + +-- union R1 R2 = R1 ∪ R2 +union : @$\forall$@ {l} @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l +union R1 R2 a b = R1 a b ⊎ R2 a b + +-- repeat n R = R^n +repeat : @$\forall$@ {l} @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l +repeat @$\mathbb{N}$@.zero R = deltaGlob +repeat (@$\mathbb{N}$@.suc m) R = comp (repeat m R) R + +-- unionInf f = ⋃_{n ∈ ω} f(n) +unionInf : @$\forall$@ {l} @$\rightarrow$@ (@$\mathbb{N}$@ @$\rightarrow$@ Rel S l) @$\rightarrow$@ Rel S l +unionInf f a b = ∃ (@$\lambda$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ f n a b) +-- restPre X R = { (s1,s2) ∈ R | s1 ∈ X } +restPre : @$\forall$@ {l} @$\rightarrow$@ Pred S @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l +restPre X R a b = X a @$\times$@ R a b + +-- restPost X R = { (s1,s2) ∈ R | s2 ∈ X } +restPost : @$\forall$@ {l} @$\rightarrow$@ Pred S @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l +restPost X R a b = R a b @$\times$@ X b + +deltaRestPre : (X : Pred S) @$\rightarrow$@ (R : Rel S Level.zero) @$\rightarrow$@ (a b : S) @$\rightarrow$@ + Iff (restPre X R a b) (comp (delta X) R a b) +deltaRestPre X R a b + = (@$\lambda$@ (h : restPre X R a b) @$\rightarrow$@ a , (proj@$\_{1}$@ h , ref) , proj@$\_{2}$@ h) , + @$\lambda$@ (h : comp (delta X) R a b) @$\rightarrow$@ proj@$\_{1}$@ (proj@$\_{1}$@ (proj@$\_{2}$@ h)) , + substId2 + (proj@$\_{2}$@ (proj@$\_{1}$@ (proj@$\_{2}$@ h))) + (@$\lambda$@ z @$\rightarrow$@ R z b) (proj@$\_{2}$@ (proj@$\_{2}$@ h)) + +deltaRestPost : (X : Pred S) @$\rightarrow$@ (R : Rel S Level.zero) @$\rightarrow$@ (a b : S) @$\rightarrow$@ + Iff (restPost X R a b) (comp R (delta X) a b) +deltaRestPost X R a b + = (@$\lambda$@ (h : restPost X R a b) @$\rightarrow$@ b , proj@$\_{1}$@ h , proj@$\_{2}$@ h , ref) , + @$\lambda$@ (h : comp R (delta X) a b) @$\rightarrow$@ + substId1 (proj@$\_{2}$@ (proj@$\_{2}$@ (proj@$\_{2}$@ h))) (R a) (proj@$\_{1}$@ (proj@$\_{2}$@ h)) , + substId1 (proj@$\_{2}$@ (proj@$\_{2}$@ (proj@$\_{2}$@ h))) X (proj@$\_{1}$@ (proj@$\_{2}$@ (proj@$\_{2}$@ h)))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-func.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,2 @@ ++1 : ℕ → ℕ ++1 m = suc m
--- a/paper/src/agda-func.agda.replaced Mon Feb 17 17:14:00 2020 +0900 +++ b/paper/src/agda-func.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -1,5 +1,2 @@ +1 : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ +1 m = suc m - --- eval +1 zero --- return suc zero
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-interpret.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,13 @@ +{-# TERMINATING #-} +interpret : Env → Comm → Env +interpret env Skip = env +interpret env Abort = env +interpret env (PComm x) = x env +interpret env (Seq comm comm1) = interpret (interpret env comm) comm1 +interpret env (If x then else) with x env +... | true = interpret env then +... | false = interpret env else +interpret env (While x comm) with x env +... | true = interpret (interpret env comm) (While x comm) +... | false = env +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-prog.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,7 @@ +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)} ))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-rule.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,27 @@ +data HTProof : Cond -> Comm -> Cond -> Set where + PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} -> + (pr : Axiom bPre pcm bPost) -> + HTProof bPre (PComm pcm) bPost + SkipRule : (b : Cond) -> HTProof b Skip b + AbortRule : (bPre : Cond) -> (bPost : Cond) -> + HTProof bPre Abort bPost + 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 + 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)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-satisfies.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,25 @@ +SemComm : Comm -> Rel State (Level.zero) +SemComm Skip = RelOpState.deltaGlob +SemComm Abort = RelOpState.emptyRel +SemComm (PComm pc) = PrimSemComm pc +SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2) +SemComm (If b c1 c2) + = RelOpState.union + (RelOpState.comp (RelOpState.delta (SemCond b)) + (SemComm c1)) + (RelOpState.comp (RelOpState.delta (NotP (SemCond b))) + (SemComm c2)) +SemComm (While b c) + = RelOpState.unionInf + (λ (n : $mathbb{N}$) -> + RelOpState.comp (RelOpState.repeat + n + (RelOpState.comp + (RelOpState.delta (SemCond b)) + (SemComm c))) + (RelOpState.delta (NotP (SemCond b)))) + +Satisfies : Cond -> Comm -> Cond -> Set +Satisfies bPre cm bPost + = (s1 : State) -> (s2 : State) -> + SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-soundness.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,66 @@ +Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> + HTProof bPre cm bPost -> Satisfies bPre cm bPost +Soundness (PrimRule {bPre} {cm} {bPost} pr) s1 s2 q1 q2 + = axiomValid bPre cm bPost pr s1 s2 q1 q2 +Soundness {.bPost} {.Skip} {bPost} (SkipRule .bPost) s1 s2 q1 q2 + = substId1 State {Level.zero} {State} {s1} {s2} (proj₂ q2) (SemCond bPost) q1 +Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 () +Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost) + s1 s2 q1 q2 + = let hyp : Satisfies bPre' cm bPost' + hyp = Soundness pr + in tautValid bPost' bPost tautPost s2 (hyp s1 s2 (tautValid bPre bPre' tautPre s1 q1) q2) +Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2) + s1 s2 q1 q2 + = let hyp1 : Satisfies bPre cm1 bMid + hyp1 = Soundness pr1 + hyp2 : Satisfies bMid cm2 bPost + hyp2 = Soundness pr2 + in hyp2 (proj₁ q2) s2 (hyp1 s1 (proj₁ q2) q1 (proj₁ (proj₂ q2))) (proj₂ (proj₂ q2)) +Soundness (IfRule {cmThen} {cmElse} {bPre} {bPost} {b} pThen pElse) + s1 s2 q1 q2 + = let hypThen : Satisfies (bPre /\ b) cmThen bPost + hypThen = Soundness pThen + hypElse : Satisfies (bPre /\ neg b) cmElse bPost + hypElse = Soundness pElse + rThen : RelOpState.comp (RelOpState.delta (SemCond b)) + (SemComm cmThen) s1 s2 -> SemCond bPost s2 + rThen = λ h -> hypThen s1 s2 ((proj₂ (respAnd bPre b s1)) (q1 , proj₁ t1)) + (proj₂ ((proj₂ (RelOpState.deltaRestPre (SemCond b) (SemComm cmThen) s1 s2)) h)) + rElse : RelOpState.comp (RelOpState.delta (NotP (SemCond b))) + (SemComm cmElse) s1 s2 -> SemCond bPost s2 + rElse = λ h -> + let t10 : (NotP (SemCond b) s1) × (SemComm cmElse s1 s2) + t10 = proj₂ (RelOpState.deltaRestPre + (NotP (SemCond b)) (SemComm cmElse) s1 s2) h + in hypElse s1 s2 (proj₂ (respAnd bPre (neg b) s1) + (q1 , (proj₂ (respNeg b s1) (proj₁ t10)))) (proj₂ t10) + in when rThen rElse q2 +Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2 + = proj₂ (respAnd bInv (neg b) s2) + (lem1 (proj₁ q2) s2 (proj₁ t15) , proj₂ (respNeg b s2) (proj₂ t15)) + where + hyp : Satisfies (bInv /\ b) cm' bInv + hyp = Soundness pr + Rel1 : ℕ -> Rel State (Level.zero) + Rel1 = λ m -> + RelOpState.repeat + m + (RelOpState.comp (RelOpState.delta (SemCond b)) + (SemComm cm')) + t15 : (Rel1 (proj₁ q2) s1 s2) × (NotP (SemCond b) s2) + t15 = proj₂ (RelOpState.deltaRestPost + (NotP (SemCond b)) (Rel1 (proj₁ q2)) s1 s2) (proj₂ q2) + lem1 : (m : ℕ) -> (ss2 : State) -> Rel1 m s1 ss2 -> SemCond bInv ss2 + lem1 zero ss2 h = substId1 State (proj₂ h) (SemCond bInv) q1 + lem1 (suc n) ss2 h + = let hyp2 : (z : State) -> Rel1 (proj₁ q2) s1 z -> + SemCond bInv z + hyp2 = lem1 n + t22 : (SemCond b (proj₁ h)) × (SemComm cm' (proj₁ h) ss2) + t22 = proj₂ (RelOpState.deltaRestPre (SemCond b) (SemComm cm') (proj₁ h) ss2) + (proj₂ (proj₂ h)) + t23 : SemCond (bInv /\ b) (proj₁ h) + t23 = proj₂ (respAnd bInv b (proj₁ h)) + (hyp2 (proj₁ h) (proj₁ (proj₂ h)) , proj₁ t22) + in hyp (proj₁ h) ss2 t23 (proj₂ t22)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-term.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,12 @@ +loopP' : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t +loopP' record { c10 = c10 ; varn = zero ; vari = vari } exit = + exit (record { c10 = c10 ; varn = zero ; vari = vari }) +loopP' record { c10 = c10 ; varn = (suc varn₁) ; vari = vari } exit = + whileLoopP' (record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) + (λ env → loopP' (record { c10 = c10 ; varn = varn₁ ; vari = vari }) exit ) exit + +whileTestPCall' : (c10 : ℕ ) → Envc +whileTestPCall' c10 = whileTestP' {_} {_} c10 (λ env → loopP' env (λ env → env)) + +-- whileTestP' 10 +-- record { c10 = 10 ; varn = 0 ; vari = 10 }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-term.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,12 @@ +loopP' : {l : Level} {t : Set l} @$\rightarrow$@ Envc @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t +loopP' record { c10 = c10 ; varn = zero ; vari = vari } exit = + exit (record { c10 = c10 ; varn = zero ; vari = vari }) +loopP' record { c10 = c10 ; varn = (suc varn@$\_{1}$@) ; vari = vari } exit = + whileLoopP' (record { c10 = c10 ; varn = (suc varn@$\_{1}$@) ; vari = vari }) + (@$\lambda$@ env @$\rightarrow$@ loopP' (record { c10 = c10 ; varn = varn@$\_{1}$@ ; vari = vari }) exit ) exit + +whileTestPCall' : (c10 : @$\mathbb{N}$@ ) @$\rightarrow$@ Envc +whileTestPCall' c10 = whileTestP' {_} {_} c10 (@$\lambda$@ env @$\rightarrow$@ loopP' env (@$\lambda$@ env @$\rightarrow$@ env)) + +-- whileTestP' 10 +-- record { c10 = 10 ; varn = 0 ; vari = 10 }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-while.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,8 @@ +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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-whileprog.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,16 @@ +whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Envc → t) → t +whileTestP c10 next = next (record {c10 = c10 ; varn = c10 ; vari = 0 }) + +whileLoopP' : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t +whileLoopP' record { c10 = c10 ; varn = zero ; vari = vari } _ exit = exit record { c10 = c10 ; varn = zero ; vari = vari } +whileLoopP' record { c10 = c10 ; varn = suc varn1 ; vari = vari } next _ = next (record {c10 = c10 ; varn = varn1 ; vari = suc vari }) + +{-# TERMINATING #-} +loopP : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t +loopP env exit = whileLoopP' env (λ env → loopP env exit ) exit + +whileTestPCall : (c10 : ℕ ) → Envc +whileTestPCall c10 = whileTestP {_} {_} c10 (λ env → loopP env (λ env → env)) + +-- whileTestPCall 10 +-- record { c10 = 10 ; varn = 0 ; vari = 10 }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-whileprog.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,16 @@ +whileTestP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (Code : Envc @$\rightarrow$@ t) @$\rightarrow$@ t +whileTestP c10 next = next (record {c10 = c10 ; varn = c10 ; vari = 0 }) + +whileLoopP' : {l : Level} {t : Set l} @$\rightarrow$@ Envc @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoopP' record { c10 = c10 ; varn = zero ; vari = vari } _ exit = exit record { c10 = c10 ; varn = zero ; vari = vari } +whileLoopP' record { c10 = c10 ; varn = suc varn1 ; vari = vari } next _ = next (record {c10 = c10 ; varn = varn1 ; vari = suc vari }) + +{-@$\#$@ TERMINATING @$\#$@-} +loopP : {l : Level} {t : Set l} @$\rightarrow$@ Envc @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t +loopP env exit = whileLoopP' env (@$\lambda$@ env @$\rightarrow$@ loopP env exit ) exit + +whileTestPCall : (c10 : @$\mathbb{N}$@ ) @$\rightarrow$@ Envc +whileTestPCall c10 = whileTestP {_} {_} c10 (@$\lambda$@ env @$\rightarrow$@ loopP env (@$\lambda$@ env @$\rightarrow$@ env)) + +-- whileTestPCall 10 +-- record { c10 = 10 ; varn = 0 ; vari = 10 }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-write.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,15 @@ +-- Nomal CodeGear +whileLoop' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc) + → (n ≡ varn env) + → (next : Envc → t) + → (exit : Envc → t) → 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 base CodeGear +whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) + → (n ≡ varn env) → (pre : varn env + vari env ≡ c10 env) + → (next : (env : Envc ) → (pred n ≡ varn env) → (post : varn env + vari env ≡ c10 env) → t) + → (exit : (env : Envc ) → (fin : vari env ≡ c10 env) → t) → t +whileLoopPwP' zero env refl refl next exit = exit env refl +whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-mcg.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,5 @@ +whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → + ((env : Envc ) → (mdg : (vari env ≡ 0) /\ (varn env ≡ c10 env)) → t) → t +whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where + env : Envc + env = whileTestP c10 ( λ env → env )
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-mdg.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,10 @@ +data whileTestState : Set where + s1 : whileTestState + s2 : whileTestState + sf : whileTestState + + +whileTestStateP : whileTestState → Envc → Set +whileTestStateP s1 env = (vari env ≡ 0) /\ (varn env ≡ c10 env) +whileTestStateP s2 env = (varn env + vari env ≡ c10 env) +whileTestStateP sf env = (vari env ≡ c10 env)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-pattern.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,4 @@ +_-_ : Nat → Nat → Nat +n - zero = n +zero - suc m = zero +suc n - suc m = n - m
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-plus.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,3 @@ +_+_ : ℕ → ℕ → ℕ +zero + m = m +suc n + m = suc (n + m)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-rewrite.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,3 @@ +rewrite-+-comm : (x y : ℕ) → x + y ≡ y + x +rewrite-+-comm zero y rewrite (+zero {y}) = refl +rewrite-+-comm (suc x) y = ?
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-term.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,28 @@ +module agda-term where + +open import Data.Nat.Base +open import Relation.Binary.PropositionalEquality + ++zero : {y : ℕ} → y + zero ≡ y ++zero {zero} = refl ++zero {suc y} = cong (λ yy → suc yy) (+zero {y}) + ++-suc : {x y : ℕ} → x + suc y ≡ suc (x + y) ++-suc {zero} {y} = refl ++-suc {suc x} {y} = cong suc (+-suc {x} {y}) + ++-comm : (x y : ℕ) → x + y ≡ y + x ++-comm zero y rewrite (+zero {y}) = refl ++-comm (suc x) y = let open ≡-Reasoning in + begin + suc (x + y) ≡⟨⟩ + suc (x + y) ≡⟨ cong suc (+-comm x y) ⟩ + suc (y + x) ≡⟨ sym (+-suc {y} {x}) ⟩ + y + suc x ∎ + ++-come : (x y : ℕ) → x + y ≡ y + x ++-come zero y rewrite (+zero {y}) = refl ++-come (suc x) y + rewrite (cong suc (+-come x y)) | sym (+-suc {y} {x}) = refl + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-term1.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,10 @@ ++-comm : (x y : ℕ) → x + y ≡ y + x ++-comm zero y rewrite (+zero {y}) = refl ++-comm (suc x) y = let open ≡-Reasoning in + begin + ?0 ≡⟨ ?1 ⟩ + ?2 ∎ + +-- ?0 : ℕ {(suc x) + y} +-- ?1 : suc x + y ≡ y + suc x +-- ?2 : ℕ
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-term2.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,11 @@ ++-comm : (x y : ℕ) → x + y ≡ y + x ++-comm zero y rewrite (+zero {y}) = refl ++-comm (suc x) y = let open ≡-Reasoning in + begin + (suc x) + y ≡⟨⟩ + suc (x + y) ≡⟨ cong suc (+-comm x y) ⟩ + suc (y + x) ≡⟨ ?0 ⟩ + ?1 ∎ + +-- ?0 : suc (y + x) ≡ y + suc x +-- ?1 : y + suc x
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-term3.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,12 @@ ++-comm : (x y : ℕ) → x + y ≡ y + x ++-comm zero y rewrite (+zero {y}) = refl ++-comm (suc x) y = let open ≡-Reasoning in + begin + suc (x + y) ≡⟨⟩ + suc (x + y) ≡⟨ cong suc (+-comm x y) ⟩ + suc (y + x) ≡⟨ sym (+-suc {y} {x}) ⟩ + y + suc x ∎ + +-- +-suc : {x y : ℕ} → x + suc y ≡ suc (x + y) +-- +-suc {zero} {y} = refl +-- +-suc {suc x} {y} = cong suc (+-suc {x} {y})
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-agda.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,6 @@ +plus : {l : Level} {t : Set l} → (x y : ℕ) → (next : ℕ -> t) -> t +plus x zero next = next x +plus x (suc y) next = plus (suc x) y next + +-- plus 10 20 +-- λ next → next 30
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-condition.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,9 @@ +data whileTestState : Set where + s1 : whileTestState + s2 : whileTestState + sf : whileTestState + +whileTestStateP : whileTestState → Envc → Set +whileTestStateP s1 env = (vari env ≡ 0) /\ (varn env ≡ c10 env) +whileTestStateP s2 env = (varn env + vari env ≡ c10 env) +whileTestStateP sf env = (vari env ≡ c10 env)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-hoare-helperCall.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,3 @@ +whileCallwP : (c : ℕ) → whileTestPCallwP' c +whileCallwP c = whileTestPwP {_} {_} c + (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-hoare-helperCall.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,3 @@ +whileCallwP : (c : @$\mathbb{N}$@) @$\rightarrow$@ whileTestPCallwP' c +whileCallwP c = whileTestPwP {_} {_} c + (@$\lambda$@ env s @$\rightarrow$@ loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-hoare-loop.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,15 @@ +whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) + → (n ≡ varn env) → whileTestStateP s2 env + → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env → t) + → (exit : (env : Envc ) → whileTestStateP sf env → t) → t +whileLoopPwP' zero env refl refl _ exit = exit env refl +whileLoopPwP' (suc n) env refl refl next _ = + next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) + + +loopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) + → (n ≡ varn env) → whileTestStateP s2 env + → (exit : (env : Envc ) → whileTestStateP sf env → t) → t +loopPwP' zero env refl refl exit = exit env refl +loopPwP' (suc n) env refl refl exit + = whileLoopPwP' (suc n) env refl refl (λ env x y → loopPwP' n env x y exit) exit
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-hoare-loop.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,15 @@ +whileLoopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) + @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env + @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ (pred n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env @$\rightarrow$@ t) + @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoopPwP' zero env refl refl _ exit = exit env refl +whileLoopPwP' (suc n) env refl refl next _ = + next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) + + +loopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) + @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env + @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env @$\rightarrow$@ t) @$\rightarrow$@ t +loopPwP' zero env refl refl exit = exit env refl +loopPwP' (suc n) env refl refl exit + = whileLoopPwP' (suc n) env refl refl (@$\lambda$@ env x y @$\rightarrow$@ loopPwP' n env x y exit) exit
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-hoare-loophelper.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,5 @@ +loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) + → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁)) +loopHelper zero env eq refl rewrite eq = refl +loopHelper (suc n) env refl refl = + loopHelper n (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-hoare-loophelper.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,5 @@ +loopHelper : (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ (eq : varn env @$\equiv$@ n) @$\rightarrow$@ (seq : whileTestStateP s2 env) + @$\rightarrow$@ loopPwP' n env (sym eq) seq (@$\lambda$@ env@$\_{1}$@ x @$\rightarrow$@ (vari env@$\_{1}$@ @$\equiv$@ c10 env@$\_{1}$@)) +loopHelper zero env eq refl rewrite eq = refl +loopHelper (suc n) env refl refl = + loopHelper n (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-hoare-prim.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,4 @@ +whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t +whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where + env : Envc + env = whileTestP c10 ( λ env → env )
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-hoare-prim.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,4 @@ +whileTestPwP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ ((env : Envc ) @$\rightarrow$@ whileTestStateP s1 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 )
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-hoare-soundness.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,6 @@ +whileCallwP : (c : ℕ) → whileTestPCallwP' c +whileCallwP c = whileTestPwP {_} {_} c + (λ env s → loopPwP' (c10 env) env (sym (pi2 s)) (conv env s) {!!}) + where + conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-hoare-soundness.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,6 @@ +whileCallwP : (c : @$\mathbb{N}$@) @$\rightarrow$@ whileTestPCallwP' c +whileCallwP c = whileTestPwP {_} {_} c + (@$\lambda$@ env s @$\rightarrow$@ loopPwP' (c10 env) env (sym (pi2 s)) (conv env s) {!!}) + where + conv : (env : Envc ) @$\rightarrow$@ (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) @$\rightarrow$@ varn env + vari env @$\equiv$@ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-hoare-while.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,5 @@ +whileCallwP : (c : ℕ ) → Set +whileCallwP c = whileTestPwP {_} {_} c (λ env s → loopPwP' (varn env) env refl (conv env s) ( λ env s → vari env ≡ c10 env ) ) + where + conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-hoare-while.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,5 @@ +whileCallwP : (c : @$\mathbb{N}$@ ) @$\rightarrow$@ Set +whileCallwP c = whileTestPwP {_} {_} c (@$\lambda$@ env s @$\rightarrow$@ loopPwP' (varn env) env refl (conv env s) ( @$\lambda$@ env s @$\rightarrow$@ vari env @$\equiv$@ c10 env ) ) + where + conv : (env : Envc ) @$\rightarrow$@ (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) @$\rightarrow$@ varn env + vari env @$\equiv$@ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/cbc-hoare.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,14 @@ +whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t +whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where + env : Envc + env = whileTestP c10 ( λ env → env ) + +loopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t +loopPwP' zero env refl refl exit = exit env refl +loopPwP' (suc n) env refl refl exit = whileLoopPwP' (suc n) env refl refl (λ env x y → loopPwP' n env x y exit) exit + + +whileTestPCallwP' : (c : ℕ ) → Set +whileTestPCallwP' c = whileTestPwP {_} {_} c (λ env s → loopPwP' (varn env) env refl (conv env s) ( λ env s → vari env ≡ c10 env ) ) + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/env.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,8 @@ +record Envc : Set where + field + vari : ℕ + varn : ℕ + c10 : ℕ + +makeEnv : ℕ → ℕ → ℕ → Envc +makeEnv i n c = record { vari = i ; varn = n ; c10 = c }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/env.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,8 @@ +record Envc : Set where + field + vari : @$\mathbb{N}$@ + varn : @$\mathbb{N}$@ + c10 : @$\mathbb{N}$@ + +makeEnv : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Envc +makeEnv i n c = record { vari = i ; varn = n ; c10 = c }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/implies.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,2 @@ +data _implies_ (A B : Set ) : Set (succ Zero) where + proof : ( A → B ) → A implies B
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/implies.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,2 @@ +data _implies_ (A B : Set ) : Set (succ Zero) where + proof : ( A @$\rightarrow$@ B ) @$\rightarrow$@ A implies B
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/termination.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,11 @@ +{-# TERMINATING #-} +loop : ℕ → ℕ +loop n = loop (pred n) + +-- pred : ℕ → ℕ +-- pred zero = zero +-- pred (suc n) = n + +stop : ℕ → ℕ +stop zero = zero +stop (suc n) = (stop n)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/termination.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,11 @@ +{-@$\#$@ TERMINATING @$\#$@-} +loop : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ +loop n = loop (pred n) + +-- pred : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ +-- pred zero = zero +-- pred (suc n) = n + +stop : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ +stop zero = zero +stop (suc n) = (stop n)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/tree.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,10 @@ +data nomal-tree (A : Set) : Set where + nleaf : (key : ℕ) → tree A + nnode : (key : ℕ) → (lnode : nomal-tree A) → (rnode : nomal-tree A) → nomal-tree A + +data meta-tree (A : Set) : (key : ℕ) → Set where + mleaf : (key : ℕ) → meta-tree A key + mnode : { l r : ℕ } → (key : ℕ) → (value : A) + → (lnode : meta-tree A l) → (rnode : meta-tree A r) + → l ≤ key → key ≤ r → metatree A key +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/utilities.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,166 @@ +{-# OPTIONS --allow-unsolved-metas #-} +module utilities where + +open import Function +open import Data.Nat +open import Data.Product +open import Data.Bool hiding ( _≟_ ; _≤?_) +open import Level renaming ( suc to succ ; zero to Zero ) +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Relation.Binary.PropositionalEquality + +Pred : Set -> Set₁ +Pred X = X -> Set + +Imply : Set -> Set -> Set +Imply X Y = X -> Y + +Iff : Set -> Set -> Set +Iff X Y = Imply X Y × Imply Y X + +record _/\_ {n : Level } (a : Set n) (b : Set n): Set n where + field + pi1 : a + pi2 : b + +open _/\_ + +_-_ : ℕ → ℕ → ℕ +x - zero = x +zero - _ = zero +(suc x) - (suc y) = x - y + ++zero : { y : ℕ } → y + zero ≡ y ++zero {zero} = refl ++zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) + + ++-sym : { x y : ℕ } → x + y ≡ y + x ++-sym {zero} {zero} = refl ++-sym {zero} {suc y} = let open ≡-Reasoning in + begin + zero + suc y + ≡⟨⟩ + suc y + ≡⟨ sym +zero ⟩ + suc y + zero + ∎ ++-sym {suc x} {zero} = let open ≡-Reasoning in + begin + suc x + zero + ≡⟨ +zero ⟩ + suc x + ≡⟨⟩ + zero + suc x + ∎ ++-sym {suc x} {suc y} = cong ( λ z → suc z ) ( let open ≡-Reasoning in + begin + x + suc y + ≡⟨ +-sym {x} {suc y} ⟩ + suc (y + x) + ≡⟨ cong ( λ z → suc z ) (+-sym {y} {x}) ⟩ + suc (x + y) + ≡⟨ sym ( +-sym {y} {suc x}) ⟩ + y + suc x + ∎ ) + + +minus-plus : { x y : ℕ } → (suc x - 1) + (y + 1) ≡ suc x + y +minus-plus {zero} {y} = +-sym {y} {1} +minus-plus {suc x} {y} = cong ( λ z → suc z ) (minus-plus {x} {y}) + ++1≡suc : { x : ℕ } → x + 1 ≡ suc x ++1≡suc {zero} = refl ++1≡suc {suc x} = cong ( λ z → suc z ) ( +1≡suc {x} ) + +lt : ℕ → ℕ → Bool +lt x y with (suc x ) ≤? y +lt x y | yes p = true +lt x y | no ¬p = false + +predℕ : {n : ℕ } → lt 0 n ≡ true → ℕ +predℕ {zero} () +predℕ {suc n} refl = n + +predℕ+1=n : {n : ℕ } → (less : lt 0 n ≡ true ) → (predℕ less) + 1 ≡ n +predℕ+1=n {zero} () +predℕ+1=n {suc n} refl = +1≡suc + +suc-predℕ=n : {n : ℕ } → (less : lt 0 n ≡ true ) → suc (predℕ less) ≡ n +suc-predℕ=n {zero} () +suc-predℕ=n {suc n} refl = refl + +Equal : ℕ → ℕ → Bool +Equal x y with x ≟ y +Equal x y | yes p = true +Equal x y | no ¬p = false + +_⇒_ : Bool → Bool → Bool +false ⇒ _ = true +true ⇒ true = true +true ⇒ false = false + +⇒t : {x : Bool} → x ⇒ true ≡ true +⇒t {x} with x +⇒t {x} | false = refl +⇒t {x} | true = refl + +f⇒ : {x : Bool} → false ⇒ x ≡ true +f⇒ {x} with x +f⇒ {x} | false = refl +f⇒ {x} | true = refl + +∧-pi1 : { x y : Bool } → x ∧ y ≡ true → x ≡ true +∧-pi1 {x} {y} eq with x | y | eq +∧-pi1 {x} {y} eq | false | b | () +∧-pi1 {x} {y} eq | true | false | () +∧-pi1 {x} {y} eq | true | true | refl = refl + +∧-pi2 : { x y : Bool } → x ∧ y ≡ true → y ≡ true +∧-pi2 {x} {y} eq with x | y | eq +∧-pi2 {x} {y} eq | false | b | () +∧-pi2 {x} {y} eq | true | false | () +∧-pi2 {x} {y} eq | true | true | refl = refl + +∧true : { x : Bool } → x ∧ true ≡ x +∧true {x} with x +∧true {x} | false = refl +∧true {x} | true = refl + +true∧ : { x : Bool } → true ∧ x ≡ x +true∧ {x} with x +true∧ {x} | false = refl +true∧ {x} | true = refl +bool-case : ( x : Bool ) { p : Set } → ( x ≡ true → p ) → ( x ≡ false → p ) → p +bool-case x T F with x +bool-case x T F | false = F refl +bool-case x T F | true = T refl + +impl⇒ : {x y : Bool} → (x ≡ true → y ≡ true ) → x ⇒ y ≡ true +impl⇒ {x} {y} p = bool-case x (λ x=t → let open ≡-Reasoning in + begin + x ⇒ y + ≡⟨ cong ( λ z → x ⇒ z ) (p x=t ) ⟩ + x ⇒ true + ≡⟨ ⇒t ⟩ + true + ∎ + ) ( λ x=f → let open ≡-Reasoning in + begin + x ⇒ y + ≡⟨ cong ( λ z → z ⇒ y ) x=f ⟩ + true + ∎ + ) + +Equal→≡ : { x y : ℕ } → Equal x y ≡ true → x ≡ y +Equal→≡ {x} {y} eq with x ≟ y +Equal→≡ {x} {y} refl | yes refl = refl +Equal→≡ {x} {y} () | no ¬p + +open import Data.Empty + +≡→Equal : { x y : ℕ } → x ≡ y → Equal x y ≡ true +≡→Equal {x} {.x} refl with x ≟ x +≡→Equal {x} {.x} refl | yes refl = refl +≡→Equal {x} {.x} refl | no ¬p = ⊥-elim ( ¬p refl )
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/utilities.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,166 @@ +{-@$\#$@ OPTIONS --allow-unsolved-metas @$\#$@-} +module utilities where + +open import Function +open import Data.Nat +open import Data.Product +open import Data.Bool hiding ( _≟_ ; _@$\leq$@?_) +open import Level renaming ( suc to succ ; zero to Zero ) +open import Relation.Nullary using (@$\neg$@_; Dec; yes; no) +open import Relation.Binary.PropositionalEquality + +Pred : Set @$\rightarrow$@ Set@$\_{1}$@ +Pred X = X @$\rightarrow$@ Set + +Imply : Set @$\rightarrow$@ Set @$\rightarrow$@ Set +Imply X Y = X @$\rightarrow$@ Y + +Iff : Set @$\rightarrow$@ Set @$\rightarrow$@ Set +Iff X Y = Imply X Y @$\times$@ Imply Y X + +record _@$\wedge$@_ {n : Level } (a : Set n) (b : Set n): Set n where + field + pi1 : a + pi2 : b + +open _@$\wedge$@_ + +_-_ : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ +x - zero = x +zero - _ = zero +(suc x) - (suc y) = x - y + ++zero : { y : @$\mathbb{N}$@ } @$\rightarrow$@ y + zero @$\equiv$@ y ++zero {zero} = refl ++zero {suc y} = cong ( @$\lambda$@ x @$\rightarrow$@ suc x ) ( +zero {y} ) + + ++-sym : { x y : @$\mathbb{N}$@ } @$\rightarrow$@ x + y @$\equiv$@ y + x ++-sym {zero} {zero} = refl ++-sym {zero} {suc y} = let open @$\equiv$@-Reasoning in + begin + zero + suc y + @$\equiv$@@$\langle$@@$\rangle$@ + suc y + @$\equiv$@@$\langle$@ sym +zero @$\rangle$@ + suc y + zero + @$\blacksquare$@ ++-sym {suc x} {zero} = let open @$\equiv$@-Reasoning in + begin + suc x + zero + @$\equiv$@@$\langle$@ +zero @$\rangle$@ + suc x + @$\equiv$@@$\langle$@@$\rangle$@ + zero + suc x + @$\blacksquare$@ ++-sym {suc x} {suc y} = cong ( @$\lambda$@ z @$\rightarrow$@ suc z ) ( let open @$\equiv$@-Reasoning in + begin + x + suc y + @$\equiv$@@$\langle$@ +-sym {x} {suc y} @$\rangle$@ + suc (y + x) + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ suc z ) (+-sym {y} {x}) @$\rangle$@ + suc (x + y) + @$\equiv$@@$\langle$@ sym ( +-sym {y} {suc x}) @$\rangle$@ + y + suc x + @$\blacksquare$@ ) + + +minus-plus : { x y : @$\mathbb{N}$@ } @$\rightarrow$@ (suc x - 1) + (y + 1) @$\equiv$@ suc x + y +minus-plus {zero} {y} = +-sym {y} {1} +minus-plus {suc x} {y} = cong ( @$\lambda$@ z @$\rightarrow$@ suc z ) (minus-plus {x} {y}) + ++1@$\equiv$@suc : { x : @$\mathbb{N}$@ } @$\rightarrow$@ x + 1 @$\equiv$@ suc x ++1@$\equiv$@suc {zero} = refl ++1@$\equiv$@suc {suc x} = cong ( @$\lambda$@ z @$\rightarrow$@ suc z ) ( +1@$\equiv$@suc {x} ) + +lt : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Bool +lt x y with (suc x ) @$\leq$@? y +lt x y | yes p = true +lt x y | no @$\neg$@p = false + +pred@$\mathbb{N}$@ : {n : @$\mathbb{N}$@ } @$\rightarrow$@ lt 0 n @$\equiv$@ true @$\rightarrow$@ @$\mathbb{N}$@ +pred@$\mathbb{N}$@ {zero} () +pred@$\mathbb{N}$@ {suc n} refl = n + +pred@$\mathbb{N}$@+1=n : {n : @$\mathbb{N}$@ } @$\rightarrow$@ (less : lt 0 n @$\equiv$@ true ) @$\rightarrow$@ (pred@$\mathbb{N}$@ less) + 1 @$\equiv$@ n +pred@$\mathbb{N}$@+1=n {zero} () +pred@$\mathbb{N}$@+1=n {suc n} refl = +1@$\equiv$@suc + +suc-pred@$\mathbb{N}$@=n : {n : @$\mathbb{N}$@ } @$\rightarrow$@ (less : lt 0 n @$\equiv$@ true ) @$\rightarrow$@ suc (pred@$\mathbb{N}$@ less) @$\equiv$@ n +suc-pred@$\mathbb{N}$@=n {zero} () +suc-pred@$\mathbb{N}$@=n {suc n} refl = refl + +Equal : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Bool +Equal x y with x ≟ y +Equal x y | yes p = true +Equal x y | no @$\neg$@p = false + +_@$\Rightarrow$@_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool +false @$\Rightarrow$@ _ = true +true @$\Rightarrow$@ true = true +true @$\Rightarrow$@ false = false + +@$\Rightarrow$@t : {x : Bool} @$\rightarrow$@ x @$\Rightarrow$@ true @$\equiv$@ true +@$\Rightarrow$@t {x} with x +@$\Rightarrow$@t {x} | false = refl +@$\Rightarrow$@t {x} | true = refl + +f@$\Rightarrow$@ : {x : Bool} @$\rightarrow$@ false @$\Rightarrow$@ x @$\equiv$@ true +f@$\Rightarrow$@ {x} with x +f@$\Rightarrow$@ {x} | false = refl +f@$\Rightarrow$@ {x} | true = refl + +@$\wedge$@-pi1 : { x y : Bool } @$\rightarrow$@ x @$\wedge$@ y @$\equiv$@ true @$\rightarrow$@ x @$\equiv$@ true +@$\wedge$@-pi1 {x} {y} eq with x | y | eq +@$\wedge$@-pi1 {x} {y} eq | false | b | () +@$\wedge$@-pi1 {x} {y} eq | true | false | () +@$\wedge$@-pi1 {x} {y} eq | true | true | refl = refl + +@$\wedge$@-pi2 : { x y : Bool } @$\rightarrow$@ x @$\wedge$@ y @$\equiv$@ true @$\rightarrow$@ y @$\equiv$@ true +@$\wedge$@-pi2 {x} {y} eq with x | y | eq +@$\wedge$@-pi2 {x} {y} eq | false | b | () +@$\wedge$@-pi2 {x} {y} eq | true | false | () +@$\wedge$@-pi2 {x} {y} eq | true | true | refl = refl + +@$\wedge$@true : { x : Bool } @$\rightarrow$@ x @$\wedge$@ true @$\equiv$@ x +@$\wedge$@true {x} with x +@$\wedge$@true {x} | false = refl +@$\wedge$@true {x} | true = refl + +true@$\wedge$@ : { x : Bool } @$\rightarrow$@ true @$\wedge$@ x @$\equiv$@ x +true@$\wedge$@ {x} with x +true@$\wedge$@ {x} | false = refl +true@$\wedge$@ {x} | true = refl +bool-case : ( x : Bool ) { p : Set } @$\rightarrow$@ ( x @$\equiv$@ true @$\rightarrow$@ p ) @$\rightarrow$@ ( x @$\equiv$@ false @$\rightarrow$@ p ) @$\rightarrow$@ p +bool-case x T F with x +bool-case x T F | false = F refl +bool-case x T F | true = T refl + +impl@$\Rightarrow$@ : {x y : Bool} @$\rightarrow$@ (x @$\equiv$@ true @$\rightarrow$@ y @$\equiv$@ true ) @$\rightarrow$@ x @$\Rightarrow$@ y @$\equiv$@ true +impl@$\Rightarrow$@ {x} {y} p = bool-case x (@$\lambda$@ x=t @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + x @$\Rightarrow$@ y + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ x @$\Rightarrow$@ z ) (p x=t ) @$\rangle$@ + x @$\Rightarrow$@ true + @$\equiv$@@$\langle$@ @$\Rightarrow$@t @$\rangle$@ + true + @$\blacksquare$@ + ) ( @$\lambda$@ x=f @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + x @$\Rightarrow$@ y + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ z @$\Rightarrow$@ y ) x=f @$\rangle$@ + true + @$\blacksquare$@ + ) + +Equal@$\rightarrow$@@$\equiv$@ : { x y : @$\mathbb{N}$@ } @$\rightarrow$@ Equal x y @$\equiv$@ true @$\rightarrow$@ x @$\equiv$@ y +Equal@$\rightarrow$@@$\equiv$@ {x} {y} eq with x ≟ y +Equal@$\rightarrow$@@$\equiv$@ {x} {y} refl | yes refl = refl +Equal@$\rightarrow$@@$\equiv$@ {x} {y} () | no @$\neg$@p + +open import Data.Empty + +@$\equiv$@@$\rightarrow$@Equal : { x y : @$\mathbb{N}$@ } @$\rightarrow$@ x @$\equiv$@ y @$\rightarrow$@ Equal x y @$\equiv$@ true +@$\equiv$@@$\rightarrow$@Equal {x} {.x} refl with x ≟ x +@$\equiv$@@$\rightarrow$@Equal {x} {.x} refl | yes refl = refl +@$\equiv$@@$\rightarrow$@Equal {x} {.x} refl | no @$\neg$@p = @$\bot$@-elim ( @$\neg$@p refl )
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileConvPSemSound.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,4 @@ +whileConvPSemSound : {l : Level} → (input : Envc) → ((vari input ≡ 0) ∧ (varn input ≡ c)) implies (varn input + vari input ≡ c10 input) +whileConvPSemSound input = proof λ x → (conversion input x) where + conversion : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env + conversion e record { pi1 = refl ; pi2 = refl } = +zero
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileConvPSemSound.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,4 @@ +whileConvPSemSound : {l : Level} @$\rightarrow$@ (input : Envc) @$\rightarrow$@ ((vari input @$\equiv$@ 0) @$\wedge$@ (varn input @$\equiv$@ c)) implies (varn input + vari input @$\equiv$@ c10 input) +whileConvPSemSound input = proof @$\lambda$@ x @$\rightarrow$@ (conversion input x) where + conversion : (env : Envc ) @$\rightarrow$@ (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) @$\rightarrow$@ varn env + vari env @$\equiv$@ c10 env + conversion e record { pi1 = refl ; pi2 = refl } = +zero
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileLoopPSem.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,21 @@ +whileLoopPSem : {l : Level} {t : Set l} → (input : Envc ) → (vari input) + (varn input) ≡ (c10 input) +→ (next : (output : Envc ) → ((vari input) + (varn input) ≡ (c10 input) ) implies ((vari output) + (varn output) ≡ (c10 output)) → t) +→ (exit : (output : Envc ) → ((vari input) + (varn input) ≡ (c10 input) ) implies ((vari output ≡ c10 output)) → t) → t +whileLoopPSem env s next exit with varn env | s +... | zero | _ = exit env (proof (λ z → z)) +... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof λ x → +-suc varn (vari env) ) + + +loopPPSem : (input output : Envc ) → output ≡ loopPP (varn input) input refl + → (vari input) + (varn input) ≡ (c10 input) → ((vari input) + (varn input) ≡ (c10 input) ) implies ((vari output ≡ c10 output)) +loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p + where + lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env) + lem n env = +-suc (n) (vari env) + loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) → (loopeq : output ≡ loopPP n current eq) + → ((vari current) + (varn current) ≡ (c10 current) ) → ((vari current) + (varn current) ≡ (c10 current) ) implies ((vari output ≡ c10 output)) + loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) + loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = + whileLoopPSem current refl + (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileLoopPSem.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,21 @@ +whileLoopPSem : {l : Level} {t : Set l} @$\rightarrow$@ (input : Envc ) @$\rightarrow$@ (vari input) + (varn input) @$\equiv$@ (c10 input) +@$\rightarrow$@ (next : (output : Envc ) @$\rightarrow$@ ((vari input) + (varn input) @$\equiv$@ (c10 input) ) implies ((vari output) + (varn output) @$\equiv$@ (c10 output)) @$\rightarrow$@ t) +@$\rightarrow$@ (exit : (output : Envc ) @$\rightarrow$@ ((vari input) + (varn input) @$\equiv$@ (c10 input) ) implies ((vari output @$\equiv$@ c10 output)) @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoopPSem env s next exit with varn env | s +... | zero | _ = exit env (proof (@$\lambda$@ z @$\rightarrow$@ z)) +... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof @$\lambda$@ x @$\rightarrow$@ +-suc varn (vari env) ) + + +loopPPSem : (input output : Envc ) @$\rightarrow$@ output @$\equiv$@ loopPP (varn input) input refl + @$\rightarrow$@ (vari input) + (varn input) @$\equiv$@ (c10 input) @$\rightarrow$@ ((vari input) + (varn input) @$\equiv$@ (c10 input) ) implies ((vari output @$\equiv$@ c10 output)) +loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p + where + lem : (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc) @$\rightarrow$@ n + suc (vari env) @$\equiv$@ suc (n + vari env) + lem n env = +-suc (n) (vari env) + loopPPSemInduct : (n : @$\mathbb{N}$@) @$\rightarrow$@ (current : Envc) @$\rightarrow$@ (eq : n @$\equiv$@ varn current) @$\rightarrow$@ (loopeq : output @$\equiv$@ loopPP n current eq) + @$\rightarrow$@ ((vari current) + (varn current) @$\equiv$@ (c10 current) ) @$\rightarrow$@ ((vari current) + (varn current) @$\equiv$@ (c10 current) ) implies ((vari output @$\equiv$@ c10 output)) + loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (@$\lambda$@ x @$\rightarrow$@ refl) + loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = + whileLoopPSem current refl + (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileLoopPSemSound.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,20 @@ +loopPPSem : (input output : Envc ) → output ≡ loopPP (varn input) input refl + → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) +loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p + where + lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env) + lem n env = +-suc (n) (vari env) + loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) → (loopeq : output ≡ loopPP n current eq) + → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output) + loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) + loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = + whileLoopPSem current refl + (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + + +whileLoopPSemSound : {l : Level} → (input output : Envc ) + → (varn input + vari input ≡ c10 input) + → output ≡ loopPP (varn input) input refl + → (varn input + vari input ≡ c10 input) implies (vari output ≡ c10 output) +whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileLoopPSemSound.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,20 @@ +loopPPSem : (input output : Envc ) @$\rightarrow$@ output @$\equiv$@ loopPP (varn input) input refl + @$\rightarrow$@ (whileTestStateP s2 input ) @$\rightarrow$@ (whileTestStateP s2 input ) implies (whileTestStateP sf output) +loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p + where + lem : (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc) @$\rightarrow$@ n + suc (vari env) @$\equiv$@ suc (n + vari env) + lem n env = +-suc (n) (vari env) + loopPPSemInduct : (n : @$\mathbb{N}$@) @$\rightarrow$@ (current : Envc) @$\rightarrow$@ (eq : n @$\equiv$@ varn current) @$\rightarrow$@ (loopeq : output @$\equiv$@ loopPP n current eq) + @$\rightarrow$@ (whileTestStateP s2 current ) @$\rightarrow$@ (whileTestStateP s2 current ) implies (whileTestStateP sf output) + loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (@$\lambda$@ x @$\rightarrow$@ refl) + loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = + whileLoopPSem current refl + (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + + +whileLoopPSemSound : {l : Level} @$\rightarrow$@ (input output : Envc ) + @$\rightarrow$@ (varn input + vari input @$\equiv$@ c10 input) + @$\rightarrow$@ output @$\equiv$@ loopPP (varn input) input refl + @$\rightarrow$@ (varn input + vari input @$\equiv$@ c10 input) implies (vari output @$\equiv$@ c10 output) +whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileTestGears.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,276 @@ +module whileTestGears where + +open import Function +open import Data.Nat +open import Data.Bool hiding ( _≟_ ; _≤?_ ; _≤_ ; _<_) +open import Data.Product +open import Level renaming ( suc to succ ; zero to Zero ) +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Relation.Binary.PropositionalEquality +open import Agda.Builtin.Unit + +open import utilities +open _/\_ + +-- original codeGear (with non terminatinng ) + +record Env : Set (succ Zero) where + field + varn : ℕ + vari : ℕ +open Env + +whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t +whileTest c10 next = next (record {varn = c10 ; vari = 0 } ) + +{-# TERMINATING #-} +whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t +whileLoop env next with lt 0 (varn env) +whileLoop env next | false = next env +whileLoop env next | true = + whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next + +test1 : Env +test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 )) + +proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 )) +proof1 = refl + +-- codeGear with pre-condtion and post-condition +-- +-- ↓PostCondition +whileTest' : {l : Level} {t : Set l} → {c10 : ℕ } → (Code : (env : Env ) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t +whileTest' {_} {_} {c10} next = next env proof2 + where + env : Env + env = record {vari = 0 ; varn = c10 } + proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition + proof2 = record {pi1 = refl ; pi2 = refl} + + +open import Data.Empty +open import Data.Nat.Properties + + +{-# TERMINATING #-} -- ↓PreCondition(Invaliant) +whileLoop' : {l : Level} {t : Set l} → (env : Env ) → {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env → t) → t +whileLoop' env proof next with ( suc zero ≤? (varn env) ) +whileLoop' env proof next | no p = next env +whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next + where + env1 = record env {varn = (varn env) - 1 ; vari = (vari env) + 1} + 1<0 : 1 ≤ zero → ⊥ + 1<0 () + proof3 : (suc zero ≤ (varn env)) → varn env1 + vari env1 ≡ c10 + proof3 (s≤s lt) with varn env + proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p) + proof3 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in + begin + n' + (vari env + 1) + ≡⟨ cong ( λ z → n' + z ) ( +-sym {vari env} {1} ) ⟩ + n' + (1 + vari env ) + ≡⟨ sym ( +-assoc (n') 1 (vari env) ) ⟩ + (n' + 1) + vari env + ≡⟨ cong ( λ z → z + vari env ) +1≡suc ⟩ + (suc n' ) + vari env + ≡⟨⟩ + varn env + vari env + ≡⟨ proof ⟩ + c10 + ∎ + +-- Condition to Invariant +conversion1 : {l : Level} {t : Set l } → (env : Env ) → {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) + → (Code : (env1 : Env ) → (varn env1 + vari env1 ≡ c10) → t) → t +conversion1 env {c10} p1 next = next env proof4 + where + proof4 : varn env + vari env ≡ c10 + proof4 = let open ≡-Reasoning in + begin + varn env + vari env + ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ + c10 + vari env + ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ + c10 + 0 + ≡⟨ +-sym {c10} {0} ⟩ + c10 + ∎ + +-- all proofs are connected +proofGears : {c10 : ℕ } → Set +proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) + +-- +-- codeGear with loop step and closed environment +-- + +open import Relation.Binary + +record Envc : Set (succ Zero) where + field + c10 : ℕ + varn : ℕ + vari : ℕ +open Envc + +whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Envc → t) → t +whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } ) + +whileLoopP : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t +whileLoopP env next exit with <-cmp 0 (varn env) +whileLoopP env next exit | tri≈ ¬a b ¬c = exit env +whileLoopP env next exit | tri< a ¬b ¬c = + next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) + +-- equivalent of whileLoopP but it looks like an induction on varn +whileLoopP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc) → (n ≡ varn env) → (next : Envc → t) → (exit : Envc → t) → t +whileLoopP' zero env refl _ exit = exit env +whileLoopP' (suc n) env refl next _ = next (record {c10 = (c10 env) ; varn = varn env ; vari = suc (vari env) }) + +-- normal loop without termination +{-# TERMINATING #-} +loopP : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t +loopP env exit = whileLoopP env (λ env → loopP env exit ) exit + +whileTestPCall : (c10 : ℕ ) → Envc +whileTestPCall c10 = whileTestP {_} {_} c10 (λ env → loopP env (λ env → env)) + +-- +-- codeGears with states of condition +-- +data whileTestState : Set where + s1 : whileTestState + s2 : whileTestState + sf : whileTestState + +whileTestStateP : whileTestState → Envc → Set +whileTestStateP s1 env = (vari env ≡ 0) /\ (varn env ≡ c10 env) +whileTestStateP s2 env = (varn env + vari env ≡ c10 env) +whileTestStateP sf env = (vari env ≡ c10 env) + +whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t +whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where + env : Envc + env = whileTestP c10 ( λ env → env ) + +whileLoopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env + → (next : (env : Envc ) → whileTestStateP s2 env → t) + → (exit : (env : Envc ) → whileTestStateP sf env → t) → t +whileLoopPwP env s next exit with <-cmp 0 (varn env) +whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env (lem (sym b) s) + where + lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env + lem refl refl = refl +whileLoopPwP env s next exit | tri< a ¬b ¬c = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a) + where + 1<0 : 1 ≤ zero → ⊥ + 1<0 () + proof5 : (suc zero ≤ (varn env)) → (varn env - 1) + (vari env + 1) ≡ c10 env + proof5 (s≤s lt) with varn env + proof5 (s≤s z≤n) | zero = ⊥-elim (1<0 a) + proof5 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in + begin + n' + (vari env + 1) + ≡⟨ cong ( λ z → n' + z ) ( +-sym {vari env} {1} ) ⟩ + n' + (1 + vari env ) + ≡⟨ sym ( +-assoc (n') 1 (vari env) ) ⟩ + (n' + 1) + vari env + ≡⟨ cong ( λ z → z + vari env ) +1≡suc ⟩ + (suc n' ) + vari env + ≡⟨⟩ + varn env + vari env + ≡⟨ s ⟩ + c10 env + ∎ + + +whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env + → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env → t) + → (exit : (env : Envc ) → whileTestStateP sf env → t) → t +whileLoopPwP' zero env refl refl next exit = exit env refl +whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) + + +{-# TERMINATING #-} +loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t +loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit + + +loopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t +loopPwP' zero env refl refl exit = exit env refl +loopPwP' (suc n) env refl refl exit = whileLoopPwP' (suc n) env refl refl (λ env x y → loopPwP' n env x y exit) exit + + +loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) → loopPwP' n env (sym eq) seq λ env₁ x → (vari env₁ ≡ c10 env₁) +loopHelper zero env eq refl rewrite eq = refl +loopHelper (suc n) env eq refl rewrite eq = loopHelper n (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env)) + + +-- all codtions are correctly connected and required condtion is proved in the continuation +-- use required condition as t in (env → t) → t +-- +whileTestPCallwP : (c : ℕ ) → Set +whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c10 env ) ) where + conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero + + +whileTestPCallwP' : (c : ℕ ) → Set +whileTestPCallwP' c = whileTestPwP {_} {_} c (λ env s → loopPwP' (varn env) env refl (conv env s) ( λ env s → vari env ≡ c10 env ) ) where + conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero + +helperCallwP : (c : ℕ) → whileTestPCallwP' c +helperCallwP c = whileTestPwP {_} {_} c (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero) + +-- +-- Using imply relation to make soundness explicit +-- termination is shown by induction on varn +-- + +data _implies_ (A B : Set ) : Set (succ Zero) where + proof : ( A → B ) → A implies B + +whileTestPSem : (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) ) +whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } ) + +whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c)) +whileTestPSemSound c output refl = whileTestPSem c + + +whileConvPSemSound : {l : Level} → (input : Envc) → (whileTestStateP s1 input ) implies (whileTestStateP s2 input) +whileConvPSemSound input = proof λ x → (conv input x) where + conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero + +loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc +loopPP zero input refl = input +loopPP (suc n) input refl = + loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl + +whileLoopPSem : {l : Level} {t : Set l} → (input : Envc ) → whileTestStateP s2 input + → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → t) + → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) → t) → t +whileLoopPSem env s next exit with varn env | s +... | zero | _ = exit env (proof (λ z → z)) +... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof λ x → +-suc varn (vari env) ) + +loopPPSem : (input output : Envc ) → output ≡ loopPP (varn input) input refl + → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) +loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p + where + lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env) + lem n env = +-suc (n) (vari env) + loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) → (loopeq : output ≡ loopPP n current eq) + → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output) + loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) + loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = + whileLoopPSem current refl + (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + +whileLoopPSemSound : {l : Level} → (input output : Envc ) + → whileTestStateP s2 input + → output ≡ loopPP (varn input) input refl + → (whileTestStateP s2 input ) implies ( whileTestStateP sf output ) +whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileTestGears.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,276 @@ +module whileTestGears where + +open import Function +open import Data.Nat +open import Data.Bool hiding ( _@$\stackrel{?}{=}$@_ ; _@$\leq$@?_ ; _@$\leq$@_ ; _<_) +open import Data.Product +open import Level renaming ( suc to succ ; zero to Zero ) +open import Relation.Nullary using (@$\neg$@_; Dec; yes; no) +open import Relation.Binary.PropositionalEquality +open import Agda.Builtin.Unit + +open import utilities +open _@$\wedge$@_ + +-- original codeGear (with non terminatinng ) + +record Env : Set (succ Zero) where + field + varn : @$\mathbb{N}$@ + vari : @$\mathbb{N}$@ +open Env + +whileTest : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t +whileTest c10 next = next (record {varn = c10 ; vari = 0 } ) + +{-@$\#$@ TERMINATING @$\#$@-} +whileLoop : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoop env next with lt 0 (varn env) +whileLoop env next | false = next env +whileLoop env next | true = + whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next + +test1 : Env +test1 = whileTest 10 (@$\lambda$@ env @$\rightarrow$@ whileLoop env (@$\lambda$@ env1 @$\rightarrow$@ env1 )) + +proof1 : whileTest 10 (@$\lambda$@ env @$\rightarrow$@ whileLoop env (@$\lambda$@ e @$\rightarrow$@ (vari e) @$\equiv$@ 10 )) +proof1 = refl + +-- codeGear with pre-condtion and post-condition +-- +-- ↓PostCondition +whileTest' : {l : Level} {t : Set l} @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ (Code : (env : Env ) @$\rightarrow$@ ((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) @$\wedge$@ ((varn env) @$\equiv$@ c10) -- PostCondition + proof2 = record {pi1 = refl ; pi2 = refl} + + +open import Data.Empty +open import Data.Nat.Properties + + +{-@$\#$@ TERMINATING @$\#$@-} -- ↓PreCondition(Invaliant) +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 +whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next + where + env1 = record env {varn = (varn env) - 1 ; vari = (vari env) + 1} + 1<0 : 1 @$\leq$@ zero @$\rightarrow$@ @$\bot$@ + 1<0 () + proof3 : (suc zero @$\leq$@ (varn env)) @$\rightarrow$@ varn env1 + vari env1 @$\equiv$@ c10 + proof3 (s@$\leq$@s lt) with varn env + proof3 (s@$\leq$@s z@$\leq$@n) | zero = @$\bot$@-elim (1<0 p) + proof3 (s@$\leq$@s (z@$\leq$@n {n'}) ) | suc n = let open @$\equiv$@-Reasoning in + begin + n' + (vari env + 1) + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ n' + z ) ( +-sym {vari env} {1} ) @$\rangle$@ + n' + (1 + vari env ) + @$\equiv$@@$\langle$@ sym ( +-assoc (n') 1 (vari env) ) @$\rangle$@ + (n' + 1) + vari env + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ z + vari env ) +1@$\equiv$@suc @$\rangle$@ + (suc n' ) + vari env + @$\equiv$@@$\langle$@@$\rangle$@ + varn env + vari env + @$\equiv$@@$\langle$@ proof @$\rangle$@ + c10 + @$\blacksquare$@ + +-- Condition to Invariant +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 + proof4 : varn env + vari env @$\equiv$@ c10 + proof4 = let open @$\equiv$@-Reasoning in + begin + varn env + vari env + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n @$\rightarrow$@ n + vari env ) (pi2 p1 ) @$\rangle$@ + c10 + vari env + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n @$\rightarrow$@ c10 + n ) (pi1 p1 ) @$\rangle$@ + c10 + 0 + @$\equiv$@@$\langle$@ +-sym {c10} {0} @$\rangle$@ + c10 + @$\blacksquare$@ + +-- all proofs are connected +proofGears : {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ Set +proofGears {c10} = whileTest' {_} {_} {c10} (@$\lambda$@ n p1 @$\rightarrow$@ conversion1 n p1 (@$\lambda$@ n1 p2 @$\rightarrow$@ whileLoop' n1 p2 (@$\lambda$@ n2 @$\rightarrow$@ ( vari n2 @$\equiv$@ c10 )))) + +-- +-- codeGear with loop step and closed environment +-- + +open import Relation.Binary + +record Envc : Set (succ Zero) where + field + c10 : @$\mathbb{N}$@ + varn : @$\mathbb{N}$@ + vari : @$\mathbb{N}$@ +open Envc + +whileTestP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (Code : Envc @$\rightarrow$@ t) @$\rightarrow$@ t +whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } ) + +whileLoopP : {l : Level} {t : Set l} @$\rightarrow$@ Envc @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoopP env next exit with <-cmp 0 (varn env) +whileLoopP env next exit | tri@$\thickapprox$@ @$\neg$@a b @$\neg$@c = exit env +whileLoopP env next exit | tri< a @$\neg$@b @$\neg$@c = + next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) + +-- equivalent of whileLoopP but it looks like an induction on varn +whileLoopP' : {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 +whileLoopP' zero env refl _ exit = exit env +whileLoopP' (suc n) env refl next _ = next (record {c10 = (c10 env) ; varn = varn env ; vari = suc (vari env) }) + +-- normal loop without termination +{-@$\#$@ TERMINATING @$\#$@-} +loopP : {l : Level} {t : Set l} @$\rightarrow$@ Envc @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t +loopP env exit = whileLoopP env (@$\lambda$@ env @$\rightarrow$@ loopP env exit ) exit + +whileTestPCall : (c10 : @$\mathbb{N}$@ ) @$\rightarrow$@ Envc +whileTestPCall c10 = whileTestP {_} {_} c10 (@$\lambda$@ env @$\rightarrow$@ loopP env (@$\lambda$@ env @$\rightarrow$@ env)) + +-- +-- codeGears with states of condition +-- +data whileTestState : Set where + s1 : whileTestState + s2 : whileTestState + sf : whileTestState + +whileTestStateP : whileTestState @$\rightarrow$@ Envc @$\rightarrow$@ Set +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) + +whileTestPwP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ ((env : Envc ) @$\rightarrow$@ whileTestStateP s1 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 ) + +whileLoopPwP : {l : Level} {t : Set l} @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ whileTestStateP s2 env + @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ whileTestStateP s2 env @$\rightarrow$@ t) + @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoopPwP env s next exit with <-cmp 0 (varn env) +whileLoopPwP env s next exit | tri@$\thickapprox$@ @$\neg$@a b @$\neg$@c = exit env (lem (sym b) s) + where + lem : (varn env @$\equiv$@ 0) @$\rightarrow$@ (varn env + vari env @$\equiv$@ c10 env) @$\rightarrow$@ vari env @$\equiv$@ c10 env + lem refl refl = refl +whileLoopPwP env s next exit | tri< a @$\neg$@b @$\neg$@c = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a) + where + 1<0 : 1 @$\leq$@ zero @$\rightarrow$@ @$\bot$@ + 1<0 () + proof5 : (suc zero @$\leq$@ (varn env)) @$\rightarrow$@ (varn env - 1) + (vari env + 1) @$\equiv$@ c10 env + proof5 (s@$\leq$@s lt) with varn env + proof5 (s@$\leq$@s z@$\leq$@n) | zero = @$\bot$@-elim (1<0 a) + proof5 (s@$\leq$@s (z@$\leq$@n {n'}) ) | suc n = let open @$\equiv$@-Reasoning in + begin + n' + (vari env + 1) + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ n' + z ) ( +-sym {vari env} {1} ) @$\rangle$@ + n' + (1 + vari env ) + @$\equiv$@@$\langle$@ sym ( +-assoc (n') 1 (vari env) ) @$\rangle$@ + (n' + 1) + vari env + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ z + vari env ) +1@$\equiv$@suc @$\rangle$@ + (suc n' ) + vari env + @$\equiv$@@$\langle$@@$\rangle$@ + varn env + vari env + @$\equiv$@@$\langle$@ s @$\rangle$@ + c10 env + @$\blacksquare$@ + + +whileLoopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env + @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ (pred n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env @$\rightarrow$@ t) + @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoopPwP' zero env refl refl next exit = exit env refl +whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) + + +{-@$\#$@ TERMINATING @$\#$@-} +loopPwP : {l : Level} {t : Set l} @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ whileTestStateP s2 env @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env @$\rightarrow$@ t) @$\rightarrow$@ t +loopPwP env s exit = whileLoopPwP env s (@$\lambda$@ env s @$\rightarrow$@ loopPwP env s exit ) exit + + +loopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env @$\rightarrow$@ t) @$\rightarrow$@ t +loopPwP' zero env refl refl exit = exit env refl +loopPwP' (suc n) env refl refl exit = whileLoopPwP' (suc n) env refl refl (@$\lambda$@ env x y @$\rightarrow$@ loopPwP' n env x y exit) exit + + +loopHelper : (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ (eq : varn env @$\equiv$@ n) @$\rightarrow$@ (seq : whileTestStateP s2 env) @$\rightarrow$@ loopPwP' n env (sym eq) seq @$\lambda$@ env@$\_{1}$@ x @$\rightarrow$@ (vari env@$\_{1}$@ @$\equiv$@ c10 env@$\_{1}$@) +loopHelper zero env eq refl rewrite eq = refl +loopHelper (suc n) env eq refl rewrite eq = loopHelper n (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env)) + + +-- all codtions are correctly connected and required condtion is proved in the continuation +-- use required condition as t in (env @$\rightarrow$@ t) @$\rightarrow$@ t +-- +whileTestPCallwP : (c : @$\mathbb{N}$@ ) @$\rightarrow$@ Set +whileTestPCallwP c = whileTestPwP {_} {_} c ( @$\lambda$@ env s @$\rightarrow$@ loopPwP env (conv env s) ( @$\lambda$@ env s @$\rightarrow$@ vari env @$\equiv$@ c10 env ) ) where + conv : (env : Envc ) @$\rightarrow$@ (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) @$\rightarrow$@ varn env + vari env @$\equiv$@ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero + + +whileTestPCallwP' : (c : @$\mathbb{N}$@ ) @$\rightarrow$@ Set +whileTestPCallwP' c = whileTestPwP {_} {_} c (@$\lambda$@ env s @$\rightarrow$@ loopPwP' (varn env) env refl (conv env s) ( @$\lambda$@ env s @$\rightarrow$@ vari env @$\equiv$@ c10 env ) ) where + conv : (env : Envc ) @$\rightarrow$@ (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) @$\rightarrow$@ varn env + vari env @$\equiv$@ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero + +helperCallwP : (c : @$\mathbb{N}$@) @$\rightarrow$@ whileTestPCallwP' c +helperCallwP c = whileTestPwP {_} {_} c (@$\lambda$@ env s @$\rightarrow$@ loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero) + +-- +-- Using imply relation to make soundness explicit +-- termination is shown by induction on varn +-- + +data _implies_ (A B : Set ) : Set (succ Zero) where + proof : ( A @$\rightarrow$@ B ) @$\rightarrow$@ A implies B + +whileTestPSem : (c : @$\mathbb{N}$@) @$\rightarrow$@ whileTestP c ( @$\lambda$@ env @$\rightarrow$@ @$\top$@ implies (whileTestStateP s1 env) ) +whileTestPSem c = proof ( @$\lambda$@ _ @$\rightarrow$@ record { pi1 = refl ; pi2 = refl } ) + +whileTestPSemSound : (c : @$\mathbb{N}$@ ) (output : Envc ) @$\rightarrow$@ output @$\equiv$@ whileTestP c (@$\lambda$@ e @$\rightarrow$@ e) @$\rightarrow$@ @$\top$@ implies ((vari output @$\equiv$@ 0) @$\wedge$@ (varn output @$\equiv$@ c)) +whileTestPSemSound c output refl = whileTestPSem c + + +whileConvPSemSound : {l : Level} @$\rightarrow$@ (input : Envc) @$\rightarrow$@ (whileTestStateP s1 input ) implies (whileTestStateP s2 input) +whileConvPSemSound input = proof @$\lambda$@ x @$\rightarrow$@ (conv input x) where + conv : (env : Envc ) @$\rightarrow$@ (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) @$\rightarrow$@ varn env + vari env @$\equiv$@ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero + +loopPP : (n : @$\mathbb{N}$@) @$\rightarrow$@ (input : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn input) @$\rightarrow$@ Envc +loopPP zero input refl = input +loopPP (suc n) input refl = + loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl + +whileLoopPSem : {l : Level} {t : Set l} @$\rightarrow$@ (input : Envc ) @$\rightarrow$@ whileTestStateP s2 input + @$\rightarrow$@ (next : (output : Envc ) @$\rightarrow$@ (whileTestStateP s2 input ) implies (whileTestStateP s2 output) @$\rightarrow$@ t) + @$\rightarrow$@ (exit : (output : Envc ) @$\rightarrow$@ (whileTestStateP s2 input ) implies (whileTestStateP sf output) @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoopPSem env s next exit with varn env | s +... | zero | _ = exit env (proof (@$\lambda$@ z @$\rightarrow$@ z)) +... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof @$\lambda$@ x @$\rightarrow$@ +-suc varn (vari env) ) + +loopPPSem : (input output : Envc ) @$\rightarrow$@ output @$\equiv$@ loopPP (varn input) input refl + @$\rightarrow$@ (whileTestStateP s2 input ) @$\rightarrow$@ (whileTestStateP s2 input ) implies (whileTestStateP sf output) +loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p + where + lem : (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc) @$\rightarrow$@ n + suc (vari env) @$\equiv$@ suc (n + vari env) + lem n env = +-suc (n) (vari env) + loopPPSemInduct : (n : @$\mathbb{N}$@) @$\rightarrow$@ (current : Envc) @$\rightarrow$@ (eq : n @$\equiv$@ varn current) @$\rightarrow$@ (loopeq : output @$\equiv$@ loopPP n current eq) + @$\rightarrow$@ (whileTestStateP s2 current ) @$\rightarrow$@ (whileTestStateP s2 current ) implies (whileTestStateP sf output) + loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (@$\lambda$@ x @$\rightarrow$@ refl) + loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = + whileLoopPSem current refl + (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + +whileLoopPSemSound : {l : Level} @$\rightarrow$@ (input output : Envc ) + @$\rightarrow$@ whileTestStateP s2 input + @$\rightarrow$@ output @$\equiv$@ loopPP (varn input) input refl + @$\rightarrow$@ (whileTestStateP s2 input ) implies ( whileTestStateP sf output ) +whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileTestPSem.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,3 @@ +whileTestPSem : (c : ℕ) → whileTestP c + ( λ env → ⊤ implies (vari env ≡ 0) ∧ (varn env ≡ c10 env) ) +whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } )
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileTestPSem.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,3 @@ +whileTestPSem : (c : @$\mathbb{N}$@) @$\rightarrow$@ whileTestP c + ( @$\lambda$@ env @$\rightarrow$@ ⊤ implies (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) ) +whileTestPSem c = proof ( @$\lambda$@ _ @$\rightarrow$@ record { pi1 = refl ; pi2 = refl } )
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileTestPrim.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,71 @@ +module whileTestPrim where + +open import Function +open import Data.Nat +open import Data.Bool hiding ( _≟_ ) +open import Level renaming ( suc to succ ; zero to Zero ) +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Relation.Binary.PropositionalEquality + +open import utilities hiding ( _/\_ ) + +record Env : Set where + field + varn : ℕ + vari : ℕ +open Env + +PrimComm : Set +PrimComm = Env → Env + +Cond : Set +Cond = (Env → Bool) + +Axiom : Cond -> PrimComm -> Cond -> Set +Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true + +Tautology : Cond -> Cond -> Set +Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true + +_and_ : Cond -> Cond -> Cond +x and y = λ env → x env ∧ y env + +neg : Cond -> Cond +neg x = λ env → not ( x env ) + +open import Hoare PrimComm Cond Axiom Tautology _and_ neg + +--------------------------- + +program : ℕ → Comm +program c10 = + Seq ( PComm (λ env → record env {varn = c10})) + $ 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)} )) + +simple : ℕ → Comm +simple c10 = + Seq ( PComm (λ env → record env {varn = c10})) + $ PComm (λ env → record env {vari = 0}) + +{-# TERMINATING #-} +interpret : Env → Comm → Env +interpret env Skip = env +interpret env Abort = env +interpret env (PComm x) = x env +interpret env (Seq comm comm1) = interpret (interpret env comm) comm1 +interpret env (If x then else) with x env +... | true = interpret env then +... | false = interpret env else +interpret env (While x comm) with x env +... | true = interpret (interpret env comm) (While x comm) +... | false = env + +test1 : Env +test1 = interpret ( record { vari = 0 ; varn = 0 } ) (program 10) + + +tests : Env +tests = interpret ( record { vari = 0 ; varn = 0 } ) (simple 10)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileTestPrim.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,71 @@ +module whileTestPrim where + +open import Function +open import Data.Nat +open import Data.Bool hiding ( _@$\stackrel{?}{=}$@_ ) +open import Level renaming ( suc to succ ; zero to Zero ) +open import Relation.Nullary using (@$\neg$@_; Dec; yes; no) +open import Relation.Binary.PropositionalEquality + +open import utilities hiding ( _@$\wedge$@_ ) + +record Env : Set where + field + varn : @$\mathbb{N}$@ + vari : @$\mathbb{N}$@ +open Env + +PrimComm : Set +PrimComm = Env @$\rightarrow$@ Env + +Cond : Set +Cond = (Env @$\rightarrow$@ Bool) + +Axiom : Cond @$\rightarrow$@ PrimComm @$\rightarrow$@ Cond @$\rightarrow$@ Set +Axiom pre comm post = @$\forall$@ (env : Env) @$\rightarrow$@ (pre env) @$\Rightarrow$@ ( post (comm env)) @$\equiv$@ true + +Tautology : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Set +Tautology pre post = @$\forall$@ (env : Env) @$\rightarrow$@ (pre env) @$\Rightarrow$@ (post env) @$\equiv$@ true + +_and_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond +x and y = @$\lambda$@ env @$\rightarrow$@ x env @$\wedge$@ y env + +neg : Cond @$\rightarrow$@ Cond +neg x = @$\lambda$@ env @$\rightarrow$@ not ( x env ) + +open import Hoare PrimComm Cond Axiom Tautology _and_ neg + +--------------------------- + +program : @$\mathbb{N}$@ @$\rightarrow$@ Comm +program c10 = + Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10})) + $ Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0})) + $ While (@$\lambda$@ env @$\rightarrow$@ lt zero (varn env ) ) + (Seq (PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = ((vari env) + 1)} )) + $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = ((varn env) - 1)} )) + +simple : @$\mathbb{N}$@ @$\rightarrow$@ Comm +simple c10 = + Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10})) + $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0}) + +{-@$\#$@ TERMINATING @$\#$@-} +interpret : Env @$\rightarrow$@ Comm @$\rightarrow$@ Env +interpret env Skip = env +interpret env Abort = env +interpret env (PComm x) = x env +interpret env (Seq comm comm1) = interpret (interpret env comm) comm1 +interpret env (If x then else) with x env +... | true = interpret env then +... | false = interpret env else +interpret env (While x comm) with x env +... | true = interpret (interpret env comm) (While x comm) +... | false = env + +test1 : Env +test1 = interpret ( record { vari = 0 ; varn = 0 } ) (program 10) + + +tests : Env +tests = interpret ( record { vari = 0 ; varn = 0 } ) (simple 10)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileTestPrimProof.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,288 @@ +module whileTestPrimProof where + +open import Function +open import Data.Nat +open import Data.Bool hiding ( _≟_ ) +open import Level renaming ( suc to succ ; zero to Zero ) +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Relation.Binary.PropositionalEquality + +open import utilities hiding ( _/\_ ) +open import whileTestPrim + +open import Hoare PrimComm Cond Axiom Tautology _and_ neg + +open Env + +initCond : Cond +initCond env = true + +stmt1Cond : {c10 : ℕ} → Cond +stmt1Cond {c10} env = Equal (varn env) c10 + +init-case : {c10 : ℕ} → (env : Env) → (( λ e → true ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) ≡ true +init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl ) + +init-type : {c10 : ℕ} → Axiom (λ env → true) (λ env → record { varn = c10 ; vari = vari env }) (stmt1Cond {c10}) +init-type {c10} env = init-case env + +stmt2Cond : {c10 : ℕ} → Cond +stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) + +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 + ∎ ) + +-- simple : ℕ → Comm +-- simple c10 = +-- Seq ( PComm (λ env → record env {varn = c10})) +-- $ PComm (λ env → record env {vari = 0}) + +proofs : (c10 : ℕ) → HTProof initCond (simple c10) (stmt2Cond {c10}) +proofs c10 = + SeqRule {initCond} ( PrimRule (init-case {c10} )) + $ PrimRule {stmt1Cond} {_} {stmt2Cond} (lemma1 {c10}) + +open import Data.Empty + +open import Data.Nat.Properties + +whileInv : {c10 : ℕ} → Cond +whileInv {c10} env = Equal ((varn env) + (vari env)) c10 + +whileInv' : {c10 : ℕ} → Cond +whileInv'{c10} env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env) + +termCond : {c10 : ℕ} → Cond +termCond {c10} env = Equal (vari env) c10 + + +-- program : ℕ → Comm +-- program c10 = +-- Seq ( PComm (λ env → record env {varn = c10})) +-- $ 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)} )) + + +proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) +proof1 c10 = + SeqRule {λ e → true} ( PrimRule (init-case {c10} )) + $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) + $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( + WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} + $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 + where + lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10 + lemma21 eq = Equal→≡ (∧-pi1 eq) + lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0 + lemma22 eq = Equal→≡ (∧-pi2 eq) + lemma23 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10 + lemma23 {env} {c10} eq = let open ≡-Reasoning in + begin + varn env + vari env + ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq ) ⟩ + c10 + vari env + ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩ + c10 + 0 + ≡⟨ +-sym {c10} {0} ⟩ + 0 + c10 + ≡⟨⟩ + c10 + ∎ + lemma2 : {c10 : ℕ} → Tautology stmt2Cond whileInv + lemma2 {c10} env = bool-case (stmt2Cond env) ( + λ eq → let open ≡-Reasoning in + begin + (stmt2Cond env) ⇒ (whileInv env) + ≡⟨⟩ + (stmt2Cond env) ⇒ ( Equal (varn env + vari env) c10 ) + ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩ + (stmt2Cond env) ⇒ (Equal c10 c10) + ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl ) ⟩ + (stmt2Cond {c10} env) ⇒ true + ≡⟨ ⇒t ⟩ + true + ∎ + ) ( + λ ne → let open ≡-Reasoning in + begin + (stmt2Cond env) ⇒ (whileInv env) + ≡⟨ cong ( \ x -> x ⇒ (whileInv env) ) ne ⟩ + false ⇒ (whileInv {c10} env) + ≡⟨ f⇒ {whileInv {c10} env} ⟩ + true + ∎ + ) + lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' + lemma3 env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + whileInv' (record { varn = varn env ; vari = vari env + 1 }) + ≡⟨⟩ + Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) ) + ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond ) ⟩ + Equal (varn env + (vari env + 1)) (suc c10) ∧ true + ≡⟨ ∧true ⟩ + Equal (varn env + (vari env + 1)) (suc c10) + ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩ + Equal ((varn env + vari env) + 1) (suc c10) + ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩ + Equal (suc (varn env + vari env)) (suc c10) + ≡⟨ sym Equal+1 ⟩ + Equal ((varn env + vari env) ) c10 + ≡⟨ ∧-pi1 cond ⟩ + true + ∎ ) + lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true → Equal ((varn env - 1) + vari env) c10 ≡ true + lemma41 env {c10} c1 c2 = let open ≡-Reasoning in + begin + Equal ((varn env - 1) + vari env) c10 + ≡⟨ cong ( λ z → Equal ((z - 1 ) + vari env ) c10 ) (sym (suc-predℕ=n c2) ) ⟩ + Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10 + ≡⟨⟩ + Equal ((predℕ {varn env} c2 ) + vari env) c10 + ≡⟨ Equal+1 ⟩ + Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10) + ≡⟨ cong ( λ z → Equal (z + vari env ) (suc c10) ) (suc-predℕ=n c2 ) ⟩ + Equal (varn env + vari env) (suc c10) + ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩ + Equal (suc c10) (suc c10) + ≡⟨ ≡→Equal refl ⟩ + true + ∎ + lemma4 : {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv + lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + whileInv (record { varn = varn env - 1 ; vari = vari env }) + ≡⟨⟩ + Equal ((varn env - 1) + vari env) c10 + ≡⟨ lemma41 env (Equal→≡ (∧-pi1 cond)) (∧-pi2 cond) ⟩ + true + ∎ + ) + lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero + lemma51 z cond with varn z + lemma51 z refl | zero = refl + lemma51 z () | suc x + lemma5 : {c10 : ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond + lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in + begin + termCond env + ≡⟨⟩ + Equal (vari env) c10 + ≡⟨⟩ + Equal (zero + vari env) c10 + ≡⟨ cong ( λ z → Equal (z + vari env) c10 ) (sym ( lemma51 env ( ∧-pi2 cond ) )) ⟩ + Equal (varn env + vari env) c10 + ≡⟨ ∧-pi1 cond ⟩ + true + ∎ + ) + +--- necessary definitions for Hoare.agda ( Soundness ) + +State : Set +State = Env + +open import RelOp +module RelOpState = RelOp State + +open import Data.Product +open import Relation.Binary + +NotP : {S : Set} -> Pred S -> Pred S +NotP X s = ¬ X s + +_/\_ : Cond -> Cond -> Cond +b1 /\ b2 = b1 and b2 + +_\/_ : Cond -> Cond -> Cond +b1 \/ b2 = neg (neg b1 /\ neg b2) + +SemCond : Cond -> State -> Set +SemCond c p = c p ≡ true + +tautValid : (b1 b2 : Cond) -> Tautology b1 b2 -> + (s : State) -> SemCond b1 s -> SemCond b2 s +tautValid b1 b2 taut s cond with b1 s | b2 s | taut s +tautValid b1 b2 taut s () | false | false | refl +tautValid b1 b2 taut s _ | false | true | refl = refl +tautValid b1 b2 taut s _ | true | false | () +tautValid b1 b2 taut s _ | true | true | refl = refl + +respNeg : (b : Cond) -> (s : State) -> + Iff (SemCond (neg b) s) (¬ SemCond b s) +respNeg b s = ( left , right ) where + left : not (b s) ≡ true → (b s) ≡ true → ⊥ + left ne with b s + left refl | false = λ () + left () | true + right : ((b s) ≡ true → ⊥) → not (b s) ≡ true + right ne with b s + right ne | false = refl + right ne | true = ⊥-elim ( ne refl ) + +respAnd : (b1 b2 : Cond) -> (s : State) -> + Iff (SemCond (b1 /\ b2) s) + ((SemCond b1 s) × (SemCond b2 s)) +respAnd b1 b2 s = ( left , right ) where + left : b1 s ∧ b2 s ≡ true → (b1 s ≡ true) × (b2 s ≡ true) + left and with b1 s | b2 s + left () | false | false + left () | false | true + left () | true | false + left refl | true | true = ( refl , refl ) + right : (b1 s ≡ true) × (b2 s ≡ true) → b1 s ∧ b2 s ≡ true + right ( x1 , x2 ) with b1 s | b2 s + right (() , ()) | false | false + right (() , _) | false | true + right (_ , ()) | true | false + right (refl , refl) | true | true = refl + +PrimSemComm : ∀ {l} -> PrimComm -> Rel State l +PrimSemComm prim s1 s2 = Id State (prim s1) s2 + + + +axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) -> + (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) -> + SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2 +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref with bPre s1 | bPost (pcm s1) | ax s1 +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | () +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl + +open import HoareSoundness + Cond + PrimComm + neg + _and_ + Tautology + State + SemCond + tautValid + respNeg + respAnd + PrimSemComm + Axiom + axiomValid + +PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> + HTProof bPre cm bPost -> Satisfies bPre cm bPost +PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht + + +proofOfProgram : (c10 : ℕ) → (input output : Env ) + → initCond input ≡ true + → (SemComm (program c10) input output) + → termCond {c10} output ≡ true +proofOfProgram c10 input output ic sem = PrimSoundness (proof1 c10) input output ic sem
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileTestPrimProof.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,288 @@ +module whileTestPrimProof where + +open import Function +open import Data.Nat +open import Data.Bool hiding ( _@$\stackrel{?}{=}$@_ ) +open import Level renaming ( suc to succ ; zero to Zero ) +open import Relation.Nullary using (@$\neg$@_; Dec; yes; no) +open import Relation.Binary.PropositionalEquality + +open import utilities hiding ( _@$\wedge$@_ ) +open import whileTestPrim + +open import Hoare PrimComm Cond Axiom Tautology _and_ neg + +open Env + +initCond : Cond +initCond env = true + +stmt1Cond : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond +stmt1Cond {c10} env = Equal (varn env) c10 + +init-case : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ (env : Env) @$\rightarrow$@ (( @$\lambda$@ e @$\rightarrow$@ true @$\Rightarrow$@ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) @$\equiv$@ true +init-case {c10} _ = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ @$\equiv$@@$\rightarrow$@Equal refl ) + +init-type : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Axiom (@$\lambda$@ env @$\rightarrow$@ true) (@$\lambda$@ env @$\rightarrow$@ record { varn = c10 ; vari = vari env }) (stmt1Cond {c10}) +init-type {c10} env = init-case env + +stmt2Cond : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond +stmt2Cond {c10} env = (Equal (varn env) c10) @$\wedge$@ (Equal (vari env) 0) + +lemma1 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Axiom (stmt1Cond {c10}) (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) +lemma1 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + (Equal (varn env) c10 ) @$\wedge$@ true + @$\equiv$@@$\langle$@ @$\wedge$@true @$\rangle$@ + Equal (varn env) c10 + @$\equiv$@@$\langle$@ cond @$\rangle$@ + true + @$\blacksquare$@ ) + +-- simple : @$\mathbb{N}$@ @$\rightarrow$@ Comm +-- simple c10 = +-- Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10})) +-- $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0}) + +proofs : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ HTProof initCond (simple c10) (stmt2Cond {c10}) +proofs c10 = + SeqRule {initCond} ( PrimRule (init-case {c10} )) + $ PrimRule {stmt1Cond} {_} {stmt2Cond} (lemma1 {c10}) + +open import Data.Empty + +open import Data.Nat.Properties + +whileInv : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond +whileInv {c10} env = Equal ((varn env) + (vari env)) c10 + +whileInv' : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond +whileInv'{c10} env = Equal ((varn env) + (vari env)) (suc c10) @$\wedge$@ lt zero (varn env) + +termCond : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Cond +termCond {c10} env = Equal (vari env) c10 + + +-- program : @$\mathbb{N}$@ @$\rightarrow$@ Comm +-- program c10 = +-- Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10})) +-- $ Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0})) +-- $ While (@$\lambda$@ env @$\rightarrow$@ lt zero (varn env ) ) +-- (Seq (PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = ((vari env) + 1)} )) +-- $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = ((varn env) - 1)} )) + + +proof1 : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ HTProof initCond (program c10 ) (termCond {c10}) +proof1 c10 = + SeqRule {@$\lambda$@ e @$\rightarrow$@ true} ( PrimRule (init-case {c10} )) + $ SeqRule {@$\lambda$@ e @$\rightarrow$@ Equal (varn e) c10} ( PrimRule lemma1 ) + $ WeakeningRule {@$\lambda$@ e @$\rightarrow$@ (Equal (varn e) c10) @$\wedge$@ (Equal (vari e) 0)} lemma2 ( + WhileRule {_} {@$\lambda$@ e @$\rightarrow$@ Equal ((varn e) + (vari e)) c10} + $ SeqRule (PrimRule {@$\lambda$@ e @$\rightarrow$@ whileInv e @$\wedge$@ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 + where + lemma21 : {env : Env } @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ stmt2Cond env @$\equiv$@ true @$\rightarrow$@ varn env @$\equiv$@ c10 + lemma21 eq = Equal@$\rightarrow$@@$\equiv$@ (@$\wedge$@-pi1 eq) + lemma22 : {env : Env } @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ stmt2Cond {c10} env @$\equiv$@ true @$\rightarrow$@ vari env @$\equiv$@ 0 + lemma22 eq = Equal@$\rightarrow$@@$\equiv$@ (@$\wedge$@-pi2 eq) + lemma23 : {env : Env } @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ stmt2Cond env @$\equiv$@ true @$\rightarrow$@ varn env + vari env @$\equiv$@ c10 + lemma23 {env} {c10} eq = let open @$\equiv$@-Reasoning in + begin + varn env + vari env + @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ x + vari env ) (lemma21 eq ) @$\rangle$@ + c10 + vari env + @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ c10 + x) (lemma22 {env} {c10} eq ) @$\rangle$@ + c10 + 0 + @$\equiv$@@$\langle$@ +-sym {c10} {0} @$\rangle$@ + 0 + c10 + @$\equiv$@@$\langle$@@$\rangle$@ + c10 + @$\blacksquare$@ + lemma2 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Tautology stmt2Cond whileInv + lemma2 {c10} env = bool-case (stmt2Cond env) ( + @$\lambda$@ eq @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + (stmt2Cond env) @$\Rightarrow$@ (whileInv env) + @$\equiv$@@$\langle$@@$\rangle$@ + (stmt2Cond env) @$\Rightarrow$@ ( Equal (varn env + vari env) c10 ) + @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ (stmt2Cond {c10} env) @$\Rightarrow$@ ( Equal x c10 ) ) ( lemma23 {env} eq ) @$\rangle$@ + (stmt2Cond env) @$\Rightarrow$@ (Equal c10 c10) + @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ (stmt2Cond {c10} env) @$\Rightarrow$@ x ) (@$\equiv$@@$\rightarrow$@Equal refl ) @$\rangle$@ + (stmt2Cond {c10} env) @$\Rightarrow$@ true + @$\equiv$@@$\langle$@ @$\Rightarrow$@t @$\rangle$@ + true + @$\blacksquare$@ + ) ( + @$\lambda$@ ne @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + (stmt2Cond env) @$\Rightarrow$@ (whileInv env) + @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ x @$\Rightarrow$@ (whileInv env) ) ne @$\rangle$@ + false @$\Rightarrow$@ (whileInv {c10} env) + @$\equiv$@@$\langle$@ f@$\Rightarrow$@ {whileInv {c10} env} @$\rangle$@ + true + @$\blacksquare$@ + ) + lemma3 : Axiom (@$\lambda$@ e @$\rightarrow$@ whileInv e @$\wedge$@ lt zero (varn e)) (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = vari env + 1 }) whileInv' + lemma3 env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + whileInv' (record { varn = varn env ; vari = vari env + 1 }) + @$\equiv$@@$\langle$@@$\rangle$@ + Equal (varn env + (vari env + 1)) (suc c10) @$\wedge$@ (lt 0 (varn env) ) + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal (varn env + (vari env + 1)) (suc c10) @$\wedge$@ z ) (@$\wedge$@-pi2 cond ) @$\rangle$@ + Equal (varn env + (vari env + 1)) (suc c10) @$\wedge$@ true + @$\equiv$@@$\langle$@ @$\wedge$@true @$\rangle$@ + Equal (varn env + (vari env + 1)) (suc c10) + @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) @$\rangle$@ + Equal ((varn env + vari env) + 1) (suc c10) + @$\equiv$@@$\langle$@ cong ( \ x @$\rightarrow$@ Equal x (suc c10) ) +1@$\equiv$@suc @$\rangle$@ + Equal (suc (varn env + vari env)) (suc c10) + @$\equiv$@@$\langle$@ sym Equal+1 @$\rangle$@ + Equal ((varn env + vari env) ) c10 + @$\equiv$@@$\langle$@ @$\wedge$@-pi1 cond @$\rangle$@ + true + @$\blacksquare$@ ) + lemma41 : (env : Env ) @$\rightarrow$@ {c10 : @$\mathbb{N}$@} @$\rightarrow$@ (varn env + vari env) @$\equiv$@ (suc c10) @$\rightarrow$@ lt 0 (varn env) @$\equiv$@ true @$\rightarrow$@ Equal ((varn env - 1) + vari env) c10 @$\equiv$@ true + lemma41 env {c10} c1 c2 = let open @$\equiv$@-Reasoning in + begin + Equal ((varn env - 1) + vari env) c10 + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal ((z - 1 ) + vari env ) c10 ) (sym (suc-pred@$\mathbb{N}$@=n c2) ) @$\rangle$@ + Equal ((suc (pred@$\mathbb{N}$@ {varn env} c2 ) - 1) + vari env) c10 + @$\equiv$@@$\langle$@@$\rangle$@ + Equal ((pred@$\mathbb{N}$@ {varn env} c2 ) + vari env) c10 + @$\equiv$@@$\langle$@ Equal+1 @$\rangle$@ + Equal ((suc (pred@$\mathbb{N}$@ {varn env} c2 )) + vari env) (suc c10) + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal (z + vari env ) (suc c10) ) (suc-pred@$\mathbb{N}$@=n c2 ) @$\rangle$@ + Equal (varn env + vari env) (suc c10) + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ (Equal z (suc c10) )) c1 @$\rangle$@ + Equal (suc c10) (suc c10) + @$\equiv$@@$\langle$@ @$\equiv$@@$\rightarrow$@Equal refl @$\rangle$@ + true + @$\blacksquare$@ + lemma4 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Axiom whileInv' (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env - 1 ; vari = vari env }) whileInv + lemma4 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + whileInv (record { varn = varn env - 1 ; vari = vari env }) + @$\equiv$@@$\langle$@@$\rangle$@ + Equal ((varn env - 1) + vari env) c10 + @$\equiv$@@$\langle$@ lemma41 env (Equal@$\rightarrow$@@$\equiv$@ (@$\wedge$@-pi1 cond)) (@$\wedge$@-pi2 cond) @$\rangle$@ + true + @$\blacksquare$@ + ) + lemma51 : (z : Env ) @$\rightarrow$@ neg (@$\lambda$@ z @$\rightarrow$@ lt zero (varn z)) z @$\equiv$@ true @$\rightarrow$@ varn z @$\equiv$@ zero + lemma51 z cond with varn z + lemma51 z refl | zero = refl + lemma51 z () | suc x + lemma5 : {c10 : @$\mathbb{N}$@} @$\rightarrow$@ Tautology ((@$\lambda$@ e @$\rightarrow$@ Equal (varn e + vari e) c10) and (neg (@$\lambda$@ z @$\rightarrow$@ lt zero (varn z)))) termCond + lemma5 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in + begin + termCond env + @$\equiv$@@$\langle$@@$\rangle$@ + Equal (vari env) c10 + @$\equiv$@@$\langle$@@$\rangle$@ + Equal (zero + vari env) c10 + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ Equal (z + vari env) c10 ) (sym ( lemma51 env ( @$\wedge$@-pi2 cond ) )) @$\rangle$@ + Equal (varn env + vari env) c10 + @$\equiv$@@$\langle$@ @$\wedge$@-pi1 cond @$\rangle$@ + true + @$\blacksquare$@ + ) + +--- necessary definitions for Hoare.agda ( Soundness ) + +State : Set +State = Env + +open import RelOp +module RelOpState = RelOp State + +open import Data.Product +open import Relation.Binary + +NotP : {S : Set} @$\rightarrow$@ Pred S @$\rightarrow$@ Pred S +NotP X s = @$\neg$@ X s + +_@$\wedge$@_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond +b1 @$\wedge$@ b2 = b1 and b2 + +_\/_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond +b1 \/ b2 = neg (neg b1 @$\wedge$@ neg b2) + +SemCond : Cond @$\rightarrow$@ State @$\rightarrow$@ Set +SemCond c p = c p @$\equiv$@ true + +tautValid : (b1 b2 : Cond) @$\rightarrow$@ Tautology b1 b2 @$\rightarrow$@ + (s : State) @$\rightarrow$@ SemCond b1 s @$\rightarrow$@ SemCond b2 s +tautValid b1 b2 taut s cond with b1 s | b2 s | taut s +tautValid b1 b2 taut s () | false | false | refl +tautValid b1 b2 taut s _ | false | true | refl = refl +tautValid b1 b2 taut s _ | true | false | () +tautValid b1 b2 taut s _ | true | true | refl = refl + +respNeg : (b : Cond) @$\rightarrow$@ (s : State) @$\rightarrow$@ + Iff (SemCond (neg b) s) (@$\neg$@ SemCond b s) +respNeg b s = ( left , right ) where + left : not (b s) @$\equiv$@ true @$\rightarrow$@ (b s) @$\equiv$@ true @$\rightarrow$@ @$\bot$@ + left ne with b s + left refl | false = @$\lambda$@ () + left () | true + right : ((b s) @$\equiv$@ true @$\rightarrow$@ @$\bot$@) @$\rightarrow$@ not (b s) @$\equiv$@ true + right ne with b s + right ne | false = refl + right ne | true = @$\bot$@-elim ( ne refl ) + +respAnd : (b1 b2 : Cond) @$\rightarrow$@ (s : State) @$\rightarrow$@ + Iff (SemCond (b1 @$\wedge$@ b2) s) + ((SemCond b1 s) @$\times$@ (SemCond b2 s)) +respAnd b1 b2 s = ( left , right ) where + left : b1 s @$\wedge$@ b2 s @$\equiv$@ true @$\rightarrow$@ (b1 s @$\equiv$@ true) @$\times$@ (b2 s @$\equiv$@ true) + left and with b1 s | b2 s + left () | false | false + left () | false | true + left () | true | false + left refl | true | true = ( refl , refl ) + right : (b1 s @$\equiv$@ true) @$\times$@ (b2 s @$\equiv$@ true) @$\rightarrow$@ b1 s @$\wedge$@ b2 s @$\equiv$@ true + right ( x1 , x2 ) with b1 s | b2 s + right (() , ()) | false | false + right (() , _) | false | true + right (_ , ()) | true | false + right (refl , refl) | true | true = refl + +PrimSemComm : @$\forall$@ {l} @$\rightarrow$@ PrimComm @$\rightarrow$@ Rel State l +PrimSemComm prim s1 s2 = Id State (prim s1) s2 + + + +axiomValid : @$\forall$@ {l} @$\rightarrow$@ (bPre : Cond) @$\rightarrow$@ (pcm : PrimComm) @$\rightarrow$@ (bPost : Cond) @$\rightarrow$@ + (ax : Axiom bPre pcm bPost) @$\rightarrow$@ (s1 s2 : State) @$\rightarrow$@ + SemCond bPre s1 @$\rightarrow$@ PrimSemComm {l} pcm s1 s2 @$\rightarrow$@ SemCond bPost s2 +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref with bPre s1 | bPost (pcm s1) | ax s1 +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | () +axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl + +open import HoareSoundness + Cond + PrimComm + neg + _and_ + Tautology + State + SemCond + tautValid + respNeg + respAnd + PrimSemComm + Axiom + axiomValid + +PrimSoundness : {bPre : Cond} @$\rightarrow$@ {cm : Comm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@ + HTProof bPre cm bPost @$\rightarrow$@ Satisfies bPre cm bPost +PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht + + +proofOfProgram : (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (input output : Env ) + @$\rightarrow$@ initCond input @$\equiv$@ true + @$\rightarrow$@ (SemComm (program c10) input output) + @$\rightarrow$@ termCond {c10} output @$\equiv$@ true +proofOfProgram c10 input output ic sem = PrimSoundness (proof1 c10) input output ic sem
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileTestProof.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,65 @@ +module whileTestProof where +-- +-- Using imply relation to make soundness explicit +-- termination is shown by induction on varn +-- + +data _implies_ (A B : Set ) : Set (succ Zero) where + proof : ( A → B ) → A implies B + +implies2p : {A B : Set } → A implies B → A → B +implies2p (proof x) = x + +whileTestPSem : (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) ) +whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } ) + +SemGears : (f : {l : Level } {t : Set l } → (e0 : Envc ) → ((e : Envc) → t) → t ) → Set (succ Zero) +SemGears f = Envc → Envc → Set + +GearsUnitSound : (e0 e1 : Envc) {pre : Envc → Set} {post : Envc → Set} + → (f : {l : Level } {t : Set l } → (e0 : Envc ) → (Envc → t) → t ) + → (fsem : (e0 : Envc ) → f e0 ( λ e1 → (pre e0) implies (post e1))) + → f e0 (λ e1 → pre e0 implies post e1) +GearsUnitSound e0 e1 f fsem = fsem e0 + +whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c)) +whileTestPSemSound c output refl = proof (λ x → record { pi1 = refl ; pi2 = refl }) +-- whileTestPSem c + + +whileConvPSemSound : {l : Level} → (input : Envc) → (whileTestStateP s1 input ) implies (whileTestStateP s2 input) +whileConvPSemSound input = proof λ x → (conv input x) where + conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero + +loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc +loopPP zero input refl = input +loopPP (suc n) input refl = + loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl + +whileLoopPSem : {l : Level} {t : Set l} → (input : Envc ) → whileTestStateP s2 input + → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → t) + → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) → t) → t +whileLoopPSem env s next exit with varn env | s +... | zero | _ = exit env (proof (λ z → z)) +... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof λ x → +-suc varn (vari env) ) + +loopPPSem : (input output : Envc ) → output ≡ loopPP (varn input) input refl + → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) +loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p + where + lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env) + lem n env = +-suc (n) (vari env) + loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) → (loopeq : output ≡ loopPP n current eq) + → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output) + loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) + loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = + whileLoopPSem current refl + (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + +whileLoopPSemSound : {l : Level} → (input output : Envc ) + → whileTestStateP s2 input + → output ≡ loopPP (varn input) input refl + → (whileTestStateP s2 input ) implies ( whileTestStateP sf output ) +whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileTestProof.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,65 @@ +module whileTestProof where +-- +-- Using imply relation to make soundness explicit +-- termination is shown by induction on varn +-- + +data _implies_ (A B : Set ) : Set (succ Zero) where + proof : ( A @$\rightarrow$@ B ) @$\rightarrow$@ A implies B + +implies2p : {A B : Set } @$\rightarrow$@ A implies B @$\rightarrow$@ A @$\rightarrow$@ B +implies2p (proof x) = x + +whileTestPSem : (c : @$\mathbb{N}$@) @$\rightarrow$@ whileTestP c ( @$\lambda$@ env @$\rightarrow$@ ⊤ implies (whileTestStateP s1 env) ) +whileTestPSem c = proof ( @$\lambda$@ _ @$\rightarrow$@ record { pi1 = refl ; pi2 = refl } ) + +SemGears : (f : {l : Level } {t : Set l } @$\rightarrow$@ (e0 : Envc ) @$\rightarrow$@ ((e : Envc) @$\rightarrow$@ t) @$\rightarrow$@ t ) @$\rightarrow$@ Set (succ Zero) +SemGears f = Envc @$\rightarrow$@ Envc @$\rightarrow$@ Set + +GearsUnitSound : (e0 e1 : Envc) {pre : Envc @$\rightarrow$@ Set} {post : Envc @$\rightarrow$@ Set} + @$\rightarrow$@ (f : {l : Level } {t : Set l } @$\rightarrow$@ (e0 : Envc ) @$\rightarrow$@ (Envc @$\rightarrow$@ t) @$\rightarrow$@ t ) + @$\rightarrow$@ (fsem : (e0 : Envc ) @$\rightarrow$@ f e0 ( @$\lambda$@ e1 @$\rightarrow$@ (pre e0) implies (post e1))) + @$\rightarrow$@ f e0 (@$\lambda$@ e1 @$\rightarrow$@ pre e0 implies post e1) +GearsUnitSound e0 e1 f fsem = fsem e0 + +whileTestPSemSound : (c : @$\mathbb{N}$@ ) (output : Envc ) @$\rightarrow$@ output @$\equiv$@ whileTestP c (@$\lambda$@ e @$\rightarrow$@ e) @$\rightarrow$@ ⊤ implies ((vari output @$\equiv$@ 0) @$\wedge$@ (varn output @$\equiv$@ c)) +whileTestPSemSound c output refl = proof (@$\lambda$@ x @$\rightarrow$@ record { pi1 = refl ; pi2 = refl }) +-- whileTestPSem c + + +whileConvPSemSound : {l : Level} @$\rightarrow$@ (input : Envc) @$\rightarrow$@ (whileTestStateP s1 input ) implies (whileTestStateP s2 input) +whileConvPSemSound input = proof @$\lambda$@ x @$\rightarrow$@ (conv input x) where + conv : (env : Envc ) @$\rightarrow$@ (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env) @$\rightarrow$@ varn env + vari env @$\equiv$@ c10 env + conv e record { pi1 = refl ; pi2 = refl } = +zero + +loopPP : (n : @$\mathbb{N}$@) @$\rightarrow$@ (input : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn input) @$\rightarrow$@ Envc +loopPP zero input refl = input +loopPP (suc n) input refl = + loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl + +whileLoopPSem : {l : Level} {t : Set l} @$\rightarrow$@ (input : Envc ) @$\rightarrow$@ whileTestStateP s2 input + @$\rightarrow$@ (next : (output : Envc ) @$\rightarrow$@ (whileTestStateP s2 input ) implies (whileTestStateP s2 output) @$\rightarrow$@ t) + @$\rightarrow$@ (exit : (output : Envc ) @$\rightarrow$@ (whileTestStateP s2 input ) implies (whileTestStateP sf output) @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoopPSem env s next exit with varn env | s +... | zero | _ = exit env (proof (@$\lambda$@ z @$\rightarrow$@ z)) +... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof @$\lambda$@ x @$\rightarrow$@ +-suc varn (vari env) ) + +loopPPSem : (input output : Envc ) @$\rightarrow$@ output @$\equiv$@ loopPP (varn input) input refl + @$\rightarrow$@ (whileTestStateP s2 input ) @$\rightarrow$@ (whileTestStateP s2 input ) implies (whileTestStateP sf output) +loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p + where + lem : (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc) @$\rightarrow$@ n + suc (vari env) @$\equiv$@ suc (n + vari env) + lem n env = +-suc (n) (vari env) + loopPPSemInduct : (n : @$\mathbb{N}$@) @$\rightarrow$@ (current : Envc) @$\rightarrow$@ (eq : n @$\equiv$@ varn current) @$\rightarrow$@ (loopeq : output @$\equiv$@ loopPP n current eq) + @$\rightarrow$@ (whileTestStateP s2 current ) @$\rightarrow$@ (whileTestStateP s2 current ) implies (whileTestStateP sf output) + loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (@$\lambda$@ x @$\rightarrow$@ refl) + loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = + whileLoopPSem current refl + (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + (@$\lambda$@ output x @$\rightarrow$@ loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) + +whileLoopPSemSound : {l : Level} @$\rightarrow$@ (input output : Envc ) + @$\rightarrow$@ whileTestStateP s2 input + @$\rightarrow$@ output @$\equiv$@ loopPP (varn input) input refl + @$\rightarrow$@ (whileTestStateP s2 input ) implies ( whileTestStateP sf output ) +whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileTestSemSound.agda Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,4 @@ +whileTestPSemSound : (c : ℕ ) (output : Envc ) + → output ≡ whileTestP c (λ e → e) + → ⊤ implies ((vari output ≡ 0) ∧ (varn output ≡ c)) + whileTestPSemSound c output refl = proof (λ _ → record { pi1 = refl ; pi2 = refl })
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/whileTestSemSound.agda.replaced Mon Mar 09 11:25:49 2020 +0900 @@ -0,0 +1,4 @@ +whileTestPSemSound : (c : @$\mathbb{N}$@ ) (output : Envc ) + @$\rightarrow$@ output @$\equiv$@ whileTestP c (@$\lambda$@ e @$\rightarrow$@ e) + @$\rightarrow$@ @$\top$@ implies ((vari output @$\equiv$@ 0) @$\wedge$@ (varn output @$\equiv$@ c)) + whileTestPSemSound c output refl = proof (@$\lambda$@ _ @$\rightarrow$@ record { pi1 = refl ; pi2 = refl })
--- a/paper/thanks.tex Mon Feb 17 17:14:00 2020 +0900 +++ b/paper/thanks.tex Mon Mar 09 11:25:49 2020 +0900 @@ -1,6 +1,6 @@ \chapter*{謝辞} -本研究の遂行、本論文の作成にあたり、御多忙にも関わらず終始懇切なる御指導と御教授を賜わりました河野真治准教授に心より感謝致します。 +本研究の遂行、本論文の作成にあたり、御多忙にも関わらず終始懇切なる御指導と御教授を賜わりました、河野真治准教授に心より感謝致します。 そして、 共に研究を行い暖かな気遣いと励ましをもって支えてくれた並列信頼研究室の全てのメンバーに感謝致します。 最後に、 有意義な時間を共に過ごした理工学研究科情報工学専攻の学友、並びに物心両面で支えてくれた家族に深く感謝致します。