products/sources/formale sprachen/REXX image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: walks.pvs   Sprache: Unknown


walks[T: TYPE]: THEORY

BEGIN

   IMPORTING graphs[T], 
             finite_sets@finite_sets_eq

   G,GG: VAR graph[T]
   n: VAR nat
   
   non_null: TYPE = {M: list[T] | length(M)>0}

   L: VAR non_null
   fs: VAR finseq[T]
 
   x,u,v,u1,u2,v1,v2,v3: VAR T
   e: VAR doubleton[T]
   i,j: VAR nat

   prewalk: TYPE = {w: finseq[T] | length(w) > 0}

   s,ps,ww: VAR prewalk

   verts_in?(G,s): bool = (FORALL (i: below(length(s))): vert(G)(seq(s)(i)))
   
   Seq(G): TYPE = {w: prewalk | verts_in?(G,w)}

   walk?(G,ps): bool = verts_in?(G,ps) AND
                             (FORALL n: n < length(ps) - 1 IMPLIES
                                         edge?(G)(ps(n),ps(n+1)))

   Walk(G): TYPE = {w: prewalk | walk?(G,w)}

   list2prewalk(L: non_null): prewalk =
          (# length := length(L),
             seq := (LAMBDA (x: below[length(L)]): nth(L, x)) #)

   from?(ps,u,v): bool = seq(ps)(0) = u AND seq(ps)(length(ps) - 1) = v

   walk_from?(G,ps,u,v): bool =
           seq(ps)(0) = u AND seq(ps)(length(ps) - 1) = v AND walk?(G,ps)

   Walk_from(G,u,v): TYPE = {w: prewalk | walk_from?(G,w,u,v)}


   verts_of(ww: prewalk): finite_set[T] = 
               {t: T | (EXISTS (i: below(length(ww))): ww(i) = t)}

   edges_of(ww): finite_set[doubleton[T]] = {e: doubleton[T] |
                           EXISTS (i: below(length(ww)-1)): e = dbl(ww(i),ww(i+1))}


   pre_circuit?(G: graph[T], w: prewalk): bool = walk?(G,w) AND 
                                                 w(0) = w(length(w)-1)

%  ----------------------- Properties -----------------------

   verts_in?_concat: LEMMA FORALL (s1,s2: Seq(G)): verts_in?(G,s1 o s2)

   verts_in?_caret : LEMMA FORALL (j: below(length(ps))): i <= j IMPLIES
                                   verts_in?(G,ps) IMPLIES verts_in?(G,ps^(i,j))

  
   vert_seq_lem    : LEMMA FORALL (w: Seq(G)): n < length(w) IMPLIES vert(G)(w(n))

   verts_of_subset : LEMMA FORALL (w: Seq(G)):
                                   subset?(verts_of(w),vert(G))


   edges_of_subset : LEMMA walk?(G,ww) IMPLIES subset?(edges_of(ww),edges(G))

   walk_verts_in   : LEMMA walk?(G,ps) IMPLIES verts_in?(G,ps)


   walk_from_vert  : LEMMA FORALL (w: prewalk,v1,v2:T):
                             walk_from?(G,w,v1,v2) IMPLIES
                                vert(G)(v1) AND vert(G)(v2)

   walk_edge_in    : LEMMA walk?(G,ww) AND 
                           subset?(edges_of(ww),edges(GG)) AND
                           subset?(verts_of(ww),vert(GG))
                         IMPLIES walk?(GG,ww)
  
%  ----------- operations and constructors for walks --------------------

   gen_seq1(G, (u: (vert(G)))): Seq(G) = 
                        (# length := 1, seq := (LAMBDA (i: below(1)): u) #)

   gen_seq2(G, (u,v: (vert(G)))): Seq(G) = 
                  (# length := 2,
                     seq := (LAMBDA (i: below(2)):
                                      IF i = 0 THEN u ELSE v ENDIF) #)
   
   Longprewalk: TYPE = {ps: prewalk | length(ps) >= 2}
   
   trunc1(p: Longprewalk ): prewalk = p^(0,length(p)-2)

   add1(ww,x): prewalk = (# length := length(ww) + 1,
                           seq := (LAMBDA (ii: below(length(ww) + 1)):
                                    IF ii < length(ww) THEN seq(ww)(ii) ELSE x ENDIF)
                         #)


   gen_seq1_is_walk: LEMMA vert(G)(x) IMPLIES walk?(G,gen_seq1(G,x))

   edge_to_walk    : LEMMA u /= v AND edges(G)(edg[T](u, v)) IMPLIES
                             walk?(G,gen_seq2(G,u,v))


   walk?_rev       : LEMMA walk?(G,ps) IMPLIES walk?(G,rev(ps))

   

   w1,w2: VAR prewalk
   walk?_reverse   : LEMMA walk_from?(G,w1,v1,v2) IMPLIES
                             (EXISTS (w: Walk(G)): walk_from?(G,w,v2,v1))

   walk?_caret     : LEMMA i <= j AND j < length(ps) AND walk?(G,ps) 
                               IMPLIES walk?(G,ps^(i,j))



   l_trunc1        : LEMMA length(ww) > 1 IMPLIES length(trunc1(ww)) = length(ww)-1

   
   walk?_add1      : LEMMA walk?(G,ww) AND vert(G)(x)
                           AND edge?(G)(seq(ww)(length(ww)-1),x)
                           IMPLIES walk?(G,add1(ww,x))                      


   walk_concat_edge: LEMMA walk_from?(G, w1, u1, v1) AND
                      walk_from?(G, w2, u2, v2) AND
                              edge?(G)(v1,u2)
                   IMPLIES
                       walk_from?(G, w1 o w2,u1,v2)

   walk_concat: LEMMA length(w1) > 1 AND
              walk_from?(G, w1, u1, v) AND
              walk_from?(G, w2, u2, v)
         IMPLIES
             walk_from?(G, w1 ^ (0, length(w1) - 2) o rev(w2),u1,u2)

   walk?_cut  : LEMMA FORALL (i,j: below(length(ps))): i < j AND
                                  seq(ps)(i) = seq(ps)(j) AND
                                  walk_from?(G, ps, u, v)
                               IMPLIES
                                  walk_from?(G, ps^(0,i) o ps^(j+1,length(ps)-1),u,v)

   yt: VAR T
   p1,p2: VAR prewalk
   walk_merge: LEMMA walk_from?(G, p1, v, yt) AND
                    walk_from?(G, p2, u, yt)
                           IMPLIES
                       (EXISTS (p: prewalk): walk_from?(G, p, u, v))

END walks


[ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ]