/* * graph nodes */ #define NULL ((void*)0) typedef struct struct_node { unsigned int m :1, c :1; struct struct_node *l, *r; } * node; /* * logical lists of nodes */ /*@ type plist */ /*@ logic plist cons(node p, plist l) */ /*@ predicate in_list(node p,plist stack) */ /*@ predicate pair_in_list(node p1, node p2, plist stack) */ /* * graph reachability, stack */ /*@ predicate reachable(node p1, node p2) @ reads p1->r,p1->l @*/ /*@ axiom reachable_refl : \forall node p ; reachable(p,p) */ /*@ predicate unmarked_reachable(node p1, node p2) @ reads p1->r,p1->l,p1->m @*/ /*@ predicate clr_list(node p, plist stack) @ reads p->c,p->l,p->r @*/ /*@ predicate reachable_elements(node p, node t, plist s) @ reads p->l,p->r @*/ /* * the complexity measure for termination */ //@ type weight_type /*@ logic weight_type weight(node p, node t) @ reads p->m,p->c,p->l,p->r @*/ /* * Schorr-Waite algorithm */ /*@ requires @ (\forall node x; @ x != \null && reachable(root,x) => \valid(x) && ! x ->m) @ && \exists plist l; reachable_elements(root,root,l) @ ensures @ (\forall node x; \old(x->l) == x->l && \old(x->r) == x->r) @ && @ (\forall node x; \valid(x) && reachable(root,x) => x->m) @ && @ (\forall node x; ! reachable(root,x) => x->m == \old(x->m)) */ void schorr_waite(node root) { node t = root; node p = NULL; /*@ @ invariant @ @ (I1 :: \forall node x; \old(reachable(root,x)) => @ reachable(t,x) || reachable(p,x)) @ && @ (I2 :: \forall node x; x != \null => // pourquoi pas && ? @ (reachable(t,x) || reachable(p,x) => @ \old(reachable(root,x)))) @ && @ (I0 :: \exists plist stack; @ (I3 :: clr_list(p,stack)) @ && @ (I4 :: \forall node p; in_list(p,stack) => p->m) @ && @ (I5 :: \forall node x; @ \valid(x) && \old(reachable(root,x)) && !x->m => @ unmarked_reachable(t,x) || @ (\exists node y; @ in_list(y,stack) && unmarked_reachable(y->r,x))) @ && @ (I6 :: \forall node x; !in_list(x,stack) => @ (x->r == \old(x->r) && x->l == \old(x->l))) @ && @ (I7 :: \forall node p1; (\forall node p2; @ pair_in_list(p1,p2,cons(t,stack)) => @ (p2->c => \old(p2->l) == p2->l && \old(p2->r) == p1) @ && @ (!p2->c => \old(p2->l) == p1 && \old(p2->r) == p2->r))) @ && @ (I8 :: \forall node x; @ ! \old(reachable(root,x)) => x->m == \old(x->m))) @ @ variant weight(p,t) for order_mark_m_and_c_and_stack @ @*/ /* I7 aurait pu etre (\forall node p1; (\forall node p2; pair_in_list(p1,p2,stack) => (\old(p2->l) == (p2->c ? p2->l : p1)) && (\old(p2->r) == (p2->c ? p1 : p2->r)))) */ while (p != NULL || (t != NULL && ! t->m)) { if (t == NULL || t->m) { if (p->c) { /* pop */ node q = t; t = p; p = p->r; t->r = q; } else { /* swing */ node q = t; t = p->r; p->r = p->l; p->l = q; p->c = 1; } } else { /* push */ node q = p; p = t; t = t->l; p->l = q; p->m = 1; p->c = 0; } } }