Commit 5dce6207 by Jean-Christophe Filliâtre

### dijkstra: updated proof on moloch

parent 3a867752
 ... ... @@ -214,7 +214,8 @@ Definition inv_succ2(src:vertex) (s:(set vertex)) (q:(set vertex)) (d:(map ~ (mem y su))) -> (((mem y s) \/ (mem y q)) /\ ((get d y) <= ((get d x) + (weight x y))%Z)%Z)). Require Import Why3. Ltac ae := why3 "alt-ergo". Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. Ltac z := why3 "z3" timelimit 3. (* Why3 goal *) Theorem WP_parameter_shortest_path_code : forall (src:vertex) (dst:vertex), ... ... @@ -274,7 +275,7 @@ intuition; try ae. assert (case: (v2 = v1 \/ v2 <> v1)) by ae. destruct case. subst v2 d4; rewrite Select_eq. apply Path_cons. why3 "z3". z. ae. trivial. subst d4; rewrite Select_neq. ... ... @@ -284,7 +285,7 @@ ae. assert (case: (v2 = v1 \/ v2 <> v1)) by ae. destruct case. subst v2 d4; rewrite Select_eq. apply Path_cons. why3 "z3". z. ae. trivial. ae. ... ...
 ... ... @@ -214,7 +214,8 @@ Definition inv_succ2(src:vertex) (s:(set vertex)) (q:(set vertex)) (d:(map ~ (mem y su))) -> (((mem y s) \/ (mem y q)) /\ ((get d y) <= ((get d x) + (weight x y))%Z)%Z)). Require Import Why3. Ltac ae := why3 "alt-ergo". Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. Ltac z := why3 "z3" timelimit 3. Require Import Classical. Lemma inside_or_exit: ... ... @@ -263,16 +264,17 @@ intros src dst d (h1,h2) q d1 visited ((h3,h4),h5) q1 d2 visited1 assert (is_empty su) by ae. clear result h19 h20. assert (inv_succ src visited2 q3 d3) by why3 "z3". assert (inv_succ src visited2 q3 d3). unfold inv_succ. split; z. assert (mem src visited2) by ae. destruct (inside_or_exit visited2 src x dx); auto. destruct H2 as (y, (z, (dy, (a1, (a2, (a3, (a4, a5))))))). unfold min in h21. assert (mem z q3) by why3 "z3". assert (mem z q3) by z. assert (get d3 z <= get d3 y + weight y z)%Z by ae. assert (dy = get d3 y) by why3 "z3". why3 "z3". assert (dy = get d3 y) by z. z. Qed.
 ... ... @@ -12,7 +12,7 @@ version="8.3pl4"/> ... ... @@ -895,7 +895,7 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -991,18 +991,18 @@ expl="17. loop invariant preservation" sum="b3e2133fbfd60019bb154555b798e714" proved="true" expanded="false" expanded="true" shape="amemV18V12Iainfix <V19amixfix []V15V17IapathV0V18V19FFIaminV17V14V15FIainfix =V16aTrueNIais_emptyV13Nqainfix =V16aTrueFIainv_succ2V0V12V14V15V11V13AainvV0V12V14V15AasubsetV13ag_succV11FIainfix =V12aaddV11V8FIashortest_pathV0V11amixfix []V7V11Iainfix =V10aremoveV11V6AaminV11V6V7FFIais_emptyV6NIainfix =V9aTrueNIais_emptyV6qainfix =V9aTrueFIamemV21V8Iainfix <V22amixfix []V7V20IapathV0V21V22FFIaminV20V6V7FAainv_succV0V8V6V7AainvV0V8V6V7FIainfix =V4amixfix [<-]V2V0c0Aainfix =V3aaddV0aemptyAais_emptyV5FIamemV1avAamemV0avFF">
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!