Commit a2fdd18a authored by Armaël Guéneau's avatar Armaël Guéneau

StackDFS: prove a more convenient derived spec for iter_edges

parent dd60afd4
......@@ -104,7 +104,7 @@ Proof.
Qed.
Lemma inv_step_push : forall G n a C L i j js,
inv G n a C L ('{j} \u js) ->
inv G n a C L (js \u \{j}) ->
C[i] = true ->
has_edge G i j ->
inv G n a (C[j:=true]) (j :: L) js.
......@@ -128,7 +128,7 @@ Proof.
Qed.
Lemma inv_step_skip : forall G n a C L j js,
inv G n a C L ('{j} \u js) ->
inv G n a C L (js \u \{j}) ->
C[j] = true ->
inv G n a C L js.
Proof.
......@@ -173,6 +173,27 @@ Lemma remove_all : forall A (E: set A),
E \- E = \{}.
Proof. intros. rew_set. intros. rew_set. tauto. Qed.
Lemma iter_edges_remaining_spec : forall (I:set int->hprop) (G:graph) g f i,
i \in nodes G ->
(forall L, (g ~> RGraph G) \c (I L)) ->
(forall j E, j \notin E -> has_edge G i j ->
(app f [j] (I (E \u \{j})) (# I E))) ->
app Graph_ml.iter_edges [g i f]
PRE (I (out_edges G i))
POST (# I \{}).
Proof.
intros. xapp_spec~ iter_edges_spec (>> (fun E => I (out_edges G i \- E)) G).
{ introv Hj Hij. xapp~.
{ intro HH. rew_set in HH. tauto. }
{ hsimpl. match goal with |- I ?x ==> I ?y \* _ => asserts_rewrite (x = y) end.
{ rew_set. intro x. rew_set. rew_logic. iff; unpack.
{ tests~: (x = j). }
{ tests~: (x = j). branches; [| now false]. tauto. } }
hsimpl. } }
{ rewrite remove_empty. hsimpl. }
{ rewrite remove_all. hsimpl. }
Qed.
Lemma reachable_imperative_spec : forall g G a b,
a \in nodes G ->
b \in nodes G ->
......@@ -206,7 +227,8 @@ Proof.
xseq (Hexists C L, hinv \{} C L).
xapp*. intros L' HL'. subst L.
xfun as f. forwards~ [Gi Ci]: inv_stack I i.
xapp (fun E => Hexists C2 L2, hinv (out_edges G i \- E) C2 L2 \* \[ C2[i] = true ]) G.
xapp_spec iter_edges_remaining_spec
(>> (fun E => Hexists C2 L2, hinv E C2 L2 \* \[ C2[i] = true ]) G).
{ auto. }
{ unfold hinv. intros. skip.
(* eapply heap_contains_intro. (* evar context issues? *) skip. skip. *) }
......@@ -216,13 +238,11 @@ Proof.
xif.
{ xapps. skip. xapp. intros _. unfold hinv. hsimpl.
{ rewrite read_update_case. case_if~. skip. }
applys~ inv_step_push i. equates 1. applys~ I'. skip. }
{ xrets. unfold hinv. hsimpl.
{ applys~ inv_step_skip j. equates 1. applys~ I'. skip. }
auto. } }
{ unfold hinv. hsimpl. rewrite remove_empty. apply~ inv_step_pop. }
applys~ inv_step_push i. }
{ xrets. unfold hinv. hsimpl. now applys~ inv_step_skip j. auto. } }
{ unfold hinv. hsimpl. apply~ inv_step_pop. }
{ rew_bool_eq~. }
{ intros r'. hpull;=> C2 L2 ?. rewrite remove_all. hsimpl. }
{ hsimpl. }
{ intros C2 L2. xapplys~ HS. } }
{ (* case loop end *)
xret. unfold hinv. subst L. hsimpl*. { rew_bool_eq*. } } }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment