# HG changeset patch # User ryokka # Date 1580993348 -32400 # Node ID b8ff2bd1a5af07332529b6391e34345394e0b3ed # Parent 8ef64db6349795407dfd0cd8fc2cca4f629b5a54 fix hoare.tex diff -r 8ef64db63497 -r b8ff2bd1a5af paper/agda.tex --- a/paper/agda.tex Thu Feb 06 19:24:32 2020 +0900 +++ b/paper/agda.tex Thu Feb 06 21:49:08 2020 +0900 @@ -17,6 +17,9 @@ コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される。 また、\verb/_/でそこに入りうるすべての値を示すことができ、 \verb/?/でそこに入る値や型を不明瞭なままにしておくことができる。 +また、Agda では停止性の検出機能が存在し、プログラム中に停止しない関数が存在するとコンパイル時にエラーが出る。 +\verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない。 + Agda のプログラムは全てモジュール内部に記述される。 そのため、各ファイルのトップレベルにモジュールを定義する必要がある。 diff -r 8ef64db63497 -r b8ff2bd1a5af paper/hoare.tex --- a/paper/hoare.tex Thu Feb 06 19:24:32 2020 +0900 +++ b/paper/hoare.tex Thu Feb 06 21:49:08 2020 +0900 @@ -1,49 +1,58 @@ -\chapter{Floyd-Hoare Logic} +\chapter{Hoare Logic} \label{c:hoare} -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}$ といった形で表される。 +Floyd-Hoare Logic \cite{10.1145/363235.363259}(以下 Hoare Logic) とは +C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。 +Hoare Logic では事前条件が成り立つとき、何らかの計算(以下コマンド)を実行した後に +事後条件が成り立つことを検証する。 +事前条件を P 、 何らかの計算を C 、 事後条件を Q としたとき、 +${P} C {Q}$ といった形で表される。 Hoare Logic ではプログラムの部分的な正当性を検証することができ、 -事後条件のあとに別の Command をつなげてプログラムを構築することで、シンプルな計算に対する検証することができる。 +事後条件のあとに別の コマンド をつなげてプログラムを構築することで、 +シンプルな計算に対する検証することができる。 -\section{Agda での Hoare Logic システムの構築} +本章は Agda で実装された Hoare Logic について解説し、 +実際に Hoare Logic を用いた検証を行う。 + + +\section{Hoare Logic} 現在 Agda 上での Hoare Logic は初期の Agda で実装されたもの \cite{agda-alpa}とそれを現在の Agda に対応させたもの \cite{agda2-hoare}が存在している。 -例として現在 Agda に対応させたもの \cite{agda2-hoare}の Command と証明のためのルールを使って Hoare Logic を実装した。 -\ref{agda-hoare} は Agda上での Hoare Logic の構築子である。 +ここでは現在 Agda に対応させたもの \cite{agda2-hoare}の コマンド と証明のためのルールを使用する。 -例として Code \ref{c-while} のようなプログラムを記述した。 +例として \coderef{c-while} のようなプログラムを記述した。 \begin{lstlisting}[caption=while Loop Program,label=c-while] - n = 10; - i = 0; +n = 10; +i = 0; - while (n>0) - { - i++; - n--; - } +while (n > 0) { + i++; + n--; +} \end{lstlisting} -$Env$ は Code \ref{c-while}の n、 i といった変数をまとめたものであり、型として Agda 上での自然数の型である Nat を持つ。 + -PrimComm は Primitive Command で、 n、i といった変数に 代入するときに使用される関数である。 +\coderef{agda-hoare} は Agda 上での Hoare Logic の構築子である。 +\verb/Env/ は \coderef{c-while}の \verb/n/、 \verb/i/ といった変数をレコード型でまとめたもので、\verb/n/と\verb/i/それぞれが型として Agda 上での自然数の型である $\mathbb{N}$ を持つ。 -Cond は Hoare Logic の Condition で、 Env を受け取って　Bool 値を返す関数となっている。 +\verb/PrimComm/ は Primitive Command で、 \verb/n/、\verb/i/ といった変数に 代入するときに使用される関数である。 -Agda のデータで定義されている Comm は Hoare Logic での Command を表す。 +\verb/Cond/ は Hoare Logic の 条件で、 \verb/Env/ を受け取って　\verb/Bool/ 値、\verb/true/ か \verb/false/ を返す関数となっている。 + -Skip は何も変更しない Command で、 Abort はプログラムを中断する Command である。 +Agda のデータで定義されている \verb/Comm/ は Hoare Logic での コマンド を表す。 -PComm は PrimComm を受けて Command を返す型で定義されており、 変数を代入するときに使われる。 +\verb/Skip/ は何も変更しない コマンド で、 \verb/Abort/ はプログラムを中断する コマンド である。 + +\verb/PComm/ は PrimComm を受けて コマンド を返す型で定義されており、 変数を代入するときに使われる。 -Seq は Sequence で Command を2つ受けて Command を返す型で定義されている。 -これは、ある Command から Command に移り、その結果を次の Command に渡す型になっている。 +\verb/Seq/ は Sequence で コマンド を2つ受けて コマンド を返す型で定義されている。 +これは、ある コマンド から コマンド に移り、その結果を次の コマンド に渡す型になっている。 -If は Cond と Comm を2つ受け取り、 Cond が true か false かで 実行する Comm を変える Command である。 +\verb/If/ は \verb/Cond/ と \verb/Comm/ を2つ受け取り、 \verb/Cond/ が \verb/true/ か \verb/false/ かで 実行する \verb/Comm/ を変える コマンド である。 -While は Cond と Comm を受け取り、 Cond の中身が True である間、 Comm を繰り返す Command である。 +\verb/While/ は \verb/Cond/ と \verb/Comm/ を受け取り、 \verb/Cond/ の中身が \verb/True/ である間、 \verb/Comm/ を繰り返す コマンド である。 \begin{lstlisting}[caption=Agda での Hoare Logic の構成,label=agda-hoare] PrimComm : Set @@ -61,12 +70,12 @@ While : Cond -> Comm -> Comm \end{lstlisting} -Agda 上の Hoare Logic で使われるプログラムは Comm 型の関数となる。 -プログラムの処理を Seq でつないでいき、最終的な状態にたどり着くと値を返して止まる。 +Agda 上の Hoare Logic で使われるプログラムは \verb/Comm/ 型の関数となる。 +プログラムの処理を \verb/Seq/ でつないでいき、最終的な状態にたどり着くと値を返して止まる。 %% Code \ref{agda-hoare-simpl} は 変数 $i$、 $n$ に代入を行うプログラムである。 %% これは Seq で PComm を2つ繋げた形になる。 - Code \ref{agda-hoare-prog}は Code \ref{c-while}で書いた While Loop を Hoare Logic での Comm で記述したものである。 + \coderef{agda-hoare-prog}は \coderef{c-while}で書いた While Loop を Hoare Logic でのコマンドで記述したものである。 ここでの $\$$は $()$の対応を合わせる Agda の糖衣構文で、行頭から行末までを $()$で囲っていることと同義である。 \lstinputlisting[caption= Hoare Logic のプログラム ,label=agda-hoare-prog]{src/agda-hoare-prog.agda.replaced} @@ -80,8 +89,7 @@ %% $ PComm (λ env → record env {varn = ((varn env) - 1)} )) %% \end{lstlisting} -この Comm は Command をならべているだけである。 -この Comm を Agda 上で実行するため、 Code \ref{agda-hoare-interpret} のような interpreter を記述した。 +この Comm を Agda 上で実行するため、 \coderef{agda-hoare-interpret} のような関数を作成した。 \lstinputlisting[caption=Agda での Hoare Logic interpreter ,label=agda-hoare-interpret]{src/agda-hoare-interpret.agda.replaced} @@ -100,38 +108,42 @@ %% ... | false = env %% \end{lstlisting} - Code \ref{agda-hoare-interpret}は 初期状態の Env と 実行する Command の並びを受けとって、実行後の Env を返すものとなっている。 +\coderef{agda-hoare-interpret}は 初期状態の \verb/Env/ と 実行する コマンド の並びを受けとって、実行後の \verb/Env/ を返すものとなっている。 +\verb/interpret/ 関数は停止性を考慮していないため、 \verb/{-# TERMINATING #-}/ タグを付けている。 -\begin{lstlisting}[caption=Agda での Hoare Logic の実行 ,label=agda-hoare-run] +\coderef{agda-hoare-run}のように \verb/interpret/ に $vari = 0 , varn = 0$ の record を渡し、 実行する Comm を渡して 評価すると $record { varn = 0 ; vari = 10 }$ のような Env が返ってくる。 +\verb/interpret/ で実行される コマンド は \coderef{agda-hoare-prog} で記述した While Loop するコマンドである + + \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 } \end{lstlisting} - Code \ref{agda-hoare-run}のように interpret に $vari = 0 , varn = 0$ の record を渡し、 実行する Comm を渡して 評価してやると$record { varn = 0 ; vari = 10 }$ のような Env が返ってくる。 - -\section{Agda 上での Hoare Logic の部分正当性} -ここでは先程例とした \ref{?} の部分正当性の検証を行う。 +\section{While Program の部分正当性} +ここでは先程記述した \coderef{agda-hoare-prog} の部分正当性の検証を行う。 - Code \ref{agda-hoare-rule} は Agda 上での Hoare Logic での Command の検証である。 -HTProof では Condition と Command もう一つ Condition を受け取って、 Set を返す Agda のデータとして表現されている。 +\coderef{agda-hoare-rule} で書かれている \verb/HTProof/ は Agda 上での Hoare Logic でのコマンドを検証するための命題をまとめたものである。 +\verb/HTProof/ では Pre-Condition とコマンド、Post-Condition を受け取って、 Set を返す Agda のデータとして表現されている。 -PrimRule は Code \ref{axiom-taut} の Axiom という関数を使い、事前条件が成り立っている時、 -実行後に事後条件が成り立つならば、 PComm で変数に値を代入できることを保証している。 +\verb/PrimRule/ は Pre-Condition と PrimComm、 Post-Condition、 +\coderef{axiom-taut} の \verb/Axiom/ 関数をが成り立つという命題を引数として受け取る。 -SkipRule は Condition を受け取ってそのままの Condition を返すことを保証する。 +\verb/SkipRule/ は Condition を受け取ってそのままの Condition を返す。 -AbortRule は PreContition を受け取って、Abort を実行して終わるルールである。 +\verb/AbortRule/ は PreContition を受け取って、Abort を実行して終わるルールである。 -WeakeningRule は \ref{axiom-taut} の Tautology という関数を使って通常の逐次処理から、 -WhileRule のみに適応されるループ不変変数に移行する際のルールである。 +\verb/WeakeningRule/ は \ref{axiom-taut} の Tautology という関数を使って通常の逐次処理から、 +\verb/WhileRule/ のみに適応されるループ不変変数に移行する際のルールである。 -SeqRule は3つの Condition と 2つの Command を受け取り、これらのプログラムの逐次的な実行を保証する。 +\verb/SeqRule/ は3つの Condition と 2つの コマンド を受け取り、これらのプログラムの逐次的な実行を保証する。 -IfRule は分岐に用いられ、3つの Condition と 2つの Command を受け取り、判定の Condition が成り立っているかいないかで実行する Command を変えるルールである。 -この時、どちらかの Command が実行されることを保証している。 +IfRule は分岐に用いられ、3つの Condition と 2つの コマンド を受け取り、判定の Condition が成り立っているかいないかで実行する コマンド を変えるルールである。 +この時、どちらかの コマンド が実行されることを保証している。 -WhileRule はループに用いられ、1つの Command と２つの Condition を受け取り、事前条件が成り立っている間、 Command を繰り返すことを保証している。 +WhileRule はループに用いられ、1つの コマンド と２つの Condition を受け取り、事前条件が成り立っている間、 コマンド を繰り返すことを保証している。 \lstinputlisting[caption=Axiom と Tautology,label=axiom-taut]{src/axiom-taut.agda.replaced} @@ -205,13 +217,13 @@ Hoare　Logic では Comannd に対応する証明規則があるため、仕様はプログラムに対応している。 -\section{Agda 上での Hoare Logic システムの健全性} +\section{Hoare Logic での健全性} \ref{agda-hoare-while} では Agda での Hoare Logic を用いた仕様の構成を行った。 この仕様が実際に正しく動作するかどうか(健全性)を証明する必要がある。 \ref{agda-hoare-satisfies} は Hoare Logic 上での部分正当性を確かめるための関数である。 SemComm では Comm を受け取って成り立つ関係を返す。 - Satisfies では Pre Condition と Command、 Post Condition を受け取って、 + Satisfies では Pre Condition と コマンド、 Post Condition を受け取って、 Pre Condition から Post Condition を正しく導けるという仕様を返す。 \lstinputlisting[caption= State Sequence の部分正当性,label=agda-hoare-satisfies]{src/agda-hoare-satisfies.agda.replaced} @@ -244,7 +256,7 @@ %% SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2 %% \end{lstlisting} -これらの仕様を検証することでそれぞれの Command に対する部分正当性を示す。 +これらの仕様を検証することでそれぞれの コマンド に対する部分正当性を示す。 \ref{agda-hoare-soundness} の Soundness では HTProof を受け取り、 Satisfies に合った証明を返す。 Soundness では HTProof に記述されている Rule でパターンマッチを行い、対応する証明を適応している。 diff -r 8ef64db63497 -r b8ff2bd1a5af paper/master_paper.pdf Binary file paper/master_paper.pdf has changed diff -r 8ef64db63497 -r b8ff2bd1a5af paper/reference.bib --- a/paper/reference.bib Thu Feb 06 19:24:32 2020 +0900 +++ b/paper/reference.bib Thu Feb 06 21:49:08 2020 +0900 @@ -94,6 +94,25 @@ address = {New York, NY, USA}, } +@article{10.1145/363235.363259, +author = {Hoare, C. A. R.}, +title = {An Axiomatic Basis for Computer Programming}, +year = {1969}, +issue_date = {October 1969}, +publisher = {Association for Computing Machinery}, +address = {New York, NY, USA}, +volume = {12}, +number = {10}, +issn = {0001-0782}, +url = {https://doi.org/10.1145/363235.363259}, +doi = {10.1145/363235.363259}, +journal = {Commun. ACM}, +month = oct, +pages = {576–580}, +numpages = {5}, +keywords = {programming language design, theory of programming’ proofs of programs, machine-independent programming, program documentation, axiomatic method, formal language definition} +} + @misc{agda-alpa, title = {Example - Hoare Logic},