Mercurial > hg > Members > ryokka > HoareLogic

changeset 48:cc8de8bdbf7e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 16 Dec 2019 16:22:52 +0900
parents b07e96029ae3
children 91d6d8097a39
files whileTestGears.agda
diffstat 1 files changed, 7 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Mon Dec 16 15:45:39 2019 +0900
+++ b/whileTestGears.agda	Mon Dec 16 16:22:52 2019 +0900
@@ -140,8 +140,11 @@
     lemma : cx env ≡ pstate1 {!!}
     lemma = {!!}
 
-loopPwithProof : {l : Level} {t : Set l} → (e : EnvP ) →  cx e ≡ pstate2 {!!} → (exit : EnvP →  cx e ≡ pstate2 {!!} → t) → t
-loopPwithProof env exit = whileLoopP env (λ env → loopPwithProof env {!!} {!!} ) {!!}
+{-# TERMINATING #-}
+loopPwithProof : {l : Level} {t : Set l} → (e : EnvP ) → (exit : (e : EnvP ) →  cx e ≡ pstate2 {!!} → t) →  cx e ≡ pstate2 {!!} → t
+loopPwithProof env exit eq = whileLoopP env (λ env → loopPwithProof env exit {!!} ) (λ env → exit env {!!} ) where
+    lemma :  cx {!!} ≡ pstate2 {!!}
+    lemma = {!!}
 
 ConvP : (e : EnvP) → cx e ≡ pstate1 {!!} →  cx e ≡ pstate2 {!!}
 ConvP = {!!}
@@ -151,10 +154,9 @@
 
 whileTestPProof : {c :  ℕ } → Set
 whileTestPProof {c} = whileTestPwithProof  c
-    $ λ env eq → loopPwithProof env (ConvP env eq)
-    $ λ env eq → pvari env ≡ c10 env
+    $ λ env eq → loopPwithProof env (λ env eq → {!!} ) (ConvP env eq )
 
 whileTestPProofMeta : {c10 :  ℕ } →  whileTestPProof {c10}
-whileTestPProofMeta {c10} = ?
+whileTestPProofMeta {c10} = {!!}