# HG changeset patch # User ryokka # Date 1580304977 -32400 # Node ID b5fffa8ae875d0da5232ecb6b709d2d79ea182a0 # Parent a6f371a5d33de2599ce8867d67759271c7bb8d20 fix chapter hoare diff -r a6f371a5d33d -r b5fffa8ae875 paper/Makefile --- a/paper/Makefile Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/Makefile Wed Jan 29 22:36:17 2020 +0900 @@ -24,8 +24,8 @@ %.xbb: %.pdf $(BB) $< -# %.agda.replaced: %.agda -# ruby escape_agda.rb $< +%.agda.replaced: %.agda + ruby escape_agda.rb $< # commands diff -r a6f371a5d33d -r b5fffa8ae875 paper/abstract.tex --- a/paper/abstract.tex Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/abstract.tex Wed Jan 29 22:36:17 2020 +0900 @@ -24,4 +24,4 @@ また、GearsOS の仕様確認のために CodeGear、DataGear という単位を用いた記述で Hoare Logic をベースと した while Loop プログラムを記述、その証明を行なった。 -\chapter*{Abstract} +%% \chapter*{Abstract} diff -r a6f371a5d33d -r b5fffa8ae875 paper/agda.tex --- a/paper/agda.tex Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/agda.tex Wed Jan 29 22:36:17 2020 +0900 @@ -8,9 +8,8 @@ また、定理証明支援器としての Agda について解説する。 \section{Agda の文法} - -Agda はインデントが意味を持ち、スペースの有無もチェックされる。 -コメントは \verb/-- comment/ や \verb/{-- comment --}/ のように記述される。 +Agdaはインデントが意味を持ち、スペースの有無もチェックされる。 +コメントは \verb/\-\- comment/ や \verb/{\-\- comment \-\-}/ のように記述される。 Agda のプログラムは全てモジュール内部に記述されるため、各ファイルのトップレベルにモ ジュールを定義する必要がある。トップレベルのモジュールはファイル名と同一である。 @@ -23,7 +22,7 @@ なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open import/ キーワードを使うことで展開できる。 モジュールをインポートする例をリスト~\ref{src:agda-import}に示す。 -\lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda} +\lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda.replaced} \section{Agda のデータ} @@ -37,7 +36,7 @@ Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。 Set は階層構造を持ち、型集合の集合の型を指定するには Set1 と書く -\lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda} +\lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda.replaced} Agda には C における構造体に相当するレコード型というデータも存在する、 @@ -45,7 +44,7 @@ レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。 複数の値を列挙する際は \verb/;/ で区切る。 -\lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda} +\lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda.replaced} \section{Agda の関数} @@ -58,13 +57,13 @@ 時の型は \verb/A -> (A -> B)/のように考えられる。 Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{src:agda-function}のようになる。 -\lstinputlisting[label=src:agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda} +\lstinputlisting[label=src:agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda.replaced} 引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなもので 例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。 -\lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda} +\lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced} パターンマッチでは全てのコンストラクタのパターンを含まなくてはならない。 例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。 @@ -72,14 +71,14 @@ 例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。 なお、マッチした値以外の挙動をまとめて書く際には \verb/_/ を用いることもできる。 -\lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda} +\lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda.replaced} Agda にはラムダ計算が存在している。ラムダ計算とは関数内で生成できる無名の関数であり、 \verb/\arg1 arg2 -> function body/ のように書くことができる。 例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ計算で書くとリスト~\ref{src:agda-lambda}のようになる。 関数 \verb/not-apply/ をラムダ計算を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。 -\lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda} +\lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda.replaced} Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。 スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。 @@ -87,7 +86,7 @@ これは \verb/f'/ と同様の動作をする。 \verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。 -\lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda} +\lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced} \section{定理証明支援器としての Agda} diff -r a6f371a5d33d -r b5fffa8ae875 paper/cbc.tex --- a/paper/cbc.tex Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/cbc.tex Wed Jan 29 22:36:17 2020 +0900 @@ -3,7 +3,7 @@ \chapter{Continuation based C} Continuation based C\cite{cbc} (以下 CbC) は CodeGear を処理の単位、 DataGear をデータの単位として記述するプログラミング言語である。 CbC は C 言語とほぼ同じ構文を持つが、よりアセンブラに近いプログラムを記述することになる。 CbC でのプログラミングは DataGear を CodeGear で変更し、その変更を次の CodeGear に渡して処理を実行する。 -現在 CbC の処理系には llvm/clang による実装\cite{llvm}と gcc\cite{gcc} による実装が存在する。 +現在 CbC の処理系には llvm/clang による実装 \cite{llvm} とgcc \cite{gcc} による実装が存在する。 本章は CbC についての説明を行う。 @@ -57,8 +57,7 @@ CbC で必要な CodeGear 、 DataGear を参照する際は Context を通してアクセスする必要がある。 \section{Meta Gears} -Meta Gear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための CodeGear である。 +Meta Gear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。 例えば、 CodeGear を実行する際、必要な DataGear を Context を通して取得する必要があるが、ユーザーが Context から直接データを扱える状態は信頼性が高いとは言えない。 そのために、 CbC では Meta CodeGear を用いて Context から必要な DataGear を取り出し、 CodeGear に接続する stub CodeGear という Meta CodeGear を定義している。 - - +% Meta DataGear は? diff -r a6f371a5d33d -r b5fffa8ae875 paper/cbc_agda.tex --- a/paper/cbc_agda.tex Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/cbc_agda.tex Wed Jan 29 22:36:17 2020 +0900 @@ -1,53 +1,62 @@ \chapter{Continuation based C と Agda} +Agda は CbC の上位言語として使われる。 +また、Agda での検証は CbC でのメタ計算に当たる。 +そのため Agda 上で記述される + CbC はメタ計算を含んだ形で記述することができる。 -本章では当研究室で推奨している単位での検証を行うため、 -Agda 上で CodeGear、 DataGear の表現を示す。 +本章では当研究室で推奨している単位を用いての検証を行うため、 +Agda 上で DataGear、 CodeGear の表現を示す。 また、Gear の単位と Hoare Logic を対応させ、 -CbC 上での Hoare Logic について説明を行う。 - - -\section{DataGear と Agda} -Agda での DataGear は CodeGear で扱うすべてのデータである。 +CbC 上での Hoare Logic について示す。 -\section{CodeGear と Agda} +\section{DataGear、 CodeGear と Agdaの対応} +DataGear は Agda で使うことのできるすべてのデータに対応する。 +また、Agda での記述はメタ計算として扱われるので Context を通してデータを +扱う必要はない。 + CodeGear は DataGear を受け取って処理を行い DataGear を返す。 また、CodeGear 間の移動は継続を用いて行われる。 継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻らず、 次の CodeGear へ継続を行う。 + これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当するため、 継続渡し(Continuation Passing Style) で書かれた Agda の関数と対応する。 継続は不定の型 (\verb/t/) を返す関数で表される。 CodeGear は次に実行する関数の型を引数として受け取り不定の型\verb/t/を返す関数として記述され、 CodeGear 自体も同じ型 \verb/t/ を返す関数となる。 -コード \ref{agda-cg} は Agda で記述した CodeGear の例である。 +コード \ref{agda-while} は Agda で記述した CodeGear の例である。 -\lstinputlisting[caption= whileTest の型, label=agda-cg]{src/while-test.agda.replaced} +\lstinputlisting[caption= whileTest の型, label=agda-while]{src/while-test.agda.replaced} %% Agda のとこで Level の話を…！ ここでは \verb/c10/ と名付けた自然数を受け取った後、 \verb/Env/ を受け取って不定の型\verb/t/を返す関数を受け取り、 \verb/t/を返す CodeGear を定義している。 - -\section{Meta CodeGear の表現} +\section{Meta CodeGear の表現と Meta DataGear} Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear である。 Agda での Meta CodeGear は通常の CodeGear を引数に取りそれらの関係などの上位概念を返す CodeGear である。 これは(図を入れる)のような Code Gear となる。 +% \lstinputlisting[label=src:agda-mcg, caption= Agda における Meta CodeGear 型の定義] {src/MetaCodeGear.agda.replaced} + +Meta DataGear については不確かであるが、 DataGear が持つ同値関係や、大小関係などの関係を表す DataGear がそれに当たると考えている。 +Agda 上では Meta DataGear を持つことで性質を持ったデータ構造を作ることができる。 + % \lstinputlisting[label=src:agda-cs, caption= Agda における CodeGear 型の定義] {src/CodeSegment.agda.replaced} - \section{CbC 上での HoareLogic の実現} CbC 上の Hoare Logic は引数として事前条件、次の CodeGear に渡す値に事後条件を含めることで記述する。 その際に事前条件が CodeGear で変更され、事後条件を導く形になる。 例として while プログラムの CbC 記述についてみる。 + %% コード ここでは~ -Hoare Logic の記述としてはこれで良く、部分整合性は示せているが、 + Hoare Logic の記述を行い、部分的な整合性を示すことができている。 全体の検証を行うためには接続されているすべての CodeGear が実行されたときの健全性(Soundness)が担保される必要がある。 そのため、検証用の Meta CodeGear を記述する。 例として while プログラムの健全性を担保するプログラムをみる。 diff -r a6f371a5d33d -r b5fffa8ae875 paper/history.tex --- a/paper/history.tex Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/history.tex Wed Jan 29 22:36:17 2020 +0900 @@ -6,10 +6,8 @@ \begin{enumerate} \item 外間政尊, 河野真治. GearsOSのAgdaによる記述と検証. 研究報告システムソフトウェアとオペレーティング・システム（OS), May, 2018 \item 外間政尊, 河野真治. GearsOSのHoare Logicをベースにした検証手法. 電子情報通信学会 ソフトウェアサイエンス研究会 (SIGSS) 1月, Jan, 2019 - + \item 外間政尊, 河野真治. 継続を基本とする言語CbCでのHoareLogicによる健全性の考察. 電子情報通信学会 ソフトウェアサイエンス研究会 (SIGSS) 3月, Jan, 2020 %% \item 宮城光希, 河野真治. Code Gear と Data Gear を持つ Gears OS の設計. 第59回プログラミング・シンポジウム, Jan, 2018 \end{enumerate} - - -\vspace*{\stretch{2}} +\vspace*{\stretch{3}} diff -r a6f371a5d33d -r b5fffa8ae875 paper/hoare.tex --- a/paper/hoare.tex Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/hoare.tex Wed Jan 29 22:36:17 2020 +0900 @@ -1,22 +1,20 @@ \chapter{Floyd-Hoare Logic} -HoareLogic\cite{hoare} とは C.A.R Hoare、 R.W Floyd らによるプログラムの検証の手法である。 -HoareLogic では事前条件(Pre-Condition)が成り立つとき、何らかの計算(Command)を実行した後に +Floyd-Hoare Logic\cite{hoare}(以下 Hoare Logic) とは C.A.R Hoare、 R.W Floyd らによるプログラムの検証の手法である。 +Hoare Logic では事前条件(Pre-Condition)が成り立つとき、何らかの計算(Command)を実行した後に 事後条件(Post-Condition)が成り立つことを検証する。 事前条件を P 、 何らかの計算を C 、 事後条件を Q としたとき、 ${P} C {Q}$ といった形で表される。 -この ${P} C {Q}$ のことを HoareTriple と呼ぶ。 -HoareTriple ではプログラムの部分的な正当性を検証することができ、 -Q のあとに別の C をつなげてプログラムを構築し、すべての実行を検証することができる。 +Hoare Logic ではプログラムの部分的な正当性を検証することができ、 +事後条件のあとに別の Command をつなげてプログラムを構築することで、シンプルな計算に対する検証することができる。 \section{Agda での Hoare Logic システムの構築} -現在 Agda 上での HoareLogic は初期の Agda で実装されたもの \cite{agda-alpa}とそれを現在の Agda に対応させたもの \cite{agda2-hoare}が存在している。 +現在 Agda 上での Hoare Logic は初期の Agda で実装されたもの \cite{agda-alpa}とそれを現在の Agda に対応させたもの \cite{agda2-hoare}が存在している。 -例として Agda に対応させたもの \cite{agda2-hoare}の Command と証明のためのルールを使って HoareLogic を実装した。 - Code \ref{agda-hoare} は Agda上での HoareLogic の構築子である。 -ここでの Comm は Agda2 に対応した Command の定義を使用している。 +例として現在 Agda に対応させたもの \cite{agda2-hoare}の Command と証明のためのルールを使って Hoare Logic を実装した。 +\ref{agda-hoare} は Agda上での Hoare Logic の構築子である。 -例として Code \ref{agda-while} のようなプログラムを記述した。 +例として Code \ref{c-while} のようなプログラムを記述した。 -\begin{lstlisting}[caption=while Loop Program,label=agda-while] +\begin{lstlisting}[caption=while Loop Program,label=c-while] n = 10; i = 0; @@ -27,13 +25,13 @@ } \end{lstlisting} -$Env$ は Code \ref{agda-while}の n、 i といった変数をまとめたものであり、型として Agda 上での自然数の型である Nat を持つ。 +$Env$ は Code \ref{c-while}の n、 i といった変数をまとめたものであり、型として Agda 上での自然数の型である Nat を持つ。 PrimComm は Primitive Command で、 n、i といった変数に 代入するときに使用される関数である。 -Cond は HoareLogic の Condition で、 Env を受け取って　Bool 値を返す関数となっている。 +Cond は Hoare Logic の Condition で、 Env を受け取って　Bool 値を返す関数となっている。 -Agda のデータで定義されている Comm は HoareLogic での Command を表す。 +Agda のデータで定義されている Comm は Hoare Logic での Command を表す。 Skip は何も変更しない Command で、 Abort はプログラムを中断する Command である。 @@ -46,7 +44,7 @@ While は Cond と Comm を受け取り、 Cond の中身が True である間、 Comm を繰り返す Command である。 -\begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare] +\begin{lstlisting}[caption=Agda での Hoare Logic の構成,label=agda-hoare] PrimComm : Set PrimComm = Env → Env @@ -62,45 +60,48 @@ While : Cond -> Comm -> Comm \end{lstlisting} -Agda 上の HoareLogic で使われるプログラムは Comm 型の関数となる。 +Agda 上の Hoare Logic で使われるプログラムは Comm 型の関数となる。 プログラムの処理を Seq でつないでいき、最終的な状態にたどり着くと値を返して止まる。 %% Code \ref{agda-hoare-simpl} は 変数 $i$、 $n$ に代入を行うプログラムである。 %% これは Seq で PComm を2つ繋げた形になる。 - Code \ref{agda-hoare-prog}は Code \ref{agda-while}で書いた While Loop を HoareLogic での Comm で記述したものである。 + Code \ref{agda-hoare-prog}は Code \ref{c-while}で書いた While Loop を Hoare Logic での Comm で記述したものである。 ここでの $\$$は $()$の対応を合わせる Agda の糖衣構文で、行頭から行末までを $()$で囲っていることと同義である。 -\begin{lstlisting}[caption= HoareLogic のプログラム ,label=agda-hoare-prog,mathescape=false] -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)} )) -\end{lstlisting} +\lstinputlisting[caption= Hoare Logic のプログラム ,label=agda-hoare-prog]{src/agda-hoare-prog.agda.replaced} +%% \begin{lstlisting}[caption= Hoare Logic のプログラム ,label=agda-hoare-prog] %% ,mathescape=false +%% 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)} )) +%% \end{lstlisting} この Comm は Command をならべているだけである。 この Comm を Agda 上で実行するため、 Code \ref{agda-hoare-interpret} のような interpreter を記述した。 -\begin{lstlisting}[caption=Agda での HoareLogic interpreter ,label=agda-hoare-interpret] -{-# 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 -\end{lstlisting} + +\lstinputlisting[caption=Agda での Hoare Logic interpreter ,label=agda-hoare-interpret]{src/agda-hoare-interpret.agda.replaced} +%% \begin{lstlisting}[caption=Agda での Hoare Logic interpreter ,label=agda-hoare-interpret] +%% {-# 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 +%% \end{lstlisting} Code \ref{agda-hoare-interpret}は 初期状態の Env と 実行する Command の並びを受けとって、実行後の Env を返すものとなっている。 -\begin{lstlisting}[caption=Agda での HoareLogic の実行 ,label=agda-hoare-run] +\begin{lstlisting}[caption=Agda での Hoare Logic の実行 ,label=agda-hoare-run] test : Env test = interpret ( record { vari = 0 ; varn = 0 } ) program \end{lstlisting} @@ -108,12 +109,11 @@ Code \ref{agda-hoare-run}のように interpret に $vari = 0 , varn = 0$ の record を渡し、 実行する Comm を渡して 評価してやると$record { varn = 0 ; vari = 10 }$ のような Env が返ってくる。 -\section{Agda 上での Hoare Logic システムの検証} -ここでは先程例とした \ref{agda-while} の検証を例とする。 +\section{Agda 上での Hoare Logic の部分正当性} +ここでは先程例とした \ref{?} の部分正当性の検証を行う。 - Code \ref{agda-hoare-rule} は Agda 上での HoareLogic での証明の構成である。 -HTProof では Condition と Command もう一つ Condition を受け取って、 Set を返す Agda のデータである。 -ここでの HTProof \cite{agda2-hoare} も Agda2 に移植されたものを使っている。 + Code \ref{agda-hoare-rule} は Agda 上での Hoare Logic での Command の検証である。 +HTProof では Condition と Command もう一つ Condition を受け取って、 Set を返す Agda のデータとして表現されている。 PrimRule は Code \ref{axiom-taut} の Axiom という関数を使い、事前条件が成り立っている時、 実行後に事後条件が成り立つならば、 PComm で変数に値を代入できることを保証している。 @@ -134,47 +134,51 @@ \lstinputlisting[caption=Axiom と Tautology,label=axiom-taut]{src/axiom-taut.agda.replaced} -\begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare-rule] -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) -\end{lstlisting} + -Code \ref{agda-hoare-rule}を使って Code \ref{agda-while}の whileProgram の証明を構築する。 +%% \begin{lstlisting}[caption=Agda での Hoare Logic の構成,label=agda-hoare-rule] +%% 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) +%% \end{lstlisting} -全体の証明は Code \ref{agda-hoare-while}の proof1 の様になる。 +Code \ref{agda-hoare-rule}を使って Code \ref{agda-while}の whileProgram の仕様を構成する。 + +\lstinputlisting[caption=Axiom と Tautology,label=axiom-taut{src/agda-hoare-rule.agda.replaced} + +全体の仕様は Code \ref{agda-hoare-while}の proof1 の様になる。 proof1 では型で initCond、 Code \ref{agda-hoare-prog}のprogram、 termCond を記述しており、 -initCond から program を実行し termCond に行き着く HoareLogic の証明になる。 +initCond から program を実行し termCond に行き着く Hoare Logic の証明になる。 それぞれの Condition は Rule の後に記述されている {} に囲まれた部分で、 initCondのみ無条件で true を返す Condition になっている。 それぞれの Rule の中にそこで証明する必要のある補題が lemma で埋められている。 -lemma1 から lemma5 の証明は幅を取ってしまうため、 詳細は当研究室レポジトリ \cite{cr-ryukyu} のプログラムを参照していただきたい。 +lemma1 から lemma5 の証明は幅を取ってしまうため、 全体は付録に載せる。 これらの lemma は HTProof の Rule に沿って必要なものを記述されており、 lemma1 では PreCondition と PostCondition が存在するときの代入の保証、 @@ -183,23 +187,212 @@ lemma4 では While Loop を抜けたときの Condition の整合性、 lemma5 では While Loop を抜けた後のループ不変条件からCondition への変換と termCond への移行の整合性を保証している。 -\begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while] -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 -\end{lstlisting} + +\lstinputlisting[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]{src/agda-hoare-while.agda.replaced} +%% \begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while] +%% proof1 : HTProof initCond program termCond +%% proof1 = +%% 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 +%% \end{lstlisting} proof1 は Code \ref{agda-hoare-prog}の program と似た形をとっている。 -HoareLogic では Comannd に対応する証明規則があるため、証明はプログラムに対応している。 +Hoare　Logic では Comannd に対応する証明規則があるため、仕様はプログラムに対応している。 \section{Agda 上での Hoare Logic システムの健全性} -\ref{agda-hoare-while} では Agda での HoareLogic を用いた証明の構築を行った。 -システムの健全性は本来 Agda 側で保証する必要があるが、今回の例では Agda 上に Hoare Logic -を行えるシステムを構築したので健全性を担保する必要がある。 -hogefugapiyo +\ref{agda-hoare-while} では Agda での Hoare Logic を用いた仕様の構成を行った。 +この仕様が実際に正しく動作するかどうか(健全性)を証明する必要がある。 + +\ref{agda-hoare-satisfies} は Hoare Logic 上での部分正当性を確かめるための関数である。 + SemComm では Comm を受け取って成り立つ関係を返す。 + Satisfies では Pre Condition と Command、 Post Condition を受け取って、 + Pre Condition から Post Condition を正しく導けるという仕様を返す。 + +\lstinputlisting[caption= State Sequence の部分正当性,label=agda-hoare-satisfies]{src/agda-hoare-satisfies.agda.replaced} + +%% \begin{lstlisting}[caption= State Sequence の部分正当性,label=agda-hoare-satisfies] +%% 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 +%% \end{lstlisting} + +これらの仕様を検証することでそれぞれの Command に対する部分正当性を示す。 + +\ref{agda-hoare-soundness} の Soundness では HTProof を受け取り、 Satisfies に合った証明を返す。 +Soundness では HTProof に記述されている Rule でパターンマッチを行い、対応する証明を適応している。 + +\lstinputlisting[caption=Agda での Hoare Logic の健全性,label=agda-hoare-soundness]{src/agda-hoare-soundness.agda.replaced} +%% ↑ ながすぎて無理説ある + +%% \begin{lstlisting}[caption=Agda での Hoare Logic の健全性,label=agda-hoare-soundness] +%% 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 : $mathbb{N}$ +%% n = proj₁ q2 +%% Rel1 : $mathbb{N}$ -> 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 : $mathbb{N}$) -> (ss2 : State) -> Rel1 m s1 ss2 -> +%% SemCond bInv ss2 +%% lem1 $mathbb{N}$.zero ss2 h +%% = substId1 State (proj₂ h) (SemCond bInv) q1 +%% lem1 ($mathbb{N}$.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 +%% \end{lstlisting} + +\ref{agda-hoare-prim-soundness} は HTProof で記述された仕様を、実際に構成可能な仕様を満たしているかを確認する Satisfies を返す。 +照明部分では HTProof で構成された使用を受け取り、 Soundness が対応した証明を返すようになっている。 + + +\begin{lstlisting}[caption=?,label=agda-hoare-prim-soundness] +PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> + HTProof bPre cm bPost -> Satisfies bPre cm bPost +PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht +\end{lstlisting} + +\ref{agda-hoare-prim-proof} は \ref{agda-hoare-prog} の program の Hoare Logic での証明である。 +この証明では初期状態$initCond$と実行するコマンド群$program$を受け取り終了状態として $termCond$ が true であることを示す。 + +\begin{lstlisting}[caption=while program の健全性,label=agda-hoare-prim-proof] +proofOfProgram : (c10 : $mathbb{N}$) → (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 +\end{lstlisting} + + +この証明は実際に構築した仕様である $proof1$ を $PrimSoundness$ に入力することで満たすことができる。 +ここまで記述することで Agda 上の Hoare Logic を用いた while program を検証することができた。 diff -r a6f371a5d33d -r b5fffa8ae875 paper/master_paper.pdf Binary file paper/master_paper.pdf has changed diff -r a6f371a5d33d -r b5fffa8ae875 paper/master_paper.tex --- a/paper/master_paper.tex Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/master_paper.tex Wed Jan 29 22:36:17 2020 +0900 @@ -4,18 +4,22 @@ \usepackage{ascmac} \usepackage[dvipdfmx]{graphicx} \usepackage{here} +\usepackage{listings} \usepackage{comment} +\usepackage[deluxe, multi]{otf} \usepackage{url} -%% \usepackage{cite} -\usepackage[deluxe, multi]{otf} -\usepackage[utf8]{inputenc} +\usepackage{cite} \usepackage{listings} \usepackage{amssymb} -\usepackage{amsmath} -%\input{dummy.tex} %% font +\usepackage[fleqn]{amsmath} + +\usepackage[utf8]{inputenc} -\jtitle{GearsOS での HoareLogic を用いた実装と検証} -\etitle{} % 英文例題まだ +%% \input{dummy.tex} %% font +\usepackage{type1cm} + +\jtitle{} +\etitle{Hoare Logic based Specification and Verification in Continuation based C} \year{2020年 3月} \eyear{March 2020} \author{外間 政尊} @@ -65,8 +69,8 @@ %%% 索引のために以下の2行を追加 \usepackage{makeidx,multicol} \makeindex + \begin{document} -%rome \maketitle \pagenumbering{roman} @@ -105,9 +109,9 @@ \input{tree.tex} \input{conclusion.tex} -%謝辞 -\addcontentsline{toc}{chapter}{謝辞} -\input{thanks.tex} +%% %謝辞 +%% \addcontentsline{toc}{chapter}{謝辞} +%% \input{thanks.tex} %参考文献 \nocite{*} @@ -117,4 +121,5 @@ %付録 \addcontentsline{toc}{chapter}{付録} \appendix + \end{document} diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/AgdaElem.agda.replaced --- a/paper/src/AgdaElem.agda.replaced Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/src/AgdaElem.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -1,3 +1,3 @@ -elem : {A : Set} {{eqA : Eq A}} → A → List A → Bool +elem : {A : Set} {{eqA : Eq A}} @$\rightarrow$@ A @$\rightarrow$@ List A @$\rightarrow$@ Bool elem {{eqA}} x (y @$\text{::}$@ xs) = (Eq._==_ eqA x y) || (elem {{eqA}} x xs) elem x [] = false diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/AgdaTreeProof.agda.replaced --- a/paper/src/AgdaTreeProof.agda.replaced Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/src/AgdaTreeProof.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -8,14 +8,14 @@ putTest1 n k x with n ... | Just n1 = lemma2 ( record { top = Nothing } ) where - lemma2 : (s : SingleLinkedStack (Node @$\mathbb{N}$@ @$\mathbb{N}$@) ) @$\rightarrow$@ putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (@$\lambda$@ t → - GetRedBlackTree.checkNode t k (@$\lambda$@ t@$\text{1}$@ x1 → check2 x1 x @$\equiv$@ True) (root t)) + lemma2 : (s : SingleLinkedStack (Node @$\mathbb{N}$@ @$\mathbb{N}$@) ) @$\rightarrow$@ putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (@$\lambda$@ t @$\rightarrow$@ + GetRedBlackTree.checkNode t k (@$\lambda$@ t@$\text{1}$@ x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) (root t)) lemma2 s with compare2 k (key n1) ... | EQ = lemma3 {!!} where lemma3 : compare2 k (key n1) @$\equiv$@ EQ @$\rightarrow$@ getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record { root = Just ( record { key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black - } ) ; nodeStack = s ; compare = @$\lambda$@ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) + } ) ; nodeStack = s ; compare = @$\lambda$@ x@$\text{1}$@ y @$\rightarrow$@ compare2 x@$\text{1}$@ y } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) lemma3 eq with compare2 x x | putTest1Lemma2 x ... | EQ | refl with compare2 k (key n1) | eq ... | EQ | refl with compare2 x x | putTest1Lemma2 x @@ -27,7 +27,7 @@ where lemma1 : getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record { root = Just ( record { key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red - } ) ; nodeStack = record { top = Nothing } ; compare = @$\lambda$@ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y } ) k + } ) ; nodeStack = record { top = Nothing } ; compare = @$\lambda$@ x@$\text{1}$@ y @$\rightarrow$@ compare2 x@$\text{1}$@ y } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) lemma1 with compare2 k k | putTest1Lemma2 k ... | EQ | refl with compare2 x x | putTest1Lemma2 x diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/Equiv.agda.replaced --- a/paper/src/Equiv.agda.replaced Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/src/Equiv.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -1,1 +1,1 @@ -data _@$\equiv$@_ {a} {A : Set a} (x : A) : A → Set a where refl : x @$\equiv$@ x \ No newline at end of file +data _@$\equiv$@_ {a} {A : Set a} (x : A) : A @$\rightarrow$@ Set a where refl : x @$\equiv$@ x \ No newline at end of file diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/RedBlackTree.agda.replaced --- a/paper/src/RedBlackTree.agda.replaced Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/src/RedBlackTree.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -209,7 +209,7 @@ open import Data.Nat hiding (compare) -compare@$\mathbb{N}$@ : @$\mathbb{N}$@ → @$\mathbb{N}$@ → CompareResult {Level.zero} +compare@$\mathbb{N}$@ : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ CompareResult {Level.zero} compare@$\mathbb{N}$@ x y with Data.Nat.compare x y ... | less _ _ = LT ... | equal _ = EQ diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/agda-hoare-interpret.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-interpret.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -0,0 +1,13 @@ +{-# 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 + diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/agda-hoare-prog.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-prog.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -0,0 +1,7 @@ +program : Comm +program = + Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = 10})) + $ 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)} )) diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/agda-hoare-rule.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-rule.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -0,0 +1,27 @@ +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 /\ b) cmThen bPost @$\rightarrow$@ + HTProof (bPre /\ neg b) cmElse bPost @$\rightarrow$@ + HTProof bPre (If b cmThen cmElse) bPost + WhileRule : {cm : Comm} @$\rightarrow$@ {bInv : Cond} @$\rightarrow$@ {b : Cond} @$\rightarrow$@ + HTProof (bInv /\ b) cm bInv @$\rightarrow$@ + HTProof bInv (While b cm) (bInv /\ neg b) diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/agda-hoare-satisfies.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-satisfies.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -0,0 +1,25 @@ +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 diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/agda-hoare-soundness.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-soundness.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -0,0 +1,118 @@ +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@$\text{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@$\text{1}$@ q2 + r1 : SemComm cm1 s1 sMid @$\times$@ SemComm cm2 sMid s2 + r1 = proj@$\text{2}$@ q2 + r2 : SemComm cm1 s1 sMid + r2 = proj@$\text{1}$@ r1 + r3 : SemComm cm2 sMid s2 + r3 = proj@$\text{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 /\ 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 @$\rightarrow$@ + SemCond bPost s2 + rThen = @$\lambda$@ h @$\rightarrow$@ + let t1 : SemCond b s1 @$\times$@ SemComm cmThen s1 s2 + t1 = (proj@$\text{2}$@ (RelOpState.deltaRestPre + (SemCond b) + (SemComm cmThen) s1 s2)) h + t2 : SemCond (bPre /\ b) s1 + t2 = (proj@$\text{2}$@ (respAnd bPre b s1)) + (q1 , proj@$\text{1}$@ t1) + in hypThen s1 s2 t2 (proj@$\text{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@$\text{2}$@ (RelOpState.deltaRestPre + (NotP (SemCond b)) (SemComm cmElse) s1 s2) + h + t6 : SemCond (neg b) s1 + t6 = proj@$\text{2}$@ (respNeg b s1) (proj@$\text{1}$@ t10) + t7 : SemComm cmElse s1 s2 + t7 = proj@$\text{2}$@ t10 + t8 : SemCond (bPre /\ neg b) s1 + t8 = proj@$\text{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@$\text{2}$@ (respAnd bInv (neg b) s2) t20 + where + hyp : Satisfies (bInv /\ b) cm' bInv + hyp = Soundness pr + n : $mathbb{N}$ + n = proj@$\text{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@$\text{2}$@ q2 + t15 : (Rel1 n s1 s2) @$\times$@ (NotP (SemCond b) s2) + t15 = proj@$\text{2}$@ (RelOpState.deltaRestPost + (NotP (SemCond b)) (Rel1 n) s1 s2) + t1 + t16 : Rel1 n s1 s2 + t16 = proj@$\text{1}$@ t15 + t17 : NotP (SemCond b) s2 + t17 = proj@$\text{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@$\text{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@$\text{1}$@ h + t21 : Rel1 n s1 s20 + t21 = proj@$\text{1}$@ (proj@$\text{2}$@ h) + t22 : (SemCond b s20) @$\times$@ (SemComm cm' s20 ss2) + t22 = proj@$\text{2}$@ (RelOpState.deltaRestPre + (SemCond b) (SemComm cm') s20 ss2) + (proj@$\text{2}$@ (proj@$\text{2}$@ h)) + t23 : SemCond (bInv /\ b) s20 + t23 = proj@$\text{2}$@ (respAnd bInv b s20) + (hyp2 s20 t21 , proj@$\text{1}$@ t22) + in hyp s20 ss2 t23 (proj@$\text{2}$@ t22) + t20 : SemCond bInv s2 @$\times$@ SemCond (neg b) s2 + t20 = lem1 n s2 t16 , proj@$\text{2}$@ (respNeg b s2) t17 diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/agda-hoare-while.agda.replaced --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-while.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -0,0 +1,8 @@ +proof1 : HTProof initCond program termCond +proof1 = + SeqRule {@$\lambda$@ e @$\rightarrow$@ true} ( PrimRule empty-case ) + $ SeqRule {@$\lambda$@ e @$\rightarrow$@ Equal (varn e) 10} ( PrimRule lemma1 ) + $ WeakeningRule {@$\lambda$@ e @$\rightarrow$@ (Equal (varn e) 10) @$\wedge$@ (Equal (vari e) 0)} lemma2 ( + WhileRule {_} {@$\lambda$@ e @$\rightarrow$@ Equal ((varn e) + (vari e)) 10} + $ SeqRule (PrimRule {@$\lambda$@ e @$\rightarrow$@ whileInv e @$\wedge$@ lt zero (varn e) } lemma3 ) + $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/axiom-taut.agda.replaced --- a/paper/src/axiom-taut.agda.replaced Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/src/axiom-taut.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -1,10 +1,10 @@ -_@$\Rightarrow$@_ : Bool → Bool → Bool +_@$\Rightarrow$@_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool false @$\Rightarrow$@ _ = true true @$\Rightarrow$@ true = true true @$\Rightarrow$@ false = false Axiom : Cond @$\rightarrow$@ PrimComm @$\rightarrow$@ Cond @$\rightarrow$@ Set -Axiom pre comm post = ∀ (env : Env) → (pre env) @$\Rightarrow$@ ( post (comm env)) @$\equiv$@ true +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 = ∀ (env : Env) → (pre env) @$\Rightarrow$@ (post env) @$\equiv$@ true +Tautology pre post = @$\forall$@ (env : Env) @$\rightarrow$@ (pre env) @$\Rightarrow$@ (post env) @$\equiv$@ true diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/function.agda.replaced --- a/paper/src/function.agda.replaced Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/src/function.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -1,4 +1,4 @@ -_-_ :@$\mathbb{N}$@ →@$\mathbb{N}$@ →@$\mathbb{N}$@ +_-_ :@$\mathbb{N}$@ @$\rightarrow$@@$\mathbb{N}$@ @$\rightarrow$@@$\mathbb{N}$@ x - zero = x zero - _ = zero (suc x) - (suc y) = x - y diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/gears-while.agda.replaced --- a/paper/src/gears-while.agda.replaced Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/src/gears-while.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -1,4 +1,4 @@ -whileTest : {l : Level} {t : Set l} @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } → (Code : (env : Env) @$\rightarrow$@ +whileTest : {l : Level} {t : Set l} @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ (Code : (env : Env) @$\rightarrow$@ ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10) @$\rightarrow$@ t) @$\rightarrow$@ t whileTest {_} {_} {c10} next = next env proof2 where @@ -7,7 +7,7 @@ proof2 : ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10) proof2 = record {pi1 = refl ; pi2 = refl} -conversion1 : {l : Level} {t : Set l } → (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } → ((vari env) @$\equiv$@ 0) /\ ((varn env) @$\equiv$@ c10) +conversion1 : {l : Level} {t : Set l } @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } @$\rightarrow$@ ((vari env) @$\equiv$@ 0) /\ ((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 @@ -15,34 +15,34 @@ proof4 = let open @$\equiv$@-Reasoning in begin varn env + vari env - @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n → n + vari env ) (pi2 p1 ) @$\rangle$@ + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n @$\rightarrow$@ n + vari env ) (pi2 p1 ) @$\rangle$@ c10 + vari env - @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n → c10 + n ) (pi1 p1 ) @$\rangle$@ + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ n @$\rightarrow$@ c10 + n ) (pi1 p1 ) @$\rangle$@ c10 + 0 @$\equiv$@@$\langle$@ +-sym {c10} {0} @$\rangle$@ c10 @$\blacksquare$@ {-# TERMINATING #-} -whileLoop : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ {c10 : @$\mathbb{N}$@ } → ((varn env) + (vari env) @$\equiv$@ c10) @$\rightarrow$@ (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t +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 {varn = (varn env) - 1 ; vari = (vari env) + 1} - 1<0 : 1 @$\leq$@ zero → @$\bot$@ + 1<0 : 1 @$\leq$@ zero @$\rightarrow$@ @$\bot$@ 1<0 () - proof3 : (suc zero @$\leq$@ (varn env)) → varn env1 + vari env1 @$\equiv$@ c10 + 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 → n' + z ) ( +-sym {vari env} {1} ) @$\rangle$@ + @$\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 → z + vari env ) +1@$\equiv$@suc @$\rangle$@ + @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ z + vari env ) +1@$\equiv$@suc @$\rangle$@ (suc n' ) + vari env @$\equiv$@@$\langle$@@$\rangle$@ varn env + vari env diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/gears.agda.replaced --- a/paper/src/gears.agda.replaced Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/src/gears.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -1,2 +1,2 @@ -proofGears : {c10 : @$\mathbb{N}$@ } → Set -proofGears {c10} = whileTest {_} {_} {c10} (@$\lambda$@ n p1 → conversion1 n p1 (@$\lambda$@ n1 p2 → whileLoop' n1 p2 (@$\lambda$@ n2 → ( vari n2 @$\equiv$@ c10 )))) +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 )))) diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/redBlackTreeTest.agda.replaced --- a/paper/src/redBlackTreeTest.agda.replaced Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/src/redBlackTreeTest.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -170,14 +170,14 @@ putTest1 n k x with n ... | Just n1 = lemma2 ( record { top = Nothing } ) where - lemma2 : (s : SingleLinkedStack (Node @$\mathbb{N}$@ @$\mathbb{N}$@) ) @$\rightarrow$@ putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (@$\lambda$@ t → - GetRedBlackTree.checkNode t k (@$\lambda$@ t@$\text{1}$@ x1 → check2 x1 x @$\equiv$@ True) (root t)) + lemma2 : (s : SingleLinkedStack (Node @$\mathbb{N}$@ @$\mathbb{N}$@) ) @$\rightarrow$@ putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (@$\lambda$@ t @$\rightarrow$@ + GetRedBlackTree.checkNode t k (@$\lambda$@ t@$\text{1}$@ x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) (root t)) lemma2 s with compare2 k (key n1) ... | EQ = lemma3 {!!} where lemma3 : compare2 k (key n1) @$\equiv$@ EQ @$\rightarrow$@ getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record { root = Just ( record { key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black - } ) ; nodeStack = s ; compare = @$\lambda$@ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) + } ) ; nodeStack = s ; compare = @$\lambda$@ x@$\text{1}$@ y @$\rightarrow$@ compare2 x@$\text{1}$@ y } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) lemma3 eq with compare2 x x | putTest1Lemma2 x ... | EQ | refl with compare2 k (key n1) | eq ... | EQ | refl with compare2 x x | putTest1Lemma2 x @@ -189,7 +189,7 @@ where lemma1 : getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record { root = Just ( record { key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red - } ) ; nodeStack = record { top = Nothing } ; compare = @$\lambda$@ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y } ) k + } ) ; nodeStack = record { top = Nothing } ; compare = @$\lambda$@ x@$\text{1}$@ y @$\rightarrow$@ compare2 x@$\text{1}$@ y } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) lemma1 with compare2 k k | putTest1Lemma2 k ... | EQ | refl with compare2 x x | putTest1Lemma2 x diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/term1.agda.replaced --- a/paper/src/term1.agda.replaced Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/src/term1.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -1,9 +1,9 @@ -stmt2Cond : {c10 :@$\mathbb{N}$@} → Cond +stmt2Cond : {c10 :@$\mathbb{N}$@} @$\rightarrow$@ Cond stmt2Cond {c10} env = (Equal (varn env) c10) @$\wedge$@ (Equal (vari env) 0) -lemma1 : {c10 :@$\mathbb{N}$@} → Axiom (stmt1Cond {c10}) (@$\lambda$@ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ +lemma1 : {c10 :@$\mathbb{N}$@} @$\rightarrow$@ Axiom (stmt1Cond {c10}) (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ 10}) -lemma1 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond → let open @$\equiv$@-Reasoning in +lemma1 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in begin ? -- ?0 @$\equiv$@@$\langle$@ ? @$\rangle$@ -- ?1 diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/term2.agda.replaced --- a/paper/src/term2.agda.replaced Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/src/term2.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -1,7 +1,7 @@ -@$\wedge$@true : { x : Bool } → x @$\wedge$@ true @$\equiv$@ x +@$\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 -stmt1Cond : {c10 :@$\mathbb{N}$@} → Cond +stmt1Cond : {c10 :@$\mathbb{N}$@} @$\rightarrow$@ Cond stmt1Cond {c10} env = Equal (varn env) c10 diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/term3.agda.replaced --- a/paper/src/term3.agda.replaced Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/src/term3.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -1,6 +1,6 @@ -lemma1 : {c10 :@$\mathbb{N}$@} → Axiom (stmt1Cond {c10}) (@$\lambda$@ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ +lemma1 : {c10 :@$\mathbb{N}$@} @$\rightarrow$@ Axiom (stmt1Cond {c10}) (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = 0 }) (stmt2Cond {c\ 10}) -lemma1 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond → let open @$\equiv$@-Reasoning in +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$@ diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/while-test.agda.replaced --- a/paper/src/while-test.agda.replaced Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/src/while-test.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -1,2 +1,2 @@ -whileTest : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) → (Code : Env @$\rightarrow$@ t) @$\rightarrow$@ t +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} ) diff -r a6f371a5d33d -r b5fffa8ae875 paper/src/zero.agda.replaced --- a/paper/src/zero.agda.replaced Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/src/zero.agda.replaced Wed Jan 29 22:36:17 2020 +0900 @@ -1,3 +1,3 @@ -+zero : { y : @$\mathbb{N}$@ } → y + zero @$\equiv$@ y ++zero : { y : @$\mathbb{N}$@ } @$\rightarrow$@ y + zero @$\equiv$@ y +zero {zero} = refl -+zero {suc y} = cong ( @$\lambda$@ x → suc x ) ( +zero {y} ) ++zero {suc y} = cong ( @$\lambda$@ x @$\rightarrow$@ suc x ) ( +zero {y} ) diff -r a6f371a5d33d -r b5fffa8ae875 paper/thanks.tex --- a/paper/thanks.tex Mon Jan 27 20:46:38 2020 +0900 +++ b/paper/thanks.tex Wed Jan 29 22:36:17 2020 +0900 @@ -5,5 +5,5 @@ 最後に、 有意義な時間を共に過ごした理工学研究科情報工学専攻の学友、並びに物心両面で支えてくれた家族に深く感謝致します。 \begin{flushright} - 2018年 3月 \\ 伊波立樹 + 2020年 3月 \\ 外間 政尊 \end{flushright} diff -r a6f371a5d33d -r b5fffa8ae875 ryokka-master.mm --- a/ryokka-master.mm Mon Jan 27 20:46:38 2020 +0900 +++ b/ryokka-master.mm Wed Jan 29 22:36:17 2020 +0900 @@ -1,6 +1,6 @@ - + @@ -10,7 +10,7 @@ Continuation based C での

- HoareLogic を用いた記述と検証 + HoareLogic を用いた仕様記述と検証