Library Scat.Atoms
non-deterministic assignment
do nothing
ensure a postcondition post (e.g. a guard)
deterministic assignment
require with empty mesg
Inductive asem: atom → state → option state → Prop :=
| asem_guassign l post s0 s1:
lframeeq l s0 s1 → oeval post s0 s1 → asem (guassign l post) s0 (Some s1)
| asem_skip s:
asem skip s (Some s)
| asem_req_ok c m s:
eval c s
→ asem (xrequire c m) s (Some s)
| asem_req_ko c m s:
~(eval c s)
→ asem (xrequire c m) s None
| asem_ensure c s:
eval c s
→ asem (ensure c) s (Some s)
| asem_assign x t s:
asem (assign x t) s (Some (add (vid x) (teval t s) s)).
Hint Resolve Some asem_guassign asem_skip asem_req_ok asem_req_ko asem_ensure asem_assign: sem.
| asem_guassign l post s0 s1:
lframeeq l s0 s1 → oeval post s0 s1 → asem (guassign l post) s0 (Some s1)
| asem_skip s:
asem skip s (Some s)
| asem_req_ok c m s:
eval c s
→ asem (xrequire c m) s (Some s)
| asem_req_ko c m s:
~(eval c s)
→ asem (xrequire c m) s None
| asem_ensure c s:
eval c s
→ asem (ensure c) s (Some s)
| asem_assign x t s:
asem (assign x t) s (Some (add (vid x) (teval t s) s)).
Hint Resolve Some asem_guassign asem_skip asem_req_ok asem_req_ko asem_ensure asem_assign: sem.
Definition awlp (p: atom) (post: state→ Prop) (s:state) : Prop :=
match p with
| guassign l c ⇒ ∀ s', lframeeq l s s' → oeval c s s' → post s'
| skip ⇒ post s
| xrequire c m ⇒ eval c s ∧ post s
| ensure c ⇒ (eval c s) → (post s)
| assign x t ⇒ post (add (vid x) (teval t s) s)
end.
Lemma awlp_monotonic p:
∀ (P Q: state → Prop) s, awlp p P s →
(∀ s, P s → Q s) → awlp p Q s.
Proof.
destruct p; simpl; intuition simpl; eauto.
Qed.
Hint Resolve ok_monotonic awlp_monotonic: echecker.
Lemma awlp_correctness p s s': (asem p s s') → ∀ post, awlp p post s → ok s' post.
Proof.
destruct 1; simpl in × |- *; intuition eauto with echecker.
Qed.
Hint Resolve awlp_correctness: echecker.
Lemma awlp_complete p: ∀ post s, (∀ s', asem p s s' → ok s' post) → awlp p post s.
Proof.
destruct p; simpl in × |- *; intros; try (refine (H (Some _) _); eauto with sem).
case (classic (eval pre s)).
intuition refine (H (Some _) _); eauto with sem.
intros; case (H None). eauto with sem.
Qed.
Definition atom_eq (inst1 inst2: atom) :=
match inst1, inst2 with
| guassign l1 post1, guassign l2 post2 ⇒ lvar_eq l1 l2 &&& cond_eq post1 post2
| skip, skip ⇒ true
| xrequire pre1 _, xrequire pre2 _ ⇒ cond_eq pre1 pre2
| ensure post1, ensure post2 ⇒ cond_eq post1 post2
| assign x1 t1, assign x2 t2 ⇒ var_eq x1 x2 &&& term_eq t1 t2
| _, _ ⇒ false
end.
Lemma atom_eq_awlp (inst1 inst2: atom) post s: atom_eq inst1 inst2=true → awlp inst1 post s → awlp inst2 post s.
Proof.
decide_eqb_eq inst1 inst2; eqtrue.
intros H1 H2 s' H3 H4.
apply H2.
eapply lvar_eq_lframeeq; eauto.
erewrite cond_eq_oeval; eauto.
intuition.
erewrite <- cond_eq_eval; eauto.
intros H0 H1 H2; apply H1.
erewrite cond_eq_eval; eauto.
intros; erewrite <- var_eq_eq; eauto.
erewrite <- term_eq_eval; eauto.
Qed.
Hint Resolve atom_eq_awlp: eqtrue.
angel_awlp angelic wlp, e.g. an "angelic" interpretation of non-determinism,
See refinement calculus. This is used for abstraction of concrete termsDefinition angel_awlp (p: atom) (post: state→ Prop) (s:state) : Prop :=
match p with
| guassign l c ⇒ ∃ s', lframeeq l s s' ∧ oeval c s s' ∧ post s'
| skip ⇒ post s
| xrequire c m ⇒ (eval c s) → post s
| ensure c ⇒ (eval c s) ∧ (post s)
| assign x t ⇒ post (add (vid x) (teval t s) s)
end.
Lemma angel_awlp_monotonic p:
∀ (P Q: state → Prop) s, angel_awlp p P s →
(∀ s, P s → Q s) → angel_awlp p Q s.
Proof.
destruct p; simpl; firstorder.
Qed.
Lemma angel_awlp_duality p P s: angel_awlp p P s → ~(awlp p (fun s ⇒ ~(P s)) s).
Proof.
destruct p; simpl; firstorder.
Qed.
Hint Resolve angel_awlp_monotonic angel_awlp_duality: angel.