Mercurial > hg > Papers > 2020 > soto-midterm

comparison src/whileTestPrim.agda.replaced @ 1:73127e0ab57c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(none)
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 08 Sep 2020 18:38:08 +0900
parents
children
comparison
equal deleted inserted replaced
0:b919985837a3 1:73127e0ab57c
1 module whileTestPrim where
2
3 open import Function
4 open import Data.Nat
5 open import Data.Bool hiding ( _@$\stackrel{?}{=}$@_ )
6 open import Level renaming ( suc to succ ; zero to Zero )
7 open import Relation.Nullary using (@$\neg$@_; Dec; yes; no)
8 open import Relation.Binary.PropositionalEquality
9
10 open import utilities hiding ( _@$\wedge$@_ )
11
12 record Env : Set where
13 field
14 varn : @$\mathbb{N}$@
15 vari : @$\mathbb{N}$@
16 open Env
17
18 PrimComm : Set
19 PrimComm = Env @$\rightarrow$@ Env
20
21 Cond : Set
22 Cond = (Env @$\rightarrow$@ Bool)
23
24 Axiom : Cond @$\rightarrow$@ PrimComm @$\rightarrow$@ Cond @$\rightarrow$@ Set
25 Axiom pre comm post = @$\forall$@ (env : Env) @$\rightarrow$@ (pre env) @$\Rightarrow$@ ( post (comm env)) @$\equiv$@ true
26
27 Tautology : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Set
28 Tautology pre post = @$\forall$@ (env : Env) @$\rightarrow$@ (pre env) @$\Rightarrow$@ (post env) @$\equiv$@ true
29
30 _and_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond
31 x and y = @$\lambda$@ env @$\rightarrow$@ x env @$\wedge$@ y env
32
33 neg : Cond @$\rightarrow$@ Cond
34 neg x = @$\lambda$@ env @$\rightarrow$@ not ( x env )
35
36 open import Hoare PrimComm Cond Axiom Tautology _and_ neg
37
38 ---------------------------
39
40 program : @$\mathbb{N}$@ @$\rightarrow$@ Comm
41 program c10 =
42 Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10}))
43 $ Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0}))
44 $ While (@$\lambda$@ env @$\rightarrow$@ lt zero (varn env ) )
45 (Seq (PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = ((vari env) + 1)} ))
46 $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = ((varn env) - 1)} ))
47
48 simple : @$\mathbb{N}$@ @$\rightarrow$@ Comm
49 simple c10 =
50 Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10}))
51 $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0})
52
53 {-@$\#$@ TERMINATING @$\#$@-}
54 interpret : Env @$\rightarrow$@ Comm @$\rightarrow$@ Env
55 interpret env Skip = env
56 interpret env Abort = env
57 interpret env (PComm x) = x env
58 interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
59 interpret env (If x then else) with x env
60 ... | true = interpret env then
61 ... | false = interpret env else
62 interpret env (While x comm) with x env
63 ... | true = interpret (interpret env comm) (While x comm)
64 ... | false = env
65
66 test1 : Env
67 test1 = interpret ( record { vari = 0 ; varn = 0 } ) (program 10)
68
69
70 tests : Env
71 tests = interpret ( record { vari = 0 ; varn = 0 } ) (simple 10)