# HG changeset patch # User Shinji KONO # Date 1545693894 -32400 # Node ID e88ad1d70faf9dded983b7936f31cdadcdd9de41 # Parent 5e4abc1919b40f3ca7d42a0c6716235c0e4f85c6 separate Hoare with whileTestPrim diff -r 5e4abc1919b4 -r e88ad1d70faf Hoare.agda --- a/Hoare.agda Mon Dec 24 22:50:25 2018 +0900 +++ b/Hoare.agda Tue Dec 25 08:24:54 2018 +0900 @@ -11,10 +11,42 @@ open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality open import RelOp -open import whileTestPrim +open import utilities -module Hoare where +module Hoare + (Cond : Set) + (PrimComm : Set) + (neg : Cond -> Cond) + (_/\_ : Cond -> Cond -> Cond) + (Tautology : Cond -> Cond -> Set) + (State : Set) + (SemCond : Cond -> State -> Set) + (tautValid : (b1 b2 : Cond) -> Tautology b1 b2 -> + (s : State) -> SemCond b1 s -> SemCond b2 s) + (respNeg : (b : Cond) -> (s : State) -> + Iff (SemCond (neg b) s) (¬ SemCond b s)) + (respAnd : (b1 b2 : Cond) -> (s : State) -> + Iff (SemCond (b1 /\ b2) s) + ((SemCond b1 s) × (SemCond b2 s))) + (PrimSemComm : ∀ {l} -> PrimComm -> Rel State l) + (Axiom : Cond -> PrimComm -> Cond -> Set) + (axiomValid : ∀ {l} -> (bPre : Cond) -> (pcm : PrimComm) -> (bPost : Cond) -> + (ax : Axiom bPre pcm bPost) -> (s1 s2 : State) -> + SemCond bPre s1 -> PrimSemComm {l} pcm s1 s2 -> SemCond bPost s2) where +open import HoareData PrimComm Cond Axiom Tautology _/\_ neg + +open import RelOp +module RelOpState = RelOp State + +NotP : {S : Set} -> Pred S -> Pred S +NotP X s = ¬ X s + +_\/_ : Cond -> Cond -> Cond +b1 \/ b2 = neg (neg b1 /\ neg b2) + +_==>_ : Cond -> Cond -> Cond +b1 ==> b2 = neg (b1 \/ b2) when : {X Y Z : Set} -> (X -> Z) -> (Y -> Z) -> X ⊎ Y -> Z diff -r 5e4abc1919b4 -r e88ad1d70faf HoareData.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/HoareData.agda Tue Dec 25 08:24:54 2018 +0900 @@ -0,0 +1,76 @@ +module HoareData + (PrimComm : Set) + (Cond : Set) + (Axiom : Cond -> PrimComm -> Cond -> Set) + (Tautology : Cond -> Cond -> Set) + (_and_ : Cond -> Cond -> Cond) + (neg : Cond -> Cond ) + where + +data Comm : Set where + Skip : Comm + Abort : Comm + PComm : PrimComm -> Comm + Seq : Comm -> Comm -> Comm + If : Cond -> Comm -> Comm -> Comm + While : Cond -> Comm -> Comm + + +{- + prPre pr prPost + ------------- ------------------ ---------------- + bPre => bPre' {bPre'} c {bPost'} bPost' => bPost +Weakening : ---------------------------------------------------- + {bPre} c {bPost} + +Assign: ---------------------------- + {bPost[v<-e]} v:=e {bPost} + + pr1 pr2 + ----------------- ------------------ + {bPre} cm1 {bMid} {bMid} cm2 {bPost} +Seq: --------------------------------------- + {bPre} cm1 ; cm2 {bPost} + + pr1 pr2 + ----------------------- --------------------------- + {bPre /\ c} cm1 {bPost} {bPre /\ neg c} cm2 {bPost} +If: ------------------------------------------------------ + {bPre} If c then cm1 else cm2 fi {bPost} + + pr + ------------------- + {inv /\ c} cm {inv} +While: --------------------------------------- + {inv} while c do cm od {inv /\ neg c} +-} + + +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 and b) cmThen bPost -> + HTProof (bPre and neg b) cmElse bPost -> + HTProof bPre (If b cmThen cmElse) bPost + WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> + HTProof (bInv and b) cm bInv -> + HTProof bInv (While b cm) (bInv and neg b) + diff -r 5e4abc1919b4 -r e88ad1d70faf whileTestPrim.agda --- a/whileTestPrim.agda Mon Dec 24 22:50:25 2018 +0900 +++ b/whileTestPrim.agda Tue Dec 25 08:24:54 2018 +0900 @@ -21,13 +21,19 @@ Cond : Set Cond = (Env → Bool) -data Comm : Set where - Skip : Comm - Abort : Comm - PComm : PrimComm -> Comm - Seq : Comm -> Comm -> Comm - If : Cond -> Comm -> Comm -> Comm - While : Cond -> Comm -> Comm +Axiom : Cond -> PrimComm -> Cond -> Set +Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true + +Tautology : Cond -> Cond -> Set +Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true + +_and_ : Cond -> Cond -> Cond +x and y = λ env → x env ∧ y env + +neg : Cond -> Cond +neg x = λ env → not ( x env ) + +open import HoareData PrimComm Cond Axiom Tautology _and_ neg --------------------------- @@ -71,75 +77,6 @@ empty-case _ = refl -Axiom : Cond -> PrimComm -> Cond -> Set -Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true - -Tautology : Cond -> Cond -> Set -Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true - -_and_ : Cond -> Cond -> Cond -x and y = λ env → x env ∧ y env - -neg : Cond -> Cond -neg x = λ env → not ( x env ) - -{- - prPre pr prPost - ------------- ------------------ ---------------- - bPre => bPre' {bPre'} c {bPost'} bPost' => bPost -Weakening : ---------------------------------------------------- - {bPre} c {bPost} - -Assign: ---------------------------- - {bPost[v<-e]} v:=e {bPost} - - pr1 pr2 - ----------------- ------------------ - {bPre} cm1 {bMid} {bMid} cm2 {bPost} -Seq: --------------------------------------- - {bPre} cm1 ; cm2 {bPost} - - pr1 pr2 - ----------------------- --------------------------- - {bPre /\ c} cm1 {bPost} {bPre /\ neg c} cm2 {bPost} -If: ------------------------------------------------------ - {bPre} If c then cm1 else cm2 fi {bPost} - - pr - ------------------- - {inv /\ c} cm {inv} -While: --------------------------------------- - {inv} while c do cm od {inv /\ neg c} --} - - -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 and b) cmThen bPost -> - HTProof (bPre and neg b) cmElse bPost -> - HTProof bPre (If b cmThen cmElse) bPost - WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} -> - HTProof (bInv and b) cm bInv -> - HTProof bInv (While b cm) (bInv and neg b) initCond : Cond initCond env = true @@ -374,3 +311,21 @@ axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | () axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl +open import Hoare + Cond + PrimComm + neg + _and_ + Tautology + State + SemCond + tautValid + respNeg + respAnd + PrimSemComm + Axiom + axiomValid + +PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} -> + HTProof bPre cm bPost -> Satisfies bPre cm bPost +PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht