Mercurial > hg > Members > ryokka > HoareLogic

changeset 7:e7d6bdb6039d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix test1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 14 Dec 2018 22:35:38 +0900
parents 28e80739eed6
children e4f087b823d4
files whileTestGears.agda whileTestPrim.agda
diffstat 2 files changed, 11 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Fri Dec 14 22:06:24 2018 +0900
+++ b/whileTestGears.agda	Fri Dec 14 22:35:38 2018 +0900
@@ -111,14 +111,7 @@
     where
       env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
       proof3 : varn env1 + vari env1 ≡ 10
-      proof3 = let open ≡-Reasoning  in
-          begin 
-            varn env1 + vari env1
-          ≡⟨⟩
-            (varn env - 1) + (vari env + 1)
-          ≡⟨ {!!} ⟩
-            10
-          ∎
+      proof3 = {!!}
 
 
 conversion1 : {l : Level} {t : Set l } → (env : Env) -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10)
--- a/whileTestPrim.agda	Fri Dec 14 22:06:24 2018 +0900
+++ b/whileTestPrim.agda	Fri Dec 14 22:35:38 2018 +0900
@@ -34,7 +34,7 @@
 (suc x) - (suc y)  = x - y
 
 lt : ℕ -> ℕ -> Bool
-lt x y with (suc x ) ≤? y
+lt x y with suc x  ≤? y
 lt x y | yes p = true
 lt x y | no ¬p = false
 
@@ -47,7 +47,7 @@
 program = 
     Seq ( PComm (λ env → record env {varn = 10}))
     $ Seq ( PComm (λ env → record env {vari = 0}))
-    $ While (λ env → lt (varn env ) zero )
+    $ While (λ env → lt zero (varn env ) )
       (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
         $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
 
@@ -72,6 +72,9 @@
 test1 : Env
 test1 =  interpret ( record { vari = 0  ; varn = 0 } ) program
 
+tests : Env
+tests =  interpret ( record { vari = 0  ; varn = 0 } ) simple
+
 
 empty-case : (env : Env) → (( λ e → true ) env ) ≡ true 
 empty-case _ = refl
@@ -161,8 +164,8 @@
     $ SeqRule {λ e →  Equal (varn e) 10} ( PrimRule lemma1   )
     $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)}  lemma2 (
             WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
-            $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt (varn e) zero } lemma3)
-                     $ PrimRule {whileInv'} {_} {whileInv}  lemma4  ) lemma5
+            $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
+                     $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
   where
      lemma1 : Axiom stmt1Cond (λ env → record { varn = varn env ; vari = 0 }) stmt2Cond
      lemma1 env with stmt1Cond env
@@ -174,11 +177,11 @@
      lemma2 env | false | true = refl
      lemma2 env | true | true = refl
      lemma2 env | true | false = {!!}
-     lemma3 : Axiom (whileInv /\ (λ env → lt (varn env) zero)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
+     lemma3 :   Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
      lemma3 = {!!}
-     lemma4 :  Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
+     lemma4 :   Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv 
      lemma4 = {!!}
-     lemma5 :  Tautology (whileInv /\ neg (λ z → lt (varn z) zero)) termCond
+     lemma5 :   Tautology ((λ e → Equal (varn e + vari e) 10) /\ neg (λ z → lt zero (varn z))) termCond
      lemma5 = {!!}