Mercurial > hg > Papers > 2020 > ryokka-master
changeset 5:196ba119ca89
fix, and add mindmap->pdf
line wrap: on
line diff
--- a/paper/abstract.tex Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/abstract.tex Mon Feb 03 21:47:43 2020 +0900 @@ -1,5 +1,5 @@ \chapter*{要旨} - +\label{c:abstract} OS やアプリケーションの信頼性は重要である。 信頼性を上げるにはプログラムが仕様を満たしていることを検証する必要がある。 プログラムの検証手法として、Floyd–Hoare logic (以下 Hoare Logic)が存在している。
--- a/paper/agda.tex Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/agda.tex Mon Feb 03 21:47:43 2020 +0900 @@ -1,4 +1,5 @@ \chapter{Agda} +\label{c:agda} Adga \cite{agda} とは定理証明支援器であり、関数型言語である。 Agda は依存型という型システムを持っており、型を第一級オブジェクトとして扱うことができる。 また、型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応ため
--- a/paper/cbc.tex Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/cbc.tex Mon Feb 03 21:47:43 2020 +0900 @@ -1,6 +1,6 @@ -% だいたい sigss のやつ +\chapter{Continuation based C} +\label{c:cbc} -\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} による実装が存在する。
--- a/paper/cbc_agda.tex Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/cbc_agda.tex Mon Feb 03 21:47:43 2020 +0900 @@ -1,8 +1,9 @@ \chapter{Continuation based C と Agda} -Agda は CbC の上位言語として使われる。 -また、Agda での検証は CbC でのメタ計算に当たる。 -そのため Agda 上で記述される - CbC はメタ計算を含んだ形で記述することができる。 +\label{c:cbc_agda} +現在 Agda は CbC の上位言語として使用されており、 +Agda で記述された CbC のプログラムはメタ計算を含む形で記述される。 +しかし、 + 本章では当研究室で推奨している単位を用いての検証を行うため、 Agda 上で DataGear、 CodeGear の表現を示す。
--- a/paper/conclusion.tex Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/conclusion.tex Mon Feb 03 21:47:43 2020 +0900 @@ -1,4 +1,5 @@ \chapter{結論} +\label{c:conclusion} まだ終わってないので最後に \section{今後の課題}
--- a/paper/hoare.tex Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/hoare.tex Mon Feb 03 21:47:43 2020 +0900 @@ -1,4 +1,5 @@ \chapter{Floyd-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)が成り立つことを検証する。 @@ -168,7 +169,7 @@ Code \ref{agda-hoare-rule}を使って Code \ref{agda-while}の whileProgram の仕様を構成する。 -\lstinputlisting[caption=Axiom と Tautology,label=axiom-taut{src/agda-hoare-rule.agda.replaced} +\lstinputlisting[caption=Agda での Hoare Locig の構成,label=hoare-rule]{src/agda-hoare-rule.agda.replaced} 全体の仕様は Code \ref{agda-hoare-while}の proof1 の様になる。 proof1 では型で initCond、 Code \ref{agda-hoare-prog}のprogram、 termCond を記述しており、
--- a/paper/introduction.tex Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/introduction.tex Mon Feb 03 21:47:43 2020 +0900 @@ -1,5 +1,6 @@ % sigos のやつ \chapter{プログラミング言語の検証} +\label{chapter:intro} 現在の OS やアプリケーションの検証では、実装と別に検証用の言語で記述された実装と証明を持つのが一般的である。 kernel 検証\cite{Klein:2010:SFV:1743546.1743574},\cite{Nelson:2017:HPV:3132747.3132748}の例では C で記述された Kernel に対して、検証用の別の言語で書かれた等価な kernel を用いて OS の検証を行っている。 また、別のアプローチとしては ATS2\cite{ats2} や Rust\cite{rust} などの低レベル記述向けの関数型言語を実装に用いる手法が存在している。
--- a/paper/master_paper.tex Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/master_paper.tex Mon Feb 03 21:47:43 2020 +0900 @@ -6,20 +6,20 @@ \usepackage{here} \usepackage{listings} \usepackage{comment} +\usepackage{url} \usepackage[deluxe, multi]{otf} -\usepackage{url} -\usepackage{cite} -\usepackage{listings} +%% \usepackage{cite} +%% \usepackage{listings} \usepackage{amssymb} -\usepackage[fleqn]{amsmath} +%% \usepackage[fleqn]{amsmath} -\usepackage[utf8]{inputenc} +%% \usepackage[utf8]{inputenc} %% \input{dummy.tex} %% font \usepackage{type1cm} -\jtitle{} -\etitle{Hoare Logic based Specification and Verification in Continuation based C} +\jtitle{Continuation based C での HoareLogic を用いた仕様記述と検証} +%% \etitle{Hoare Logic based Specification and Verification in Continuation based C} \year{2020年 3月} \eyear{March 2020} \author{外間 政尊} @@ -79,8 +79,7 @@ \newpage -% -要旨 +%要旨 \input{abstract.tex} %発表履歴 @@ -106,12 +105,13 @@ \input{agda.tex} \input{hoare.tex} \input{cbc_agda.tex} -\input{tree.tex} +%% \input{tree.tex} +\input{cbc_hoare.tex} \input{conclusion.tex} %% %謝辞 -%% \addcontentsline{toc}{chapter}{謝辞} -%% \input{thanks.tex} +\addcontentsline{toc}{chapter}{謝辞} +\input{thanks.tex} %参考文献 \nocite{*}
--- a/paper/src/AgdaNPushNPop.agda.replaced Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/src/AgdaNPushNPop.agda.replaced Mon Feb 03 21:47:43 2020 +0900 @@ -6,7 +6,7 @@ n-pop {{mm}} (zero) = M.cs {{mm}} {{mm}} id n-pop {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m @$\rightarrow$@ M.exec {{mm}} {{mm}} (n-pop {m} {{mm}} n) (popOnce m)) -pop-n-push-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\text{1}$@ +pop-n-push-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@ pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta @$\equiv$@ M.exec (n-push {meta} n) meta where
--- a/paper/src/AgdaNPushNPopProof.agda.replaced Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/src/AgdaNPushNPopProof.agda.replaced Mon Feb 03 21:47:43 2020 +0900 @@ -1,4 +1,4 @@ -pop-n-push-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\text{1}$@ +pop-n-push-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@ pop-n-push-type n cn ce s = M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) meta @$\equiv$@ M.exec (n-push n) meta where @@ -30,7 +30,7 @@ -n-push-pop-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\text{1}$@ +n-push-pop-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@ n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop n) (n-push n)) meta @$\equiv$@ meta where meta = id-meta cn ce st
--- a/paper/src/AgdaPushPopProof.agda.replaced Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/src/AgdaPushPopProof.agda.replaced Mon Feb 03 21:47:43 2020 +0900 @@ -2,7 +2,7 @@ id-meta n e s = record { context = record {n = n ; element = just e} ; nextCS = (N.cs id) ; stack = s} -push-pop-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Element @$\mathbb{N}$@ @$\rightarrow$@ Set@$\text{1}$@ +push-pop-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Element @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@ push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta @$\equiv$@ meta where meta = id-meta n e record {top = just (cons x (just s))}
--- a/paper/src/AgdaStackDS.agda.replaced Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/src/AgdaStackDS.agda.replaced Mon Feb 03 21:47:43 2020 +0900 @@ -6,7 +6,7 @@ open import subtype Context as N -record Meta : Set@$\text{1}$@ where +record Meta : Set@$\_{1}$@ where field -- context as set of data segments context : Context
--- a/paper/src/AgdaTreeProof.agda.replaced Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/src/AgdaTreeProof.agda.replaced Mon Feb 03 21:47:43 2020 +0900 @@ -9,13 +9,13 @@ ... | 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 @$\rightarrow$@ - GetRedBlackTree.checkNode t k (@$\lambda$@ t@$\text{1}$@ x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) (root t)) + GetRedBlackTree.checkNode t k (@$\lambda$@ t@$\_{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 @$\rightarrow$@ compare2 x@$\text{1}$@ y } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) + } ) ; nodeStack = s ; compare = @$\lambda$@ x@$\_{1}$@ y @$\rightarrow$@ compare2 x@$\_{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 @$\rightarrow$@ compare2 x@$\text{1}$@ y } ) k + } ) ; nodeStack = record { top = Nothing } ; compare = @$\lambda$@ x@$\_{1}$@ y @$\rightarrow$@ compare2 x@$\_{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
--- a/paper/src/PushPopType.agda.replaced Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/src/PushPopType.agda.replaced Mon Feb 03 21:47:43 2020 +0900 @@ -4,6 +4,6 @@ popOnce : Meta @$\rightarrow$@ Meta popOnce m = M.exec popSingleLinkedStackCS m -push-pop-type : Meta @$\rightarrow$@ Set@$\text{1}$@ +push-pop-type : Meta @$\rightarrow$@ Set@$\_{1}$@ push-pop-type meta = M.exec (M.csComp (M.cs popOnce) (M.cs pushOnce)) meta @$\equiv$@ meta
--- a/paper/src/agda-hoare-soundness.agda.replaced Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/src/agda-hoare-soundness.agda.replaced Mon Feb 03 21:47:43 2020 +0900 @@ -3,7 +3,7 @@ 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 + = substId1 State {Level.zero} {State} {s1} {s2} (proj@$\_{2}$@ q2) (SemCond bPost) q1 Soundness {bPre} {.Abort} {bPost} (AbortRule .bPre .bPost) s1 s2 q1 () Soundness (WeakeningRule {bPre} {bPre'} {cm} {bPost'} {bPost} tautPre pr tautPost) s1 s2 q1 q2 @@ -21,13 +21,13 @@ hyp2 : Satisfies bMid cm2 bPost hyp2 = Soundness pr2 sMid : State - sMid = proj@$\text{1}$@ q2 + sMid = proj@$\_{1}$@ q2 r1 : SemComm cm1 s1 sMid @$\times$@ SemComm cm2 sMid s2 - r1 = proj@$\text{2}$@ q2 + r1 = proj@$\_{2}$@ q2 r2 : SemComm cm1 s1 sMid - r2 = proj@$\text{1}$@ r1 + r2 = proj@$\_{1}$@ r1 r3 : SemComm cm2 sMid s2 - r3 = proj@$\text{2}$@ r1 + r3 = proj@$\_{2}$@ r1 r4 : SemCond bMid sMid r4 = hyp1 s1 sMid q1 r2 in hyp2 sMid s2 r4 r3 @@ -43,13 +43,13 @@ SemCond bPost s2 rThen = @$\lambda$@ h @$\rightarrow$@ let t1 : SemCond b s1 @$\times$@ SemComm cmThen s1 s2 - t1 = (proj@$\text{2}$@ (RelOpState.deltaRestPre + t1 = (proj@$\_{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) + t2 = (proj@$\_{2}$@ (respAnd bPre b s1)) + (q1 , proj@$\_{1}$@ t1) + in hypThen s1 s2 t2 (proj@$\_{2}$@ t1) rElse : RelOpState.comp (RelOpState.delta (NotP (SemCond b))) (SemComm cmElse) s1 s2 @$\rightarrow$@ @@ -57,25 +57,25 @@ rElse = @$\lambda$@ h @$\rightarrow$@ let t10 : (NotP (SemCond b) s1) @$\times$@ (SemComm cmElse s1 s2) - t10 = proj@$\text{2}$@ (RelOpState.deltaRestPre + t10 = proj@$\_{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) + t6 = proj@$\_{2}$@ (respNeg b s1) (proj@$\_{1}$@ t10) t7 : SemComm cmElse s1 s2 - t7 = proj@$\text{2}$@ t10 + t7 = proj@$\_{2}$@ t10 t8 : SemCond (bPre /\ neg b) s1 - t8 = proj@$\text{2}$@ (respAnd bPre (neg b) s1) + t8 = proj@$\_{2}$@ (respAnd bPre (neg b) s1) (q1 , t6) in hypElse s1 s2 t8 t7 in when rThen rElse q2 Soundness (WhileRule {cm'} {bInv} {b} pr) s1 s2 q1 q2 - = proj@$\text{2}$@ (respAnd bInv (neg b) s2) t20 + = proj@$\_{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 + n = proj@$\_{1}$@ q2 Rel1 : $mathbb{N}$ @$\rightarrow$@ Rel State (Level.zero) Rel1 = @$\lambda$@ m @$\rightarrow$@ RelOpState.repeat @@ -85,34 +85,34 @@ t1 : RelOpState.comp (Rel1 n) (RelOpState.delta (NotP (SemCond b))) s1 s2 - t1 = proj@$\text{2}$@ q2 + t1 = proj@$\_{2}$@ q2 t15 : (Rel1 n s1 s2) @$\times$@ (NotP (SemCond b) s2) - t15 = proj@$\text{2}$@ (RelOpState.deltaRestPost + t15 = proj@$\_{2}$@ (RelOpState.deltaRestPost (NotP (SemCond b)) (Rel1 n) s1 s2) t1 t16 : Rel1 n s1 s2 - t16 = proj@$\text{1}$@ t15 + t16 = proj@$\_{1}$@ t15 t17 : NotP (SemCond b) s2 - t17 = proj@$\text{2}$@ t15 + t17 = proj@$\_{2}$@ t15 lem1 : (m : $mathbb{N}$) @$\rightarrow$@ (ss2 : State) @$\rightarrow$@ Rel1 m s1 ss2 @$\rightarrow$@ SemCond bInv ss2 lem1 $mathbb{N}$.zero ss2 h - = substId1 State (proj@$\text{2}$@ h) (SemCond bInv) q1 + = substId1 State (proj@$\_{2}$@ h) (SemCond bInv) q1 lem1 ($mathbb{N}$.suc n) ss2 h = let hyp2 : (z : State) @$\rightarrow$@ Rel1 n s1 z @$\rightarrow$@ SemCond bInv z hyp2 = lem1 n s20 : State - s20 = proj@$\text{1}$@ h + s20 = proj@$\_{1}$@ h t21 : Rel1 n s1 s20 - t21 = proj@$\text{1}$@ (proj@$\text{2}$@ h) + t21 = proj@$\_{1}$@ (proj@$\_{2}$@ h) t22 : (SemCond b s20) @$\times$@ (SemComm cm' s20 ss2) - t22 = proj@$\text{2}$@ (RelOpState.deltaRestPre + t22 = proj@$\_{2}$@ (RelOpState.deltaRestPre (SemCond b) (SemComm cm') s20 ss2) - (proj@$\text{2}$@ (proj@$\text{2}$@ h)) + (proj@$\_{2}$@ (proj@$\_{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) + t23 = proj@$\_{2}$@ (respAnd bInv b s20) + (hyp2 s20 t21 , proj@$\_{1}$@ t22) + in hyp s20 ss2 t23 (proj@$\_{2}$@ t22) t20 : SemCond bInv s2 @$\times$@ SemCond (neg b) s2 - t20 = lem1 n s2 t16 , proj@$\text{2}$@ (respNeg b s2) t17 + t20 = lem1 n s2 t16 , proj@$\_{2}$@ (respNeg b s2) t17
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/agda-hoare-write.agda.replaced Mon Feb 03 21:47:43 2020 +0900 @@ -0,0 +1,11 @@ +-- 通常の CodeGear +whileLoop' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoop' zero env refl _ exit = exit env +whileLoop' (suc n) env refl next _ = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) + +-- Hoare Logic ベースの CodeGear +whileLoopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ (pre : varn env + vari env @$\equiv$@ c10 env) + @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ (pred n @$\equiv$@ varn env) @$\rightarrow$@ (post : varn env + vari env @$\equiv$@ c10 env) @$\rightarrow$@ t) + @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ (fin : vari env @$\equiv$@ c10 env) @$\rightarrow$@ t) @$\rightarrow$@ t +whileLoopPwP' zero env refl refl next exit = exit env refl +whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))
--- a/paper/src/redBlackTreeTest.agda.replaced Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/src/redBlackTreeTest.agda.replaced Mon Feb 03 21:47:43 2020 +0900 @@ -171,13 +171,13 @@ ... | 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 @$\rightarrow$@ - GetRedBlackTree.checkNode t k (@$\lambda$@ t@$\text{1}$@ x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) (root t)) + GetRedBlackTree.checkNode t k (@$\lambda$@ t@$\_{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 @$\rightarrow$@ compare2 x@$\text{1}$@ y } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x @$\equiv$@ True) + } ) ; nodeStack = s ; compare = @$\lambda$@ x@$\_{1}$@ y @$\rightarrow$@ compare2 x@$\_{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 @$\rightarrow$@ compare2 x@$\text{1}$@ y } ) k + } ) ; nodeStack = record { top = Nothing } ; compare = @$\lambda$@ x@$\_{1}$@ y @$\rightarrow$@ compare2 x@$\_{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
--- a/paper/src/stack-subtype-sample.agda.replaced Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/src/stack-subtype-sample.agda.replaced Mon Feb 03 21:47:43 2020 +0900 @@ -140,7 +140,7 @@ exec-comp (M.cs x) (M.cs _) m = refl -push-pop-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Element @$\mathbb{N}$@ @$\rightarrow$@ Set@$\text{1}$@ +push-pop-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Element @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@ push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta @$\equiv$@ meta where meta = id-meta n e record {top = just (cons x (just s))} @@ -150,7 +150,7 @@ -pop-n-push-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\text{1}$@ +pop-n-push-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@ pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta @$\equiv$@ M.exec (n-push {meta} n) meta where @@ -183,7 +183,7 @@ -n-push-pop-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\text{1}$@ +n-push-pop-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@ n-push-pop-type n cn ce st = M.exec (M.csComp {meta} (n-pop {meta} n) (n-push {meta} n)) meta @$\equiv$@ meta where meta = id-meta cn ce st
--- a/paper/src/stack-subtype.agda.replaced Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/src/stack-subtype.agda.replaced Mon Feb 03 21:47:43 2020 +0900 @@ -40,7 +40,7 @@ ContextIsDataSegment = record {get = (\c @$\rightarrow$@ c) ; set = (\_ c @$\rightarrow$@ c)} -record Meta : Set@$\text{1}$@ where +record Meta : Set@$\_{1}$@ where field -- context as set of data segments context : Context
--- a/paper/tree.tex Wed Jan 29 22:36:17 2020 +0900 +++ b/paper/tree.tex Mon Feb 03 21:47:43 2020 +0900 @@ -1,4 +1,5 @@ \chapter{BinaryTree} +\label{chapter:btree} CbC-Agda 上での Binary Tree \section{BinaryTree}
--- a/ryokka-master.mm Wed Jan 29 22:36:17 2020 +0900 +++ b/ryokka-master.mm Mon Feb 03 21:47:43 2020 +0900 @@ -44,7 +44,7 @@ <node CREATED="1577179370109" ID="ID_809388614" MODIFIED="1579169646927" TEXT="whileTest (Hoare Logic の例)"> <font NAME="SansSerif" SIZE="14"/> </node> -<node CREATED="1577179360283" ID="ID_501247037" MODIFIED="1579169646927" TEXT="Agda と Hoare Logic"> +<node CREATED="1577179360283" FOLDED="true" ID="ID_501247037" MODIFIED="1580733240320" TEXT="Agda と Hoare Logic"> <font NAME="SansSerif" SIZE="14"/> <node CREATED="1577179441565" ID="ID_1388092541" MODIFIED="1579169646927" TEXT="記述"> <font NAME="SansSerif" SIZE="14"/> @@ -54,22 +54,20 @@ </node> </node> </node> -<node CREATED="1577179318540" ID="ID_402362033" MODIFIED="1579169646926" POSITION="right" TEXT="Continuation based C と HoareLogic"> -<font NAME="SansSerif" SIZE="14"/> -<node CREATED="1577182741707" ID="ID_1751180005" MODIFIED="1579169646926" TEXT="HoareLogic"> -<font NAME="SansSerif" SIZE="14"/> +<node CREATED="1580733258780" ID="ID_309485478" MODIFIED="1580733267818" POSITION="right" TEXT="Continuation based C と Agda"> +<node CREATED="1580733268446" ID="ID_1382286556" MODIFIED="1580733276190" TEXT="Agda と CbC の対応"/> +<node CREATED="1580733278420" ID="ID_1658404824" MODIFIED="1580733301471" TEXT="CbC のメタ計算と Agda"> +<node CREATED="1580733301709" ID="ID_914616090" MODIFIED="1580733331759" TEXT="Agda は CbC の上位言語の一つとして使われそう..."/> </node> </node> -<node CREATED="1577182694546" ID="ID_764943519" MODIFIED="1579169646926" POSITION="right" TEXT="BinaryTree と RedBlack Tree(Agda)"> +<node CREATED="1577179318540" ID="ID_402362033" MODIFIED="1579169646926" POSITION="right" TEXT="Continuation based C と HoareLogic"> <font NAME="SansSerif" SIZE="14"/> -<node CREATED="1577182754406" ID="ID_1200857877" MODIFIED="1579169646926" TEXT="HoareLogic"> -<font NAME="SansSerif" SIZE="14"/> +<node CREATED="1580733080230" ID="ID_1644923722" MODIFIED="1580733118392" TEXT="Hoare Logic と CbC の対応"> +<node CREATED="1580733118792" ID="ID_415990499" MODIFIED="1580733144465" TEXT="Command たち(というか HTProof の概形？)"/> </node> -<node CREATED="1577182712718" ID="ID_283296995" MODIFIED="1579169646926" TEXT="BinaryTree の 条件つきのやつの話"> +<node CREATED="1577182741707" ID="ID_1751180005" MODIFIED="1580733188604" TEXT="Hoare Logic ベースの検証"> <font NAME="SansSerif" SIZE="14"/> -</node> -<node CREATED="1577182765996" ID="ID_740598781" MODIFIED="1579169646926" TEXT="RedBlackTree"> -<font NAME="SansSerif" SIZE="14"/> +<node CREATED="1580733190923" ID="ID_1861833651" MODIFIED="1580733195484" TEXT="while Test の例"/> </node> </node> <node CREATED="1577179295267" ID="ID_747054126" MODIFIED="1579169646925" POSITION="right" TEXT="まとめ"> @@ -87,5 +85,66 @@ <node CREATED="1577179492520" ID="ID_1327764636" MODIFIED="1579169646912" POSITION="left" TEXT="できたらいいな(Binary-Tree)"> <font NAME="SansSerif" SIZE="14"/> </node> +<node CREATED="1577182694546" ID="ID_764943519" MODIFIED="1579169646926" POSITION="left" TEXT="BinaryTree と RedBlack Tree(Agda)"> +<font NAME="SansSerif" SIZE="14"/> +<node CREATED="1577182754406" ID="ID_1200857877" MODIFIED="1579169646926" TEXT="HoareLogic"> +<font NAME="SansSerif" SIZE="14"/> +</node> +<node CREATED="1577182712718" ID="ID_283296995" MODIFIED="1579169646926" TEXT="BinaryTree の 条件つきのやつの話"> +<font NAME="SansSerif" SIZE="14"/> +</node> +<node CREATED="1577182765996" ID="ID_740598781" MODIFIED="1579169646926" TEXT="RedBlackTree"> +<font NAME="SansSerif" SIZE="14"/> +</node> +</node> +<node CREATED="1580721326343" ID="ID_1512980116" MODIFIED="1580721341151" POSITION="left" TEXT="Agda と CbC の対応について"> +<node CREATED="1580721373542" ID="ID_1954543280" MODIFIED="1580721383972" TEXT="CbC"> +<node CREATED="1580721384201" ID="ID_115992653" MODIFIED="1580733814782" TEXT="当研究室で開発してる"> +<icon BUILTIN="full-1"/> +</node> +<node CREATED="1580721396170" ID="ID_499703619" MODIFIED="1580733823040" TEXT="Cの下位言語"> +<icon BUILTIN="full-2"/> +</node> +<node CREATED="1580721408290" ID="ID_998450693" MODIFIED="1580733826688" TEXT="継続をベースとした言語"> +<icon BUILTIN="full-3"/> +</node> +<node CREATED="1580733361534" ID="ID_533829353" MODIFIED="1580733828942" TEXT="メタレベルの計算を分離している"> +<icon BUILTIN="full-4"/> +</node> +</node> +<node CREATED="1580721461991" ID="ID_591117015" MODIFIED="1580721463942" TEXT="Agda"> +<node CREATED="1580733533448" ID="ID_769096207" MODIFIED="1580733929041" TEXT="今書いてるやつ"> +<node CREATED="1580721464218" ID="ID_21769693" MODIFIED="1580733816784" TEXT="定理証明支援系言語"> +<icon BUILTIN="full-1"/> +</node> +<node CREATED="1580721533881" ID="ID_1399874964" MODIFIED="1580733831368" TEXT="CbC の上位言語"> +<icon BUILTIN="full-2"/> +</node> +<node CREATED="1580721541271" ID="ID_947618755" MODIFIED="1580733833446" TEXT="CPS で末尾再帰の形にすると CbC と対応"> +<icon BUILTIN="full-3"/> +</node> +<node CREATED="1580733406249" ID="ID_366137551" MODIFIED="1580733836038" TEXT="CbC から見ると ノーマルとメタレベルが一緒"> +<icon BUILTIN="full-4"/> +<node CREATED="1580733453908" ID="ID_798759509" MODIFIED="1580733676720" TEXT="(検証以外のメタ計算が行えない)"/> +</node> +</node> +<node CREATED="1580733547354" ID="ID_1244670000" MODIFIED="1580733554106" TEXT="あっとんさんが書いたやつ"> +<node CREATED="1580733555545" ID="ID_1619441901" MODIFIED="1580733819409" TEXT="Agda 上での CbC 言語実装みたいなの"> +<icon BUILTIN="full-1"/> +</node> +<node CREATED="1580733573052" ID="ID_1738251390" MODIFIED="1580733838805" TEXT="CbC の記述と等価(のはず)"> +<icon BUILTIN="full-2"/> +</node> +<node CREATED="1580733594205" ID="ID_1706512006" MODIFIED="1580733842123" TEXT="goto だったり metagoto みたいなの使って書く"> +<icon BUILTIN="full-3"/> +</node> +<node CREATED="1580733640095" ID="ID_464738583" MODIFIED="1580733844698" TEXT="上と同様に同一視できる"> +<icon BUILTIN="full-4"/> +<node CREATED="1580733704500" ID="ID_1089033110" MODIFIED="1580733756379" TEXT="Agda 上の CbC 実装なので一応他の計算も実装すれば行ける…？"/> +<node CREATED="1580733757793" ID="ID_352478839" MODIFIED="1580733785660" TEXT="ただし現時点で Hoare Logic ベースで証明できるかがわからない"/> +</node> +</node> +</node> +</node> </node> </map>