# HG changeset patch # User ryokka # Date 1581323184 -32400 # Node ID bf3288c36d7e93f3a11a7460f92deb10cfd9b93a # Parent 831316a767e8b0c7fe0429ffecc6de54705dcaa8 update abstract_eng diff -r 831316a767e8 -r bf3288c36d7e paper/abstract.tex --- a/paper/abstract.tex Mon Feb 10 14:20:21 2020 +0900 +++ b/paper/abstract.tex Mon Feb 10 17:26:24 2020 +0900 @@ -1,27 +1,75 @@ -\chapter*{要旨} -\label{c:abstract} +\begin{abstract} + OS やアプリケーションの信頼性は重要である。 信頼性を上げるにはプログラムが仕様を満たしていることを検証する必要がある。 -プログラムの検証手法として、Floyd–Hoare logic (以下 Hoare Logic)が存在している。 -HoareLogic は事前条件が成り立っているときにある -関数を実行して、それが停止する際に事後条件を満たすことを確認することで、検証を行う。 -しかし、 HoareLogic はシンプルなアプローチであるが通常のプログラミング言語で使用することができず、 -広まっているとはいえない。 +プログラムの検証手法として、Floyd–Hoare logic (以下 Hoare Logic)が知られている。 +Hoare Logic は事前条件が成り立っているときにある関数を実行して、それが停止する際に事後条件を満たすことを確認することで、検証を行う。 +Hoare Logic はシンプルなアプローチであるが限定されたコマンド群やwhile programにしか適用されないことが多く、 +複雑な通常のプログラミング言語には向いていない。 + +当研究室では信頼性の高い言語として Continuation based C (CbC)を開発している。 +CbC では CodeGear、DataGear という単位を用いてプログラムを記述する。 + +CodeGearを Agda で継続渡しの記述を用いた関数として記述する。ここで +AgdaはCurry Howard対応にもどつく定理証明系であり、それ自身が関数型プログラング言語でもある。 +Agda では条件を命題として記述することができるので、 +継続に事前条件や事後条件をもたせることができる。 -当研究室では信頼性の高い OS として GearsOS を開発している。 -現在 GearsOS ではCodeGear、DataGearという単位を用いてプログラムを記述する手法を用いており、 -仕様の確認には定理証明系である Agda を用いている。 +既存の言語では条件はassertなどで記述することになるが、その証明をそのプログラミング言語内で行うことはできない。 +Agdaでは証明そのもの、つまり命題に対する推論をλ項として記述することができるので、 +Hoare Logicの証明そのものを Meta Code Gearとして記述できる。これは既存の言語では不可能であった。 +ポイントは、プログラムそのものを Agda baseのCode Gearで記述できることである。 +Code Gearは入力と出力のみを持ち関数呼び出しせずにgoto的に継続実行する。この形式がそのまま +Hoare Logicのコマンドを自然に定義する。 + +Hoare Logicの証明には３つの条件が必要である。一つは +事前条件と事後条件がプログラム全体で正しく接続されていることである。 +ループ(ループを含むCodeGearの接続)で、事前条件と事後条件が等しく、不変条件を構成していること。 +さらに、ループが停止することを示す必要がある。停止しないプログラムに対しては停止性を省いた部分正当性を定義できる。 + +本論文では Agda 上での Hoare Logic の記述を使い、簡単な while Loop のプログラムの作成、証明を行った。 +この証明は停止性と証明全体の健全性を含んでいる。従来はHoare Logicの健全性は制限されたコマンドなどに +対して一般的に示すのが普通であるが、本手法では複雑なCodeGearに対して、個別の証明をMeta CodeGearとして +自分で記述するところに特徴がある。これにより健全性自体の証明が可能になった。 + +\end{abstract} +%% \chapter*{Abstract} + +\begin{abstract_eng} + -CodeGearは Agda 上では継続渡しの記述を用いた関数として -記述する。 -また、継続にある関数を実行するための事前条件や -事後条件などをもたせることが可能である。 +OS and application reliability are important. +To increase reliability, verifications of program with specifications are necessary. +Floyd-Hoare logic (hereafter Hoare Logic) is a welknown program verification method. +Hoare Logic verifies the postonditions of a function are satisfied when the postconditions are satifiles. +It also checks the halt condition of the program. +Hoare Logic is a useful simple approach but often only applies to a limited set of commands and while programs. +It is not generaly suitable for complex ordinary programming languages. + +Our laboratory is developping Continuation based C (CbC) as a reliable language. +In CbC, programs are described using units of CodeGear and DataGear. + +CodeGear can be described in Agda as a function using the description of a light weight continuous passing. +Agda is a theorem proof system based Curry Howard correspondence, and it is also a functional programming language. +In Agda, conditions can be described as propositions, +The continuation can have preconditions and postconditions. -そのため Hoare Logic と CodeGear、DataGear という単位を用いたプログラミング手法 -記述とは相性が良く、既存の言語とは異なり HoareLogic を使ったプログラミングが容易に行えると考えている。 +In existing languages, conditions are described in asserts, etc., but the proof cannot be done in that programming language. +Since Agda can describe the proof itself, that is, the inference among the propositions, as λ terms, +The proof of Hoare Logic itself can be described as Meta Code Gear. This was not possible with existing languages. +The point is that the program itself can be described with Code Gear of Agda base. +Code Gear has only input and output, and executes continuously in a goto manner without calling a function. This format is +naturally define Hoare Logic commands. -本研究では Agda 上での HoareLogic の記述を使い、簡単な while Loop のプログラムの作成、証明を行った。 -また、GearsOS の仕様確認のために CodeGear、DataGear という単位を用いた記述で Hoare Logic をベースと -した while Loop プログラムを記述、その証明を行なった。 +Hoare Logic's proof requires three conditions. One, +Pre-conditions and post-conditions are connected correctly throughout the program. +The preconditions and postconditions are equal in the loop (the connection of CodeGear including the loop) and constitute an invariant condition. +In addition, we need to show that the loop stops. For a program that does not stop, it is possible to define partial validity without stopping. -%% \chapter*{Abstract} +In this paper, we created and proved a simple while Loop program using the description of Hoare Logic on Agda. +This proof includes termination and the overall soundness of the proof. Previously, the soundness of Hoare Logic was limited to rather simple commands. +However, in this method, individual proofs are given as Meta CodeGears for complex CodeGears. + +This made it possible to prove the soundness itself. + +\end{abstract_eng} diff -r 831316a767e8 -r bf3288c36d7e paper/hoare.tex --- a/paper/hoare.tex Mon Feb 10 14:20:21 2020 +0900 +++ b/paper/hoare.tex Mon Feb 10 17:26:24 2020 +0900 @@ -85,19 +85,9 @@ プログラムはコマンド \verb/Comm/を \verb/Seq/ でつないでいき、最終的な状態にたどり着くと値を返して止まる。 - \coderef{agda-hoare-prog}は \coderef{c-while}で書いた While Loop を Hoare Logic でのコマンドで記述したものである。 -ここでの $\$$は $()$の対応を合わせる Agda の糖衣構文で、行頭から行末までを $()$で囲っていることと同義である。 +\coderef{agda-hoare-prog}は \coderef{c-while}で書いた While Loop を Hoare Logic でのコマンドで記述したものである。ここでの $\$$は $()$の対応を合わせる Agda の糖衣構文で、行頭から行末までを $()$で囲っていることと同義である。 -\lstinputlisting[caption= \coderef{c-while} と対応した 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} +比較しやすいように \coderef{c-while} を \coderef{c-while2} に再掲した。 \begin{lstlisting}[caption= while Loop (再掲),label=c-while-2] n = 10; @@ -109,24 +99,19 @@ } \end{lstlisting} +\lstinputlisting[caption= \coderef{c-while2} と対応した 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 を Agda 上で実行するため、 \coderef{agda-hoare-interpret} の \verb/interpret/ 関数を作成した。 - \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} \coderef{agda-hoare-interpret}は 初期状態の \verb/Env/ と 実行する コマンド の並びを受けとって、実行後の \verb/Env/ を返すものとなっている。 \verb/interpret/ 関数は停止性を考慮していないため、 \verb/{-# TERMINATING #-}/ タグを付けている。 @@ -140,7 +125,6 @@ -- record { varn = 0 ; vari = 10 } \end{lstlisting} - \section{While Program の部分正当性} ここでは先程記述した \coderef{agda-hoare-prog} の部分正当性の検証を行う。 @@ -169,37 +153,6 @@ \lstinputlisting[caption=Axiom と Tautology,label=axiom-taut]{src/axiom-taut.agda.replaced} - -%% \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} - \coderef{hoare-rule}を使って \coderef{c-while}の WhileProgram の仕様を構成する。 \lstinputlisting[caption=Agda での Hoare Locig の構成,label=hoare-rule]{src/agda-hoare-rule.agda.replaced} @@ -284,127 +237,6 @@ \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} - \coderef{agda-hoare-prim-soundness} は \verb/HTProof/ で記述された仕様を、実際に満たすことが可能であることを \verb/Satisfies/ が返す。 証明部分では \verb/HTProof/ で構成された使用を受け取り、 \verb/Soundness/ が対応した証明を返すようになっている。 diff -r 831316a767e8 -r bf3288c36d7e paper/master_paper.pdf Binary file paper/master_paper.pdf has changed diff -r 831316a767e8 -r bf3288c36d7e paper/master_paper.tex --- a/paper/master_paper.tex Mon Feb 10 14:20:21 2020 +0900 +++ b/paper/master_paper.tex Mon Feb 10 17:26:24 2020 +0900 @@ -26,8 +26,12 @@ \eyear{March 2020} \author{外間 政尊} \eauthor{Masataka HOKAMA} -\chife{指導教員：教授 玉城 史朗} % 多分このままでもあってる後で確認 + +\chife{指導教員：教授 玉城 史朗} \echife{Supervisor: Prof. Shirou TAMAKI} +%% \chife{　} % 表紙用 +%% \echife{　} + \marklefthead{% 左上に挿入 \begin{minipage}[b]{.4\textwidth} diff -r 831316a767e8 -r bf3288c36d7e paper/src/agda-hoare-soundness.agda.replaced --- a/paper/src/agda-hoare-soundness.agda.replaced Mon Feb 10 14:20:21 2020 +0900 +++ b/paper/src/agda-hoare-soundness.agda.replaced Mon Feb 10 17:26:24 2020 +0900 @@ -9,11 +9,7 @@ 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 + in tautValid bPost' bPost tautPost s2 (hyp s1 s2 (tautValid bPre bPre' tautPre s1 q1) q2) Soundness (SeqRule {bPre} {cm1} {bMid} {cm2} {bPost} pr1 pr2) s1 s2 q1 q2 = let hyp1 : Satisfies bPre cm1 bMid