Mercurial > hg > Members > ryokka > HoareLogic

changeset 44:5a3c9d087c7c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 15 Dec 2019 15:57:07 +0900
parents 8813f26da3b7
children de8449321356
files whileTestGears.agda
diffstat 1 files changed, 28 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Sun Dec 15 12:29:13 2019 +0900
+++ b/whileTestGears.agda	Sun Dec 15 15:57:07 2019 +0900
@@ -10,35 +10,35 @@
 open import utilities
 open  _/\_
 
-record Env : Set (succ Zero) where
+record Env (Cxt : Set) : Set (succ Zero) where
   field
     varn : ℕ
     vari : ℕ
-    cx : Set
-open Env 
+    cx : Cxt
+open Env  
 
-whileTest : {l : Level} {t : Set l} (c : Set ) → (c10 : ℕ) → (Code : Env → t) → t
-whileTest c c10 next = next (record {varn = c10 ; vari = 0 ; cx = c} )
+whileTest : {l : Level} {t : Set l} {Cxt : Set} (c : Cxt ) → (c10 : ℕ) → (Code : Env Cxt → t) → t
+whileTest c c10 next = next (record {varn = c10 ; vari = 0 ; cx = c } )
 
 {-# TERMINATING #-}
-whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
+whileLoop : {l : Level} {t : Set l} {Cxt : Set} {c : Cxt } → Env Cxt → (Code : Env Cxt → t) → t
 whileLoop env next with lt 0 (varn env)
 whileLoop env next | false = next env
 whileLoop env next | true =
     whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
 
-test1 : (c : Set ) → Env 
+test1 : {Cxt : Set }  → (c : Cxt) → Env Cxt 
 test1 c = whileTest c 10 (λ env → whileLoop env (λ env1 → env1 ))
 
 
-proof1 : (c : Set ) → whileTest c 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
+proof1 : {Cxt : Set } (c : Cxt ) → whileTest c 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
 proof1 c = refl
 
 --                                                                              ↓PostCondition
-whileTest' : {l : Level} {t : Set l}  →  {c : Set} → {c10 :  ℕ } → (Code : (env : Env )  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
-whileTest' {_} {_} {c} {c10} next = next env proof2
+whileTest' : {l : Level} {t : Set l} {Cxt : Set}  →  {c : Cxt} → {c10 :  ℕ } → (Code : (env : Env Cxt )  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
+whileTest' {_} {_} {Cxt} {c} {c10} next = next env proof2
   where
-    env : Env 
+    env : Env Cxt 
     env = record {vari = 0 ; varn = c10 ; cx = c }
     proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
     proof2 = record {pi1 = refl ; pi2 = refl}
@@ -48,7 +48,7 @@
 
 
 {-# TERMINATING #-} --                                                  ↓PreCondition(Invaliant)
-whileLoop' : {l : Level} {t : Set l} → (env : Env ) → {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env  → t) → t
+whileLoop' : {l : Level} {t : Set l} {Cxt : Set} {c : Cxt } → (env : Env Cxt ) → {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env Cxt  → t) → t
 whileLoop' env proof next with  ( suc zero  ≤? (varn  env) )
 whileLoop' env proof next | no p = next env 
 whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next
@@ -76,8 +76,8 @@
       --     ∎
 
 -- Condition to Invaliant
-conversion1 : {l : Level} {t : Set l } → (env : Env ) → {c10 :  ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
-               → (Code : (env1 : Env ) → (varn env1 + vari env1 ≡ c10) → t) → t
+conversion1 : {l : Level} {t : Set l } {Cxt : Set} {c : Cxt } → (env : Env Cxt ) → {c10 :  ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
+               → (Code : (env1 : Env Cxt ) → (varn env1 + vari env1 ≡ c10) → t) → t
 conversion1 env {c10} p1 next = next env proof4
    where
       proof4 : varn env + vari env ≡ c10
@@ -93,23 +93,25 @@
           ∎
 
 
-proofGears : {c10 :  ℕ } → Set → Set
-proofGears {c10} c = whileTest' {_} {_} {c} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
+proofGears : {c10 :  ℕ } → { Cxt : Set } → (c : Cxt ) → Set
+proofGears {c10} c = whileTest' {_} {_} {_} {c} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 
-data whileTestState (c10 : ℕ ) (env : Env ) : Set where
+record Context (e : Set ) : Set (succ Zero)
+
+data whileTestState {Cxt : Set } (c10 : ℕ ) (env : Env Cxt ) : Set  where
   error : whileTestState c10 env
   state1 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestState c10 env
   state2 : (varn env + vari env ≡ c10) → whileTestState c10 env
   finstate : ((vari env) ≡ c10 ) → whileTestState c10 env
 
 --
---      openended Env c  <=>  Context
+--      openended Env Cxt c  <=>  Context
 --
 
-record Context : Set (succ Zero) where
+record Context e where
    field 
      c10 : ℕ
-     whileDG : Env 
+     whileDG : Env e
      whileCond : whileTestState c10 whileDG
 
 open Context
@@ -121,7 +123,7 @@
 -- transparency of condition
 --
 
-whileCondP : Env → Set
+whileCondP : Env {!!} → Set
 whileCondP env = varn env > 0
 
 whileDec : (cxt : Context) → Dec (whileCondP (whileDG cxt))
@@ -141,7 +143,7 @@
         proof cxt = {!!} 
 
 {-# TERMINATING #-}
-whileLoopStep : {l : Level} {t : Set l} → Env → (next : (e : Env ) → t) (exit : (e : Env) → t) → t
+whileLoopStep : {l : Level} {t : Set l} → Env {!!} → (next : (e : Env {!!} ) → t) (exit : (e : Env {!!} ) → t) → t
 whileLoopStep env next exit with <-cmp 0 (varn env)
 whileLoopStep env next exit | tri≈ _ eq _ = exit env 
 whileLoopStep env next exit | tri< gt ¬eq _  = next record env {varn = (varn env) - 1 ; vari = (vari env) + 1} 
@@ -149,7 +151,7 @@
 
 whileTestProof : {l : Level} {t : Set l} → Context → (Code : (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) ) → t) → t
 whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } i!=n where
-    out : Env 
+    out : Env {!!} 
     out =  whileTest {!!} (c10 cxt) ( λ e → e ) 
     init : whileTestState (c10 cxt) out
     init = state1 record { pi1 = refl ; pi2 = refl }
@@ -162,9 +164,9 @@
 whileLoopProof cxt i!=n next exit = whileLoopStep (whileDG cxt)
     ( λ env → next record cxt { whileDG = env ; whileCond = {!!} } {!!} ) 
     ( λ env → exit record cxt { whileDG = env ; whileCond = exitCond env {!!} } {!!} )   where
-        proof5 : (e : Env ) → varn e + vari e ≡ c10 cxt →  0 ≡ varn e → vari e ≡ c10 cxt
+        proof5 : (e : Env {!!} ) → varn e + vari e ≡ c10 cxt →  0 ≡ varn e → vari e ≡ c10 cxt
         proof5 record { varn = .0 ; vari = vari } refl refl = refl
-        exitCond : (e : Env ) → 0 ≡ varn e → whileTestState (c10 cxt) e
+        exitCond : (e : Env {!!} ) → 0 ≡ varn e → whileTestState (c10 cxt) e
         exitCond nenv eq1 with whileCond cxt | inspect whileDG cxt
         ... | state2 cond | record { eq = eq2 } = finstate ( proof5 nenv {!!} eq1 )
         ... | _ | _ = error
@@ -172,7 +174,7 @@
 whileConvProof : {l : Level} {t : Set l} → (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt))
     → ((cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt)) → t) → t
 whileConvProof cxt i!=n next = next record cxt { whileCond = postCond } i!=n where
-    proof4 : (e : Env ) → (vari e ≡ 0) /\ (varn e ≡ c10 cxt)  → varn e + vari e ≡ c10 cxt
+    proof4 : (e : Env {!!} ) → (vari e ≡ 0) /\ (varn e ≡ c10 cxt)  → varn e + vari e ≡ c10 cxt
     proof4 env p1 = let open ≡-Reasoning  in
           begin
             varn env + vari env