Mercurial > hg > Members > ryokka > HoareLogic

changeset 22:e88ad1d70faf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate Hoare with whileTestPrim
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 25 Dec 2018 08:24:54 +0900
parents 5e4abc1919b4
children 3968822b9693
files Hoare.agda HoareData.agda whileTestPrim.agda
diffstat 3 files changed, 141 insertions(+), 78 deletions(-) [+]
line wrap: on
line diff
--- 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
--- /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)
+
--- 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