|
0
|
1 %% v3.1 [2018/04/18]
|
|
|
2 %\documentclass[Proof,technicalreport]{ieicej}
|
|
|
3 \documentclass[technicalreport]{ieicej}
|
|
1
|
4
|
|
|
5 \usepackage[dvipdfmx]{graphicx}
|
|
|
6 \usepackage{graphicx}
|
|
0
|
7 \usepackage{lmodern}
|
|
|
8 \usepackage{textcomp}
|
|
|
9 \usepackage{latexsym}
|
|
8
|
10 \usepackage{ascmac}
|
|
|
11 \usepackage[fleqn]{amsmath}
|
|
|
12 \usepackage{amssymb}
|
|
|
13 \usepackage[deluxe, multi]{otf}
|
|
4
|
14 \usepackage{url}
|
|
5
|
15 \usepackage{cite}
|
|
6
|
16 \usepackage[portuguese]{babel}
|
|
|
17 \usepackage[utf8]{inputenc}
|
|
|
18 \usepackage{listingsutf8}
|
|
1
|
19 \usepackage{listings}
|
|
8
|
20 \usepackage{colonequals}
|
|
6
|
21 \usepackage{inconsolata}
|
|
1
|
22 \lstset{
|
|
|
23 frame=single,
|
|
|
24 keepspaces=true,
|
|
|
25 stringstyle={\ttfamily},
|
|
|
26 commentstyle={\ttfamily},
|
|
|
27 identifierstyle={\ttfamily},
|
|
|
28 keywordstyle={\ttfamily},
|
|
6
|
29 % basicstyle=\footnotesize,
|
|
1
|
30 breaklines=true,
|
|
|
31 xleftmargin=0zw,
|
|
|
32 xrightmargin=0zw,
|
|
|
33 framerule=.2pt,
|
|
|
34 columns=[l]{fullflexible},
|
|
|
35 numbers=left,
|
|
|
36 stepnumber=1,
|
|
|
37 numberstyle={\scriptsize},
|
|
|
38 numbersep=1em,
|
|
|
39 language={},
|
|
|
40 tabsize=4,
|
|
|
41 lineskip=-0.5zw,
|
|
6
|
42 inputencoding=utf8,
|
|
|
43 extendedchars=true,
|
|
8
|
44 stringstyle={\ttfamily},
|
|
6
|
45 escapechar={@},
|
|
8
|
46 %% mathescape=true,
|
|
1
|
47 }
|
|
5
|
48
|
|
8
|
49 %% literate=
|
|
|
50 %% {⟨}{{\langle}}1
|
|
|
51 %% {⟩}{{\rangle}}1
|
|
|
52 %% {ℕ}{{$\mathbb{N}$}}1
|
|
|
53 %% {^^e2^^84^^95}{{$\mathbb{N}$}}1
|
|
|
54
|
|
5
|
55 % basicstyle={\ttfamily},
|
|
1
|
56 \renewcommand{\lstlistingname}{Code}
|
|
|
57 \usepackage{caption}
|
|
|
58 \captionsetup[lstlisting]{font={small,tt}}
|
|
|
59
|
|
0
|
60 \def\IEICEJcls{\texttt{ieicej.cls}}
|
|
|
61 \def\IEICEJver{3.1}
|
|
|
62 \newcommand{\AmSLaTeX}{%
|
|
|
63 $\mathcal A$\lower.4ex\hbox{$\!\mathcal M\!$}$\mathcal S$-\LaTeX}
|
|
|
64 %\newcommand{\PS}{{\scshape Post\-Script}}
|
|
|
65 \def\BibTeX{{\rmfamily B\kern-.05em{\scshape i\kern-.025em b}\kern-.08em
|
|
|
66 T\kern-.1667em\lower.7ex\hbox{E}\kern-.125em X}}
|
|
|
67
|
|
2
|
68 \jtitle{GearsOSのHoare Logicをベースにした検証手法}
|
|
0
|
69 %% \jsubtitle{技術研究報告原稿のための解説とテンプレート}
|
|
|
70 %% \etitle{How to Use \LaTeXe\ Class File (\IEICEJcls\ version \IEICEJver)
|
|
|
71 %% for the Technical Report of the Institute of Electronics, Information
|
|
|
72 %% and Communication Engineers}
|
|
|
73 %% \esubtitle{Guide to the Technical Report and Template}
|
|
|
74 \authorlist{
|
|
1
|
75 \authorentry[masataka@cr.ie.u-ryukyu.ac.jp]{外間 政尊}{Masataka Hokama}{1}%
|
|
|
76 \authorentry[kono@cr.ie.u-ryukyu.ac.jp]{河野 真治}{Shinji Kono}{2}%
|
|
0
|
77 }
|
|
|
78 \affiliate[1]{琉球大学大学院理工学研究科情報工学専攻}
|
|
1
|
79 {Interdisciplinary Information Engineering, Graduate School of Engineering and Science, University of the Ryukyus.}
|
|
0
|
80 \affiliate[2]{琉球大学工学部情報工学科}
|
|
|
81 {Information Engineering, University of the Ryukyus.}
|
|
|
82 %\MailAddress{$\dagger$hanako@denshi.ac.jp,
|
|
|
83 % $\dagger\dagger$\{taro,jiro\}@jouhou.co.jp}
|
|
|
84 \begin{document}
|
|
|
85 \begin{jabstract}
|
|
|
86 あらまし
|
|
|
87 \end{jabstract}
|
|
|
88 \begin{jkeyword}
|
|
|
89 プログラミング言語,
|
|
5
|
90 CbC, Gears OS, Agda, 検証
|
|
0
|
91 %% あと他…？
|
|
|
92 \end{jkeyword}
|
|
|
93 %% \begin{eabstract}
|
|
|
94 %% %% メールを見た感じ日本語のみとなっていたので不必要…？
|
|
|
95 %% \end{eabstract}
|
|
|
96 %% \begin{ekeyword}
|
|
|
97 %% %% 不必要？
|
|
|
98 %% \end{ekeyword}
|
|
|
99 \maketitle
|
|
|
100 \section{まえがき}
|
|
5
|
101 OS やアプリケーションの信頼性は重要である。
|
|
9
|
102 信頼性を上げるにはプログラムが仕様を満たしていることを検証する必要がある。
|
|
5
|
103 プログラムの検証手法として、Floyd–Hoare logic (以下 Hoare Logic)が存在している。
|
|
|
104 HoareLogic は事前条件が成り立っているときにある
|
|
|
105 関数を実行して、それが停止する際に事後条件を満た
|
|
|
106 すことを確認することで、検証を行う。
|
|
|
107 HoareLogic はシンプルなアプローチだが通常のプログラミング言語で使用することができず、
|
|
|
108 広まっているとはいえない。
|
|
|
109
|
|
|
110 当研究室では信頼性の高い OS として GearsOS を開発している。
|
|
|
111 現在 GearsOS ではCodeGear、DataGearという単位を用いてプログラムを記述する手法を用いており、
|
|
|
112 仕様の確認には定理証明系である Agda を用いている。
|
|
|
113
|
|
|
114 CodeGearは Agda 上では継続渡しの記述を用いた関数として
|
|
0
|
115 記述する。
|
|
5
|
116 また、継続にある関数を実行するための事前条件や
|
|
0
|
117 事後条件などをもたせることが可能である。
|
|
5
|
118
|
|
|
119 そのため Hoare Logic と CodeGear、DataGear という単位を用いたプログラミング手法
|
|
9
|
120 記述とは相性が良く、既存の言語とは異なり HoareLogic を使ったプログラミングが容易に行えると考えている。
|
|
5
|
121
|
|
9
|
122 本研究では Agda 上での HoareLogic の記述を使い、簡単な while Loop のプログラムの作成、証明を行った。
|
|
5
|
123 また、GearsOS の仕様確認のために CodeGear、DataGear という単位を用いた記述で Hoare Logic をベースと
|
|
|
124 したwhile Loop プログラムを記述、その証明を行なった。
|
|
|
125
|
|
|
126 \section{現状}
|
|
|
127 現在の OS やアプリケーションの検証では、実装と別に検証用の言語で記述された実装と証明を持つのが一般的である。
|
|
9
|
128 kernel 検証\cite{Klein:2010:SFV:1743546.1743574},\cite{Nelson:2017:HPV:3132747.3132748}の例では C で記述された Kernel に対して、検証用の別の言語で書かれた等価な kernel を用いて OS の検証を行っている。
|
|
|
129 また、別のアプローチとしては ATS2\cite{ats2} や Rust\cite{rust} などの低レベル記述向けの関数型言語を実装に用いる手法が存在している。
|
|
|
130
|
|
|
131 証明支援向けのプログラミング言語としては Agda\cite{agda}、 Coq\cite{coq} などが存在しているが、これらの言語自体は実行速度が期待できるものではない。
|
|
5
|
132
|
|
9
|
133 そこで、当研究室では検証と実装が同一の言語で行う Continuation based C\cite{cbc} という言語を開発している。
|
|
|
134 Continuation based C(CbC) では、処理の単位を CodeGear、 データの単位を DataGear としている。
|
|
|
135 CodeGear は値を入力として受け取り出力を行う処理の単位であり、 CodeGear の出力を 次の GodeGear に接続してプログラミングを行う。 CodeGear の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行うことができる。
|
|
|
136 このメタ計算部分で assertion などの検証を行うことで、 CodeGear の処理に手を加えることなく検証を行う。
|
|
|
137 現段階では CbC 自体に証明を行うためのシステムが存在しないため、証明支援系言語である Agda を用いて等価な実装の検証を行っている。
|
|
5
|
138
|
|
|
139 \section{Agda}
|
|
9
|
140 Adga \cite{agda} とは証明支援系の関数型言語である。
|
|
5
|
141 Agdaにおける型指定は : を用いて行う。例えば、 変数 x が型 A を持つ、ということを表すには x : A と記述する。
|
|
|
142 データ型は、代数的なデータ構造で、その定義には data キーワードを用いる。
|
|
|
143 data キーワードの後に data の名前と、型、 where 句を書きインデントを深 くした後、
|
|
|
144 値にコンストラクタとその型を列挙する。 Code \ref{agda-data} はこの data 型の例である。
|
|
|
145 Comm では Skip、Abort、PComm などのコンストラクタを持ち、: の後に型が書かれている。
|
|
|
146
|
|
|
147 \begin{lstlisting}[caption=data の例,label=agda-data]
|
|
|
148 data Comm : Set where
|
|
|
149 Skip : Comm
|
|
|
150 Abort : Comm
|
|
|
151 PComm : PrimComm -> Comm
|
|
|
152 Seq : Comm -> Comm -> Comm
|
|
|
153 If : Cond -> Comm -> Comm -> Comm
|
|
|
154 While : Cond -> Comm -> Comm
|
|
|
155 \end{lstlisting}
|
|
|
156
|
|
|
157 Agda には C における構造体に相当するレコード型というデータも存在する、
|
|
|
158 record キーワード後の内部に field キーワードを記述し、その下に Name = value の形で値を列挙していく。
|
|
|
159 複数の値を列挙する際は ; で区切る必要がある。
|
|
|
160 Code \ref{agda-record} はレコード型の例であり、Env では varn と vari の二つの field を持ち、
|
|
|
161 それぞれの型が Agda 上で自然数を表す Nat になっている。
|
|
|
162
|
|
8
|
163 \lstinputlisting[caption=record の例,label=agda-record]{src/record.agda.replaced}
|
|
6
|
164 %% \begin{lstlisting}[caption=record の例,label=agda-record]
|
|
|
165 %% record Env : Set where
|
|
|
166 %% field
|
|
|
167 %% varn : ℕ
|
|
|
168 %% vari : ℕ
|
|
|
169 %% \end{lstlisting}
|
|
5
|
170
|
|
8
|
171 関数の定義は、関数名と型を記述した後に関数の本体を = の後に記述する。関数の型には → 、または$->$ を用いる。
|
|
|
172 例えば引数が型 A で返り値が型 B の関数は A $->$ B のように書ける。また、複数の引数を取る関数の型は A $->$ A $->$ B のように書ける。この時の型は A $->$ (A $->$ B) のように考えられる。
|
|
5
|
173 ここでは Code \ref{agda-function}を例にとる。これは引き算の演算子で、Agda の Nat を二つ引数に受けて Nat を返す
|
|
|
174 関数である。
|
|
|
175
|
|
8
|
176 \lstinputlisting[caption=関数の例,label=agda-function]{src/function.agda.replaced}
|
|
|
177 %% \begin{lstlisting}[caption=関数の例,label=agda-function]
|
|
|
178 %% _-_ : ℕ →ℕ →ℕ
|
|
|
179 %% x - zero = x
|
|
|
180 %% zero - _ = zero
|
|
|
181 %% (suc x) - (suc y) = x - y
|
|
|
182 %% \end{lstlisting}
|
|
5
|
183
|
|
|
184 Agda での証明では型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明が完成する。
|
|
|
185 証明の例として Code \ref{proof} を見る。
|
|
|
186 ここでの $+zero$ は右から zero を足しても $\equiv$ の両辺は等しいことを証明している。
|
|
|
187 これは、引数として受けている y が Nat なので、 zero の時と suc y の二つの場合を証明する必要がある。
|
|
|
188
|
|
|
189 $y = zero$ の時は両辺が zero とできて、左右の項が等しいということを表す refl で証明することができる。
|
|
|
190 $y = suc y$ の時は x == y の時 fx == fy が成り立つという cong を使って、y の値を 1 減らしたのちに再帰的に $+zero y$
|
|
|
191 を用いて証明している。
|
|
8
|
192 \lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced}
|
|
|
193 %% \begin{lstlisting}[caption=等式変形の例,label=proof]
|
|
|
194 %% +zero : { y : ℕ } → y + zero ≡ y
|
|
|
195 %% +zero {zero} = refl
|
|
|
196 %% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
|
|
|
197 %% \end{lstlisting}
|
|
5
|
198
|
|
|
199 また、他にも $\lambda$ 項部分で等式を変形する構文が存在している。
|
|
|
200 Code \ref{agda-term-pre}、 \ref{agda-term-post} は等式変形の例である。
|
|
|
201 始めに等式変形を始めたいところで $let open \equiv-Reasoning in begin$と記述する。
|
|
|
202 Agda 上では分からないところを ? と置いておくことができるので、残りを ? としておく。
|
|
|
203 $--$ は Agda 上ではコメントである。
|
|
|
204
|
|
8
|
205 \lstinputlisting[caption=等式変形の例1/2,label=agda-term-pre]{src/term1.agda.replaced}
|
|
|
206 %% \begin{lstlisting}[caption=等式変形の例1/3,label=agda-term-pre]
|
|
|
207 %% stmt2Cond : {c10 : ℕ} → Cond
|
|
|
208 %% stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
|
|
5
|
209
|
|
8
|
210 %% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\
|
|
|
211 %% 10})
|
|
|
212 %% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
|
|
|
213 %% begin
|
|
|
214 %% ? -- ?0
|
|
|
215 %% ≡⟨ ? ⟩ -- ?1
|
|
|
216 %% ? -- ?2
|
|
|
217 %% ∎ )
|
|
5
|
218
|
|
8
|
219 %% -- ?0 : Bool
|
|
|
220 %% -- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) ≡ true
|
|
|
221 %% -- ?2 : Bool
|
|
|
222 %% \end{lstlisting}
|
|
5
|
223
|
|
9
|
224 この状態で実行すると ? 部分に入る型を Agda が示してくれる。
|
|
|
225 始めに変形する等式を ?0 に記述し、?1 の中に $x == y$ のような変形規則を入れることで等式を変形して証明することができる。
|
|
5
|
226
|
|
|
227 ここでは \ref{agda-term-mid} の Bool 値 x を受け取って $x \wedge true$ の時必ず x であるという証明 $\wedge$true と 値と Env を受け取って Bool 値を返す stmt1Cond を使って等式変形を行う。
|
|
8
|
228 \lstinputlisting[caption=使っている等式変形規則,label=agda-term-mid]{src/term2.agda.replaced}
|
|
|
229 %% \begin{lstlisting}[caption=等式変形の例2/3,label=agda-term-mid]
|
|
|
230 %% ∧true : { x : Bool } → x ∧ true ≡ x
|
|
|
231 %% ∧true {x} with x
|
|
|
232 %% ∧true {x} | false = refl
|
|
|
233 %% ∧true {x} | true = refl
|
|
5
|
234
|
|
8
|
235 %% stmt1Cond : {c10 : ℕ} → Cond
|
|
|
236 %% stmt1Cond {c10} env = Equal (varn env) c10
|
|
|
237 %% \end{lstlisting}
|
|
5
|
238
|
|
|
239 最終的な証明は\ref{agda-term-post} のようになる。
|
|
8
|
240 \lstinputlisting[caption=等式変形の例2/2,label=agda-term-post]{src/term3.agda.replaced}
|
|
|
241 %% \begin{lstlisting}[caption=等式変形の例2/2,label=agda-term-post]
|
|
|
242 %% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c\
|
|
|
243 %% 10})
|
|
|
244 %% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
|
|
|
245 %% begin
|
|
|
246 %% (Equal (varn env) c10 ) ∧ true
|
|
|
247 %% ≡⟨ ∧true ⟩
|
|
|
248 %% Equal (varn env) c10
|
|
|
249 %% ≡⟨ cond ⟩
|
|
|
250 %% true
|
|
|
251 %% ∎ )
|
|
|
252 %% \end{lstlisting}
|
|
5
|
253
|
|
2
|
254
|
|
0
|
255 \section{GearsOS}
|
|
1
|
256 Gears OS は信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に開発している OSである。
|
|
|
257
|
|
|
258 Gears OS は処理の単位を Code Gear、データの単位を Data Gear と呼ばれる単位でプログラムを構成する。
|
|
|
259 信頼性や拡張性はメタ計算として、通常の計算とは区別して記述する。
|
|
9
|
260 Gears OS は Code Gear、Data Gear を用いたプログラミング言語である CbC(Continuation based C) で実装される。
|
|
|
261 そのため、Gears OS の実装は Gears を用いたプログラミングスタイルの指標となる。
|
|
1
|
262
|
|
0
|
263 \section{CodeGearとDataGear}
|
|
1
|
264 Gears OS ではプログラムとデータの単位として CodeGear、 DataGear を用いる。 Gear
|
|
|
265 は並列実行の単位、データ分割、 Gear 間の接続等になる。
|
|
5
|
266 CodeGear はプログラムの処理そのもので、図 Code \ref{fig:cgdg}で示しているように任意の数の
|
|
1
|
267 Input DataGear を参照し、処理が完了すると任意の数の Output DataGear に書き込む。
|
|
|
268
|
|
|
269 CodeGear 間の移動は継続を用いて行われる。継続は関数呼び出しとは異なり、呼び出し
|
|
5
|
270 た後に元のコードに戻らず、次の CodeGear へ継続を行う。
|
|
|
271 これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。
|
|
1
|
272
|
|
|
273 \begin{figure}[htpb]
|
|
|
274 \begin{center}
|
|
8
|
275 \scalebox{0.425}{\includegraphics{pic/meta_cg_dg.pdf}}
|
|
1
|
276 \end{center}
|
|
|
277 \caption{CodeGear と DataGear の関係}
|
|
|
278 \label{fig:cgdg}
|
|
|
279 \end{figure}
|
|
|
280
|
|
9
|
281 CodeGear の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行うことができる。
|
|
|
282 このメタ計算部分で assertion などの検証を行うことで、 CodeGear の処理に手を加えることなく検証を行う。
|
|
4
|
283
|
|
9
|
284 \section{Gears と Agda}
|
|
4
|
285 %% CbC の CodeGear, DataGear を用いたプログラミングスタイルと Agda での対応
|
|
5
|
286 ここでは Gears を用いたプログラムを検証するため、
|
|
9
|
287 Agda 上での CodeGear、 DataGear との対応をみていく。
|
|
4
|
288
|
|
1
|
289 CodeGear は Agda では継続渡しで書かれた関数と等価である。
|
|
|
290 継続は不定の型 (\verb+t+) を返す関数で表される。
|
|
|
291 CodeGear 自体も同じ型 \verb+t+ を返す関数となる。
|
|
9
|
292 このとき、継続に渡される引数や、関数から出力される値が DataGear と等価になる。
|
|
8
|
293 Code \ref{agda-cg}は Agda で書いた CodeGear の型の例である。
|
|
1
|
294
|
|
8
|
295 \lstinputlisting[caption= whileTest の型,label=agda-cg]{src/while-test.agda.replaced}
|
|
|
296 %% \begin{lstlisting}[caption= whileTest の型,label=agda-cg]
|
|
|
297 %% whileTest : {l : Level} {t : Set l} -> (c10 : ℕ) → (Code : Env -> t) -> t
|
|
|
298 %% whileTest c10 next = next (record {varn = c10 ; vari = 0} )
|
|
|
299 %% \end{lstlisting}
|
|
1
|
300
|
|
|
301
|
|
|
302 GearsOS で CodeGear の性質を証明するには、 Agda で記述された CodeGear と
|
|
5
|
303 DataGear に対して証明を行う。証明すべき性質は、不定の型を持つ継続
|
|
|
304 \verb+t+ に記述することができる。
|
|
|
305 例えば、 Code \ref{gears-proof} では $(vari e) ≡ 10 $ が証明したい命題で、whileTest
|
|
|
306 から、whileLoop の CodeGear に継続した後、この命題が正しければよい。
|
|
|
307 この証明は proof1 の型に対応する$\lambda$項を与えると証明が完了したことになる。
|
|
9
|
308 ここで与えている refl は左右の項が等しいというもので、ここでの命題が正しいことが証明できている。
|
|
1
|
309
|
|
|
310 % \begin{verbatim}
|
|
5
|
311 \begin{lstlisting}[caption=Agda での証明の例,label=gears-proof]
|
|
|
312 proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
|
|
|
313 proof1 = refl
|
|
1
|
314 \end{lstlisting}
|
|
|
315 % \end{verbatim}
|
|
|
316
|
|
5
|
317 %% \section{HoareLogic}
|
|
|
318 %% %% HoareLogic の説明と Commands、 Rules の説明。公理としてのものなのですべて説明。
|
|
1
|
319
|
|
5
|
320 %% HoareLogic とは C.A.R Hoare、 R.W Floyd らによるプログラムの検証のアイディアである。
|
|
|
321 %% これはプログラムの部分的な正当性を検証するアイディアで、
|
|
|
322 %% 事前条件(Pre-Condition) P が成り立つとき、コマンド C を実行した後に
|
|
|
323 %% 事後条件(Post-Condition) Q が成り立つ。
|
|
|
324 %% これを ${P} C {Q}$ のように表し、コマンドをつなげてプログラム全体を記述することで、
|
|
|
325 %% プログラム内のすべての部分について検証を行うことができる。
|
|
|
326 %% %% これは、プログラムを Skip、 Abort、 Seq、 PComm、 If、 While の6つの規則で記述することで
|
|
4
|
327
|
|
5
|
328 %% HoareLogic ではプログラムを Assign、 Sequential Composition、 If、 While というコマンドで
|
|
|
329 %% 記述する。
|
|
4
|
330
|
|
|
331 %% Skip は動作をしないコマンドで事前条件や事後条件に変化を与えない。
|
|
|
332 %% About は途中で処理を中断するコマンドで Skip と同様、条件に変化を与えることはない。
|
|
|
333 %% Assign は変数に値を代入するコマンドで、事前条件では代入する前の変数が存在することと
|
|
|
334 %% 事後条件ではその変数に値が代入されていることになる。
|
|
|
335 %% Sequential
|
|
1
|
336
|
|
0
|
337
|
|
2
|
338 \section{AgdaでのHoareLogic}
|
|
5
|
339
|
|
|
340 % Agda 上での HoareLogic についての記述と検証を行う。
|
|
|
341
|
|
|
342 今回は、 Code \ref{agda-while} のような while Loop に対しての検証を行う。
|
|
2
|
343
|
|
8
|
344 \begin{lstlisting}[caption=while Loop Program,label=agda-while]
|
|
2
|
345 n = 10;
|
|
|
346 i = 0;
|
|
|
347
|
|
|
348 while (n>0)
|
|
|
349 {
|
|
|
350 i++;
|
|
|
351 n--;
|
|
|
352 }
|
|
|
353 \end{lstlisting}
|
|
|
354
|
|
5
|
355 Code \ref{agda-while}では最初期の事前条件は何もなく、プログラムが停止するときの条件として、 $i==10 ∧ n == 0$ が成り立つ。
|
|
|
356 また、 $n = 10$、 $i = 0$、 といった代入に事前条件と、事後条件をつけ、 while 文にループの普遍条件をつけることになる。
|
|
2
|
357
|
|
5
|
358 現在 Agda 上での HoareLogic は初期の Agda で実装されたもの \cite{agda-alpa}とそれを現在のAgdaに対応させたもの \cite{agda2-hoare}が存在している。
|
|
|
359
|
|
|
360 今回は現在のAgdaに対応させたもの \cite{agda2-hoare}の Command と証明のためのルールを使って HoareLogic を実装した。
|
|
|
361 Code \ref{agda-hoare} は Agda上での HoareLogic の構築子である。
|
|
|
362 ここでの Comm は Agda2 に対応した Command の定義をそのまま使っている。
|
|
2
|
363
|
|
5
|
364 % Code \ref{agda-alfa} \cite{agda2-hoare}
|
|
|
365 $Env$ は Code \ref{agda-while}の n、 i といった変数をまとめたものであり、型として Agda 上での自然数の型である Nat を持つ。
|
|
|
366
|
|
2
|
367 PrimComm は Primitive Command で、 n、i といった変数に 代入するときに使用される関数である。
|
|
5
|
368
|
|
|
369 Cond は HoareLogic の Condition で、 Env を受け取って Bool 値を返す関数となっている。
|
|
|
370
|
|
|
371
|
|
2
|
372 Agda のデータで定義されている Comm は HoareLogic での Command を表す。
|
|
5
|
373
|
|
2
|
374 Skip は何も変更しない Command で、 Abort はプログラムを中断する Command である。
|
|
|
375
|
|
5
|
376 PComm は PrimComm を受けて Command を返す型で定義されており、 変数を代入するときに使われる。
|
|
|
377
|
|
|
378 Seq は Sequence で Command を2つ受けて Command を返す型で定義されている。
|
|
|
379 これは、ある Command から Command に移り、その結果を次の Command に渡す型になっている。
|
|
|
380
|
|
|
381 If は Cond と Comm を2つ受け取り、 Cond が true か false かで 実行する Comm を変える Command である。
|
|
|
382
|
|
2
|
383 While は Cond と Comm を受け取り、 Cond の中身が True である間、 Comm を繰り返す Command である。
|
|
|
384
|
|
|
385 \begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare]
|
|
|
386 PrimComm : Set
|
|
|
387 PrimComm = Env → Env
|
|
|
388
|
|
|
389 Cond : Set
|
|
|
390 Cond = (Env → Bool)
|
|
|
391
|
|
|
392 data Comm : Set where
|
|
|
393 Skip : Comm
|
|
|
394 Abort : Comm
|
|
|
395 PComm : PrimComm -> Comm
|
|
|
396 Seq : Comm -> Comm -> Comm
|
|
|
397 If : Cond -> Comm -> Comm -> Comm
|
|
|
398 While : Cond -> Comm -> Comm
|
|
|
399 \end{lstlisting}
|
|
|
400
|
|
|
401 Agda 上の HoareLogic で使われるプログラムは Comm 型の関数となる。
|
|
|
402 プログラムの処理を Seq でつないでいき、最終的な状態にたどり着くと値を返して止まる。
|
|
5
|
403 %% Code \ref{agda-hoare-simpl} は 変数 $i$、 $n$ に代入を行うプログラムである。
|
|
2
|
404 %% これは Seq で PComm を2つ繋げた形になる。
|
|
5
|
405 Code \ref{agda-hoare-prog}は Code \ref{agda-while}で書いた While Loop を HoareLogic での Comm で記述したものである。
|
|
|
406 ここでの $\$$は $()$の対応を合わせる Agda の糖衣構文で、行頭から行末までを $()$で囲っていることと同義である。
|
|
2
|
407
|
|
8
|
408 \begin{lstlisting}[caption= HoareLogic のプログラム ,label=agda-hoare-prog,mathescape=false]
|
|
2
|
409 program : Comm
|
|
|
410 program =
|
|
|
411 Seq ( PComm (λ env → record env {varn = 10}))
|
|
|
412 $ Seq ( PComm (λ env → record env {vari = 0}))
|
|
|
413 $ While (λ env → lt zero (varn env ) )
|
|
|
414 (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
|
|
|
415 $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
|
|
|
416 \end{lstlisting}
|
|
|
417
|
|
5
|
418 この Comm は Command をならべているだけである。
|
|
|
419 この Comm を Agda 上で実行するため、 Code \ref{agda-hoare-interpret} のような interpreter を記述した。
|
|
|
420
|
|
2
|
421 \begin{lstlisting}[caption=Agda での HoareLogic interpreter ,label=agda-hoare-interpret]
|
|
|
422 {-# TERMINATING #-}
|
|
|
423 interpret : Env → Comm → Env
|
|
|
424 interpret env Skip = env
|
|
|
425 interpret env Abort = env
|
|
|
426 interpret env (PComm x) = x env
|
|
|
427 interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
|
|
|
428 interpret env (If x then else) with x env
|
|
|
429 ... | true = interpret env then
|
|
|
430 ... | false = interpret env else
|
|
|
431 interpret env (While x comm) with x env
|
|
|
432 ... | true = interpret (interpret env comm) (While x comm)
|
|
|
433 ... | false = env
|
|
|
434 \end{lstlisting}
|
|
|
435
|
|
5
|
436 Code \ref{agda-hoare-interpret}は 初期状態の Env と 実行する Command の並びを受けとって、実行後の Env を返すものとなっている。
|
|
2
|
437
|
|
|
438 \begin{lstlisting}[caption=Agda での HoareLogic の実行 ,label=agda-hoare-run]
|
|
|
439 test : Env
|
|
5
|
440 test = interpret ( record { vari = 0 ; varn = 0 } ) program
|
|
2
|
441 \end{lstlisting}
|
|
5
|
442
|
|
|
443 Code \ref{agda-hoare-run}のように interpret に $vari = 0 , varn = 0$ の record を渡し、 実行する Comm を渡して 評価してやると$record { varn = 0 ; vari = 10 }$ のような Env が返ってくる。
|
|
2
|
444
|
|
|
445 次に先程書いたプログラムの証明について記述する。
|
|
|
446
|
|
5
|
447 Code \ref{agda-hoare-rule} は Agda 上での HoareLogic での証明の構成である。
|
|
2
|
448 HTProof では Condition と Command もう一つ Condition を受け取って、 Set を返す Agda のデータである。
|
|
|
449 -- これは Pre と Post の Condition を Command で変化させる
|
|
5
|
450 ここでの HTProof \cite{agda2-hoare} も Agda2 に移植されたものを使っている。
|
|
|
451
|
|
|
452 PrimRule は Code \ref{axiom-taut} の Axiom という関数を使い、事前条件が成り立っている時、
|
|
|
453 実行後に事後条件が成り立つならば、 PComm で変数に値を代入できることを保証している。
|
|
|
454
|
|
|
455 SkipRule は Condition を受け取ってそのままの Condition を返すことを保証する。
|
|
|
456
|
|
|
457 AbortRule は PreContition を受け取って、Abort を実行して終わるルールである。
|
|
|
458
|
|
|
459 WeakeningRule は \ref{axiom-taut} の Tautology という関数を使って通常の逐次処理から、
|
|
|
460 WhileRule のみに適応されるループ不変変数に移行する際のルールである。
|
|
|
461
|
|
|
462 SeqRule は3つの Condition と 2つの Command を受け取り、これらのプログラムの逐次的な実行を保証する。
|
|
|
463
|
|
|
464 IfRule は分岐に用いられ、3つの Condition と 2つの Command を受け取り、判定の Condition が成り立っているかいないかで実行する Command を変えるルールである。
|
|
|
465 この時、どちらかの Command が実行されることを保証している。
|
|
|
466
|
|
|
467 WhileRule はループに用いられ、1つの Command と２つの Condition を受け取り、事前条件が成り立っている間、 Command を繰り返すことを保証している。
|
|
|
468
|
|
9
|
469 \lstinputlisting[caption=Axiom と Tautology,label=axiom-taut]{src/axiom-taut.agda.replaced}
|
|
|
470 %% \begin{lstlisting}[caption=Axiom と Tautology,label=axiom-taut]
|
|
|
471 %% _⇒_ : Bool → Bool → Bool
|
|
|
472 %% false ⇒ _ = true
|
|
|
473 %% true ⇒ true = true
|
|
|
474 %% true ⇒ false = false
|
|
5
|
475
|
|
9
|
476 %% Axiom : Cond -> PrimComm -> Cond -> Set
|
|
|
477 %% Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true
|
|
5
|
478
|
|
9
|
479 %% Tautology : Cond -> Cond -> Set
|
|
|
480 %% Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true
|
|
|
481 %% \end{lstlisting}
|
|
2
|
482
|
|
|
483 \begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare-rule]
|
|
|
484 data HTProof : Cond -> Comm -> Cond -> Set where
|
|
|
485 PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
|
|
|
486 (pr : Axiom bPre pcm bPost) ->
|
|
|
487 HTProof bPre (PComm pcm) bPost
|
|
|
488 SkipRule : (b : Cond) -> HTProof b Skip b
|
|
|
489 AbortRule : (bPre : Cond) -> (bPost : Cond) ->
|
|
|
490 HTProof bPre Abort bPost
|
|
|
491 WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
|
|
|
492 {bPost' : Cond} -> {bPost : Cond} ->
|
|
|
493 Tautology bPre bPre' ->
|
|
|
494 HTProof bPre' cm bPost' ->
|
|
|
495 Tautology bPost' bPost ->
|
|
|
496 HTProof bPre cm bPost
|
|
|
497 SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
|
|
|
498 {cm2 : Comm} -> {bPost : Cond} ->
|
|
|
499 HTProof bPre cm1 bMid ->
|
|
|
500 HTProof bMid cm2 bPost ->
|
|
|
501 HTProof bPre (Seq cm1 cm2) bPost
|
|
|
502 IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
|
|
|
503 {bPre : Cond} -> {bPost : Cond} ->
|
|
|
504 {b : Cond} ->
|
|
|
505 HTProof (bPre /\ b) cmThen bPost ->
|
|
|
506 HTProof (bPre /\ neg b) cmElse bPost ->
|
|
|
507 HTProof bPre (If b cmThen cmElse) bPost
|
|
|
508 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
|
|
|
509 HTProof (bInv /\ b) cm bInv ->
|
|
|
510 HTProof bInv (While b cm) (bInv /\ neg b)
|
|
|
511 \end{lstlisting}
|
|
|
512
|
|
5
|
513 Code \ref{agda-hoare-rule}を使って Code \ref{agda-while}の whileProgram を証明する。
|
|
2
|
514
|
|
6
|
515 全体の証明は Code \ref{agda-hoare-while}の proof1 の様になる。
|
|
5
|
516 proof1 では型で initCond、 Code \ref{agda-hoare-prog}のprogram、 termCond を記述しており、
|
|
|
517 initCond から program を実行し termCond に行き着く HoareLogic の証明になっている。
|
|
|
518
|
|
6
|
519 それぞれの Condition は Rule の後に記述されている {} に囲まれた部分で、
|
|
|
520 initCondのみ無条件で true を返す Condition になっている。
|
|
|
521
|
|
|
522 それぞれの Rule の中にそこで証明する必要のある補題が lemma で埋められている。
|
|
9
|
523 lemma1 から lemma5 の証明は幅を取ってしまうため、 詳細は当研究室レポジトリ \cite{cr-ryukyu} のプログラムを参照していただきたい。
|
|
6
|
524
|
|
|
525 これらの lemma は HTProof の Rule に沿って必要なものを記述されており、
|
|
|
526 lemma1 では PreCondition と PostCondition が存在するときの代入の保証、
|
|
|
527 lemma2 では While Loop に入る前の Condition からループ不変条件への変換の証明、
|
|
|
528 lemma3 では While Loop 内での PComm の代入の証明、
|
|
|
529 lemma4 では While Loop を抜けたときの Condition の整合性、
|
|
|
530 lemma5 では While Loop を抜けた後のループ不変条件からCondition への変換と termCond への移行の整合性を保証している。
|
|
5
|
531
|
|
|
532 \begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]
|
|
2
|
533 proof1 : HTProof initCond program termCond
|
|
|
534 proof1 =
|
|
|
535 SeqRule {λ e → true} ( PrimRule empty-case )
|
|
|
536 $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 )
|
|
|
537 $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 (
|
|
|
538 WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
|
|
|
539 $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 )
|
|
|
540 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5
|
|
|
541 \end{lstlisting}
|
|
|
542
|
|
6
|
543 %% \begin{lstlisting}[caption=whileProgram Condition, label=while-cond]
|
|
|
544 %% initCond : Cond
|
|
|
545 %% initCond env = true
|
|
|
546
|
|
8
|
547 %% stmt1Cond : {c10 : ℕ} → Cond
|
|
6
|
548 %% stmt1Cond {c10} env = Equal (varn env) c10
|
|
|
549
|
|
|
550 %% init-case : {c10 : ℕ} → (env : Env) → (( λ e → true ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari \
|
|
|
551 %% = vari env }) ) ≡ true
|
|
|
552 %% init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl )
|
|
|
553
|
|
|
554 %% init-type : {c10 : ℕ} → Axiom (λ env → true) (λ env → record { varn = c10 ; vari = vari env }) (stmt1Co\
|
|
|
555 %% nd {c10})
|
|
|
556 %% init-type {c10} env = init-case env
|
|
|
557
|
|
8
|
558 %% stmt2Cond : {c10 : ℕ} → Cond
|
|
6
|
559 %% stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)
|
|
|
560
|
|
8
|
561 %% whileInv : {c10 : ℕ} → Cond
|
|
6
|
562 %% whileInv {c10} env = Equal ((varn env) + (vari env)) c10
|
|
|
563
|
|
8
|
564 %% whileInv' : {c10 : ℕ} → Cond
|
|
6
|
565 %% whileInv' {c10} env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env)
|
|
|
566
|
|
8
|
567 %% termCond : {c10 : ℕ} → Cond
|
|
6
|
568 %% termCond {c10} env = Equal (vari env) c10
|
|
|
569 %% \end{lstlisting}
|
|
|
570
|
|
5
|
571 %% \begin{lstlisting}[caption=proof1 の lemma ,label=agda-hoare-while-lemma]
|
|
8
|
572 %% lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10})
|
|
5
|
573 %% (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
|
|
|
574 %% lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
|
|
|
575 %% begin
|
|
|
576 %% (Equal (varn env) c10 ) ∧ true
|
|
|
577 %% ≡⟨ ∧true ⟩
|
|
|
578 %% Equal (varn env) c10
|
|
|
579 %% ≡⟨ cond ⟩
|
|
|
580 %% true
|
|
|
581 %% ∎ )
|
|
4
|
582
|
|
8
|
583 %% lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10
|
|
5
|
584 %% lemma21 eq = Equal→≡ (∧-pi1 eq)
|
|
8
|
585 %% lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0
|
|
5
|
586 %% lemma22 eq = Equal→≡ (∧-pi2 eq)
|
|
8
|
587 %% lemma23 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10
|
|
5
|
588 %% lemma23 {env} {c10} eq = let open ≡-Reasoning in
|
|
|
589 %% begin
|
|
|
590 %% varn env + vari env
|
|
|
591 %% ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq ) ⟩
|
|
|
592 %% c10 + vari env
|
|
|
593 %% ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩
|
|
|
594 %% c10 + 0
|
|
|
595 %% ≡⟨ +-sym {c10} {0} ⟩
|
|
|
596 %% 0 + c10
|
|
|
597 %% ≡⟨⟩
|
|
|
598 %% c10
|
|
|
599 %% ∎
|
|
8
|
600 %% lemma2 : {c10 : ℕ} → Tautology stmt2Cond whileInv
|
|
5
|
601 %% lemma2 {c10} env = bool-case (stmt2Cond env) (
|
|
|
602 %% λ eq → let open ≡-Reasoning in
|
|
|
603 %% begin
|
|
|
604 %% (stmt2Cond env) ⇒ (whileInv env)
|
|
|
605 %% ≡⟨⟩
|
|
|
606 %% (stmt2Cond env) ⇒ ( Equal (varn env + vari env) c10 )
|
|
|
607 %% ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩
|
|
|
608 %% (stmt2Cond env) ⇒ (Equal c10 c10)
|
|
|
609 %% ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl ) ⟩
|
|
|
610 %% (stmt2Cond {c10} env) ⇒ true
|
|
|
611 %% ≡⟨ ⇒t ⟩
|
|
|
612 %% true
|
|
|
613 %% ∎
|
|
|
614 %% ) (
|
|
|
615 %% λ ne → let open ≡-Reasoning in
|
|
|
616 %% begin
|
|
|
617 %% (stmt2Cond env) ⇒ (whileInv env)
|
|
|
618 %% ≡⟨ cong ( \ x -> x ⇒ (whileInv env) ) ne ⟩
|
|
|
619 %% false ⇒ (whileInv {c10} env)
|
|
|
620 %% ≡⟨ f⇒ {whileInv {c10} env} ⟩
|
|
|
621 %% true
|
|
|
622 %% ∎
|
|
|
623 %% )
|
|
|
624 %% lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
|
|
|
625 %% lemma3 env = impl⇒ ( λ cond → let open ≡-Reasoning in
|
|
|
626 %% begin
|
|
|
627 %% whileInv' (record { varn = varn env ; vari = vari env + 1 })
|
|
|
628 %% ≡⟨⟩
|
|
|
629 %% Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) )
|
|
|
630 %% ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond ) ⟩
|
|
|
631 %% Equal (varn env + (vari env + 1)) (suc c10) ∧ true
|
|
|
632 %% ≡⟨ ∧true ⟩
|
|
|
633 %% Equal (varn env + (vari env + 1)) (suc c10)
|
|
|
634 %% ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩
|
|
|
635 %% Equal ((varn env + vari env) + 1) (suc c10)
|
|
|
636 %% ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩
|
|
|
637 %% Equal (suc (varn env + vari env)) (suc c10)
|
|
|
638 %% ≡⟨ sym Equal+1 ⟩
|
|
|
639 %% Equal ((varn env + vari env) ) c10
|
|
|
640 %% ≡⟨ ∧-pi1 cond ⟩
|
|
|
641 %% true
|
|
|
642 %% ∎ )
|
|
8
|
643 %% lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true → Equal ((varn env - 1) + vari env) c10 ≡ true
|
|
5
|
644 %% lemma41 env {c10} c1 c2 = let open ≡-Reasoning in
|
|
|
645 %% begin
|
|
|
646 %% Equal ((varn env - 1) + vari env) c10
|
|
6
|
647 %% ≡⟨ cong ( λ z → Equal ((z - 1 ) + vari env ) c10 ) (sym (suc-pred*ℕ*=n c2) ) ⟩
|
|
|
648 %% Equal ((suc (pred*ℕ* {varn env} c2 ) - 1) + vari env) c10
|
|
5
|
649 %% ≡⟨⟩
|
|
6
|
650 %% Equal ((pred*ℕ* {varn env} c2 ) + vari env) c10
|
|
5
|
651 %% ≡⟨ Equal+1 ⟩
|
|
6
|
652 %% Equal ((suc (pred*ℕ* {varn env} c2 )) + vari env) (suc c10)
|
|
|
653 %% ≡⟨ cong ( λ z → Equal (z + vari env ) (suc c10) ) (suc-pred*ℕ*=n c2 ) ⟩
|
|
5
|
654 %% Equal (varn env + vari env) (suc c10)
|
|
|
655 %% ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩
|
|
|
656 %% Equal (suc c10) (suc c10)
|
|
|
657 %% ≡⟨ ≡→Equal refl ⟩
|
|
|
658 %% true
|
|
|
659 %% ∎
|
|
8
|
660 %% lemma4 : {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
|
|
5
|
661 %% lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
|
|
|
662 %% begin
|
|
|
663 %% whileInv (record { varn = varn env - 1 ; vari = vari env })
|
|
|
664 %% ≡⟨⟩
|
|
|
665 %% Equal ((varn env - 1) + vari env) c10
|
|
|
666 %% ≡⟨ lemma41 env (Equal→≡ (∧-pi1 cond)) (∧-pi2 cond) ⟩
|
|
|
667 %% true
|
|
|
668 %% ∎
|
|
|
669 %% )
|
|
|
670 %% lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero
|
|
|
671 %% lemma51 z cond with lt zero (varn z) | (suc zero) ≤? (varn z)
|
|
|
672 %% lemma51 z () | false | yes p
|
|
|
673 %% lemma51 z () | true | yes p
|
|
|
674 %% lemma51 z refl | _ | no ¬p with varn z
|
|
|
675 %% lemma51 z refl | _ | no ¬p | zero = refl
|
|
|
676 %% lemma51 z refl | _ | no ¬p | suc x = ⊥-elim ( ¬p (s≤s z≤n ) )
|
|
8
|
677 %% lemma5 : {c10 : ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond
|
|
5
|
678 %% lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
|
|
|
679 %% begin
|
|
|
680 %% termCond env
|
|
|
681 %% ≡⟨⟩
|
|
|
682 %% Equal (vari env) c10
|
|
|
683 %% ≡⟨⟩
|
|
|
684 %% Equal (zero + vari env) c10
|
|
|
685 %% ≡⟨ cong ( λ z → Equal (z + vari env) c10 ) (sym ( lemma51 env ( ∧-pi2 cond ) )) ⟩
|
|
|
686 %% Equal (varn env + vari env) c10
|
|
|
687 %% ≡⟨ ∧-pi1 cond ⟩
|
|
|
688 %% true
|
|
|
689 %% ∎
|
|
|
690 %% )
|
|
|
691 %% \end{lstlisting}
|
|
8
|
692 proof1 は Code \ref{agda-hoare-prog}の program と似た形をとっている。
|
|
5
|
693 HoareLogic では Comannd に対応する証明規則があるため、証明はプログラムに対応する形になる。
|
|
|
694
|
|
|
695 \section{Gears ベースの HoareLogic の証明}
|
|
|
696 次に Gears をベースにした HoareLogic の例を見ていく。
|
|
|
697 Gears を用いた記述では、 Input の DataGear 、 CodeGear、 Output の DataGearという
|
|
|
698 並びでプログラムを記述していく。
|
|
|
699 そのため、Input DataGear を PreCondition、 Command を CodeGear、 Output DataGear を PostCondition と
|
|
|
700 そのまま置き換えることができる。
|
|
|
701
|
|
9
|
702 こちらも通常の HoareLogic と同様に Code \ref{agda-while} のwhileプログラムと同様のものを記述する
|
|
5
|
703 Code \ref{Gears-hoare-while} は、 CodeGear、 DataGear を用いた Agda 上での while Program の記述であり、証明でもある。
|
|
|
704
|
|
8
|
705 \lstinputlisting[caption=Gears 上での WhileLoop の記述と検証,label=Gears-hoare-while]{src/gears.agda.replaced}
|
|
|
706 %% \begin{lstlisting}[caption=Gears 上での WhileLoop の記述と検証,label=Gears-hoare-while]
|
|
|
707 %% proofGears : {c10 : ℕ } → Set
|
|
|
708 %% proofGears {c10} = whileTest {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 ))))
|
|
|
709 %% \end{lstlisting}
|
|
5
|
710 Code \ref{Gears-hoare-while} で使われている CodeGear を見ていく
|
|
|
711
|
|
|
712 始めに Code \ref{gears-while} の whileTest では変数 i、n にそれぞれ 0 と 10 を代入している。
|
|
|
713 whileTest は最初のCodeGear なので initCondition は true で、
|
|
|
714 Code : の後ろに書かれた$(env : Env) -> ((vari env) ≡ 0) /\ ((varn env) ≡ c10)$ が PostCondition である。
|
|
|
715 $\lambda$ 項の next には次のCodeGear が入り、継続される引数である env は whileTest の PostCondition であり、
|
|
|
716 次の CodeGear の PreCondition にあたる。
|
|
|
717 conversion1 は通常の Condition からループ不変条件に移行するためのもので前のCondition である $i == 0 and n == 10$ が
|
|
|
718 成り立っている時、$i + n == 10$ を返すCodeGear となっている。
|
|
|
719 whileLoop では conversion1 のループ不変条件を受け取ってWhile の条件である$0 < n$ が成り立っている間、 $i++;n++$
|
|
|
720 を行う。
|
|
|
721 そして、ループを抜けた後の termCondition は $i == 10$ となる。
|
|
|
722
|
|
8
|
723 \lstinputlisting[caption=Gears whileProgram, label=gears-while]{src/gears-while.agda.replaced}
|
|
|
724 %% \begin{lstlisting}[caption=Gears whileProgram, label=gears-while]
|
|
|
725 %% whileTest : {l : Level} {t : Set l} -> {c10 : ℕ } → (Code : (env : Env) ->
|
|
|
726 %% ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -> t) -> t
|
|
|
727 %% whileTest {_} {_} {c10} next = next env proof2
|
|
|
728 %% where
|
|
|
729 %% env : Env
|
|
|
730 %% env = record {vari = 0 ; varn = c10}
|
|
|
731 %% proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
|
|
|
732 %% proof2 = record {pi1 = refl ; pi2 = refl}
|
|
4
|
733
|
|
8
|
734 %% conversion1 : {l : Level} {t : Set l } → (env : Env) -> {c10 : ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c\
|
|
|
735 %% 10)
|
|
|
736 %% -> (Code : (env1 : Env) -> (varn env1 + vari env1 ≡ c10) -> t) -> t
|
|
|
737 %% conversion1 env {c10} p1 next = next env proof4
|
|
|
738 %% where
|
|
|
739 %% proof4 : varn env + vari env ≡ c10
|
|
|
740 %% proof4 = let open ≡-Reasoning in
|
|
|
741 %% begin
|
|
|
742 %% varn env + vari env
|
|
|
743 %% ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
|
|
|
744 %% c10 + vari env
|
|
|
745 %% ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
|
|
|
746 %% c10 + 0
|
|
|
747 %% ≡⟨ +-sym {c10} {0} ⟩
|
|
|
748 %% c10
|
|
|
749 %% ∎
|
|
5
|
750
|
|
8
|
751 %% {-# TERMINATING #-}
|
|
|
752 %% whileLoop : {l : Level} {t : Set l} -> (env : Env) -> {c10 : ℕ } → ((varn env) + (vari env) ≡ c10) -> (Co\
|
|
|
753 %% de : Env -> t) -> t
|
|
|
754 %% whileLoop env proof next with ( suc zero ≤? (varn env) )
|
|
|
755 %% whileLoop env proof next | no p = next env
|
|
|
756 %% whileLoop env {c10} proof next | yes p = whileLoop env1 (proof3 p ) next
|
|
|
757 %% where
|
|
|
758 %% env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1}
|
|
|
759 %% 1<0 : 1 ≤ zero → ⊥
|
|
|
760 %% 1<0 ()
|
|
|
761 %% proof3 : (suc zero ≤ (varn env)) → varn env1 + vari env1 ≡ c10
|
|
|
762 %% proof3 (s≤s lt) with varn env
|
|
|
763 %% proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p)
|
|
|
764 %% proof3 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in
|
|
|
765 %% begin
|
|
|
766 %% n' + (vari env + 1)
|
|
|
767 %% ≡⟨ cong ( λ z → n' + z ) ( +-sym {vari env} {1} ) ⟩
|
|
|
768 %% n' + (1 + vari env )
|
|
|
769 %% ≡⟨ sym ( +-assoc (n') 1 (vari env) ) ⟩
|
|
|
770 %% (n' + 1) + vari env
|
|
|
771 %% ≡⟨ cong ( λ z → z + vari env ) +1≡suc ⟩
|
|
|
772 %% (suc n' ) + vari env
|
|
|
773 %% ≡⟨⟩
|
|
|
774 %% varn env + vari env
|
|
|
775 %% ≡⟨ proof ⟩
|
|
|
776 %% c10
|
|
|
777 %% ∎
|
|
|
778 %% \end{lstlisting}
|
|
0
|
779
|
|
|
780
|
|
5
|
781 \section{まとめと今後の課題}
|
|
|
782 本研究では Agda 上で HoareLogic のwhileを使った例題を作成し、
|
|
|
783 証明を行なった。
|
|
0
|
784
|
|
5
|
785 また、 Gears を用いた HoareLogic を記述することができた。
|
|
|
786 さらに、Gears を用いてHoareLocic 記述で、
|
|
9
|
787 証明を引数として受け渡して記述することで、証明とプログラムを一体化することができた。
|
|
0
|
788
|
|
5
|
789 今後の課題としては GearsOS の検証のために、
|
|
|
790 RedBlackTree や SynchronizedQueue などのデータ構造の検証をHoareLogic ベースで行うことなどが挙げられる。
|
|
|
791 %% 特に SynchronizedQueue の検証のために、 並列なプログラムを状態遷移に変換する。
|
|
2
|
792
|
|
5
|
793 \nocite{*}
|
|
|
794 \bibliography{tecrep}{}
|
|
|
795 \bibliographystyle{plain}
|
|
0
|
796
|
|
|
797 \end{document}
|
