Mercurial > hg > Members > ryokka > HoareLogic

annotate whileTestPrim.agda @ 61:62dcb0ae2c94

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add Soundness Proof
author ryokka
date Sat, 21 Dec 2019 19:37:41 +0900
parents e668962ac31a
children 07b183a726f6
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module whileTestPrim where
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Function
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Nat
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.Bool hiding ( _≟_ )
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Level renaming ( suc to succ ; zero to Zero )
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Relation.Nullary using (¬_; Dec; yes; no)
4
64bd5c236002 add whileTestGears
ryokka
parents: 3
diff changeset
8 open import Relation.Binary.PropositionalEquality
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
21
5e4abc1919b4 fix module relation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
10 open import utilities hiding ( _/\_ )
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 record Env : Set where
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 field
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 varn : ℕ
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 vari : ℕ
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 open Env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 PrimComm : Set
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 PrimComm = Env → Env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 Cond : Set
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 Cond = (Env → Bool)
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
22
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
24 Axiom : Cond -> PrimComm -> Cond -> Set
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
25 Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
26
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
27 Tautology : Cond -> Cond -> Set
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
28 Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
29
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
30 _and_ : Cond -> Cond -> Cond
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
31 x and y = λ env → x env ∧ y env
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
32
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
33 neg : Cond -> Cond
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
34 neg x = λ env → not ( x env )
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
35
24
e668962ac31a rename modules
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
36 open import Hoare PrimComm Cond Axiom Tautology _and_ neg
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37
8
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
38 ---------------------------
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
39
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
40 program : ℕ → Comm
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
41 program c10 =
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
42 Seq ( PComm (λ env → record env {varn = c10}))
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 $ Seq ( PComm (λ env → record env {vari = 0}))
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
44 $ While (λ env → lt zero (varn env ) )
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
48 simple : ℕ → Comm
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
49 simple c10 =
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
50 Seq ( PComm (λ env → record env {varn = c10}))
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 $ PComm (λ env → record env {vari = 0})
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 {-# TERMINATING #-}
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 interpret : Env → Comm → Env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 interpret env Skip = env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 interpret env Abort = env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 interpret env (PComm x) = x env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 interpret env (If x then else) with x env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 ... | true = interpret env then
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 ... | false = interpret env else
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 interpret env (While x comm) with x env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 ... | true = interpret (interpret env comm) (While x comm)
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 ... | false = env
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 test1 : Env
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
67 test1 = interpret ( record { vari = 0 ; varn = 0 } ) (program 10)
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68
8
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
69 eval-proof : vari test1 ≡ 10
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
70 eval-proof = refl
e4f087b823d4 add proofs
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 7
diff changeset
71
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
72 tests : Env
14
a622d1700a1b make 10 variable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
73 tests = interpret ( record { vari = 0 ; varn = 0 } ) (simple 10)
7
e7d6bdb6039d fix test1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
74