-
Notifications
You must be signed in to change notification settings - Fork 1
/
basics.v
77 lines (46 loc) · 1.63 KB
/
basics.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
(* -*- coding:utf-8 -*- *)
Require Import Unicode.Utf8.
Module basics.
(* programs, designs, specifications *)
Variable D : Set.
(* refinement relationship *)
Variable R : D -> D -> Prop.
Notation "A 'ref' B" := (R A B) (at level 20).
Notation "A ⊑ B" := (R A B) (at level 20).
Axiom Transitivity : forall x y z : D, R x y /\ R y z -> R x z.
Axiom Reflexivity : forall x : D, x ref x.
Axiom AntiSymmetry : forall x y : D, R x y -> R y x -> x = y.
Hint Resolve Transitivity Reflexivity AntiSymmetry.
(* sequential composition *)
Variable SeqComp : D -> D -> D.
Notation "A ; B" := (SeqComp A B) (at level 15).
Axiom Monotonicity :
forall p q p' q' : D,
p ref p' -> q ref q' ->
(p; q) ref (p'; q').
Hint Resolve Monotonicity.
(* parallel composition *)
Variable ParComp : D -> D -> D.
Notation "A | B" := (ParComp A B) (at level 16).
Axiom ParCommutativity :
forall p q : D,
p | q = q | p.
Axiom ParMonotonicity :
forall p q p' q' : D,
p ref p' -> q ref q' ->
(p | q) ref (p' | q').
Hint Resolve ParCommutativity ParMonotonicity.
(* triples *)
Definition HoareTriple (p q r : D) := R (SeqComp p q) r.
Notation "[ A ] B [ C ]" := (HoareTriple A B C) (at level 20).
(* square brackets because of syntactic limitations *)
Definition PlotkinReduction (p q r : D) := r ref p; q.
Definition MilnerTransition (p q r : D) := q; r ref p.
Definition TestGeneration (p q r : D) := p ref q; r.
(* no sugar for these triples because it's ugly anyway *)
Hint Unfold HoareTriple PlotkinReduction MilnerTransition TestGeneration.
Definition AssociativityLaw :=
forall p q r : D,
(p; q); r = p; (q; r).
End basics.
Export basics.