enrich INV , 
       nat_or_fail with
comment: Definition of the algorithm BFS.;
   procedures 
      BFS  elem × elem : nat_or_fail nondeterministic;
      ADD  set : set × set nonfunctional nondeterministic;
   variables 
      source, dest : elem; 
      S, V, C, N : set; 
      v, w : elem; 
      done : bool; 
declaration 
   BFS (source, dest; norfail)
     { 
        let V = {source} , C = {source} , N = ∅, n = 0, done = false
        in { 
              while C ≠ ∅ ∧ ¬ done
              do { 
                    choose  v with v ∈ C in if v = dest
                                            then done := true
                                            else { 
                                                    C := C -- v ; ADD(succ(v); V, N)
                                                 } ; 
                    if C = ∅
                    then C := N, N := ∅, n := n + 1
                 } ; 
              norfail := (done ⊃ some(n); fail)
           }
     };
   ADD (S; V, N)
     { 
        while S ≠ ∅ do choose  w with w ∈ S in { 
                                                  S := S -- w ; if ¬ w ∈ V
                                                  then V := V ++ w, N := N ++ w
                                               }
     };
end enrich