# HG changeset patch
# User ryokka
# Date 1580734063 -32400
# Node ID 196ba119ca8932c0c4c52bdaf5782d6b21735512
# Parent b5fffa8ae875d0da5232ecb6b709d2d79ea182a0
fix, and add mindmap->pdf
diff -r b5fffa8ae875 -r 196ba119ca89 paper/abstract.tex
--- 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)が存在している。
diff -r b5fffa8ae875 -r 196ba119ca89 paper/agda.tex
--- 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 同型対応により命題と型付きラムダ計算が一対一で対応ため
diff -r b5fffa8ae875 -r 196ba119ca89 paper/cbc.tex
--- 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} による実装が存在する。
diff -r b5fffa8ae875 -r 196ba119ca89 paper/cbc_agda.tex
--- 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 の表現を示す。
diff -r b5fffa8ae875 -r 196ba119ca89 paper/conclusion.tex
--- 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{今後の課題}
diff -r b5fffa8ae875 -r 196ba119ca89 paper/hoare.tex
--- 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 を記述しており、
diff -r b5fffa8ae875 -r 196ba119ca89 paper/introduction.tex
--- 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} などの低レベル記述向けの関数型言語を実装に用いる手法が存在している。
diff -r b5fffa8ae875 -r 196ba119ca89 paper/master_paper.pdf
Binary file paper/master_paper.pdf has changed
diff -r b5fffa8ae875 -r 196ba119ca89 paper/master_paper.tex
--- 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{*}
diff -r b5fffa8ae875 -r 196ba119ca89 paper/src/AgdaNPushNPop.agda.replaced
--- 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
diff -r b5fffa8ae875 -r 196ba119ca89 paper/src/AgdaNPushNPopProof.agda.replaced
--- 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
diff -r b5fffa8ae875 -r 196ba119ca89 paper/src/AgdaPushPopProof.agda.replaced
--- 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))}
diff -r b5fffa8ae875 -r 196ba119ca89 paper/src/AgdaStackDS.agda.replaced
--- 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
diff -r b5fffa8ae875 -r 196ba119ca89 paper/src/AgdaTreeProof.agda.replaced
--- 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
diff -r b5fffa8ae875 -r 196ba119ca89 paper/src/PushPopType.agda.replaced
--- 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
diff -r b5fffa8ae875 -r 196ba119ca89 paper/src/agda-hoare-soundness.agda.replaced
--- 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
diff -r b5fffa8ae875 -r 196ba119ca89 paper/src/agda-hoare-write.agda.replaced
--- /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))
diff -r b5fffa8ae875 -r 196ba119ca89 paper/src/redBlackTreeTest.agda.replaced
--- 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
diff -r b5fffa8ae875 -r 196ba119ca89 paper/src/stack-subtype-sample.agda.replaced
--- 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
diff -r b5fffa8ae875 -r 196ba119ca89 paper/src/stack-subtype.agda.replaced
--- 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
diff -r b5fffa8ae875 -r 196ba119ca89 paper/tree.tex
--- 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}
diff -r b5fffa8ae875 -r 196ba119ca89 ryokka-master.mm
--- 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 @@
-
+
@@ -54,22 +54,20 @@
-
-
-
-
+
+
+
+
-
+
-
-
+
+
-
+
-
-
-
+
@@ -87,5 +85,66 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff -r b5fffa8ae875 -r 196ba119ca89 ryokka-mm.pdf
Binary file ryokka-mm.pdf has changed