products/sources/formale Sprachen/PVS/digraphs/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: LaTeXLog.C   Sprache: PVS

Untersuchung PVS©
walks[T: TYPE]: THEORY

BEGIN

   IMPORTING digraphs[T],
             structures@seq_extras[T]
             


   G,GG: VAR digraph[T]
   n: VAR nat
   x,u,v,u1,u2,v1,v2,v3: VAR T
   e: VAR edgetype[T]
   i,j: VAR nat


% -------------------------------------------------------------------------------
%     Definitions
% -------------------------------------------------------------------------------

   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)}

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

   walk_from?(G,ps,u,v): bool = from?(ps,u,v) AND walk?(G,ps)

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

   set_walk_from(G, e): set[prewalk] = 
         LET (u, v) = e IN {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[edgetype[T]] = {e: edgetype[T] |
                           EXISTS (i: below(length(ww)-1)): e = (ww(i),ww(i+1))}

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

   walk_from_l     : LEMMA walk_from?(G,ps,u,v) AND u /= v IMPLIES length(ps) >= 2

   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)

   prewalk_across: LEMMA ww(0) /= ww(length(ww)-1) AND length(ww) > 1 IMPLIES
                        (EXISTS (i: below(length(ww)-1)): ww(i) = ww(0) AND
                                                  ww(i+1) /= ww(0))
  
%  ----------- 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}

   lWalk(G) : TYPE = {w: Longprewalk | walk?(G,w)}
   
   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)((u, v)) IMPLIES
                             walk?(G,gen_seq2(G,u,v))

   w1,w2: VAR prewalk

%%%%%%%%%%%%%%%%%%%%% NOT THEOREMS for directed graphs %%%%%%%%%%%%%%
%
%   walk?_rev       : LEMMA walk?(G,ps) IMPLIES walk?(G,rev(ps))
%
%   
%
%   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, v, u2)
         IMPLIES
             walk_from?(G, w1 ^ (0, length(w1) - 2) o 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, u, yt) AND
                    walk_from?(G, p2, yt, v )
                           IMPLIES
                       (EXISTS (p: prewalk): walk_from?(G, p, u, v))




%********************************************************************************%
%
%   Contributions from:
%
%       Andréia Borges Avelar -- Universidade de Brasília - Brasil  
%       Mauricio Ayala-Rincon -- Universidade de Brasília - Brasil  
%                 Cesar Muñoz -- NASA Langley Research Center - US
%
%********************************************************************************%

% --------------------------------------------------------------------------------
%     Definitions
% --------------------------------------------------------------------------------

 sub_walk?(G: digraph, w: Walk(G), ww): bool =  
    EXISTS (i, j: below(length(w))): w^(i,j) = ww

 reachable?(G)( u, v : (vert(G)) ) : bool = (u = v OR
    EXISTS (w: prewalk) : walk_from?(G, w, u, v))

 reord_prewalk(w: prewalk, i: posnat): prewalk =
    w ^ (i, length(w) - 1) o w ^ (0, i - 1)

 eq_prewalk?(w1, w2: prewalk): bool =
    w1 = w2 OR EXISTS (i: posnat): w2 = reord_prewalk(w1, i)

 % owalk(G: digraph, w1, w2: Walk(G) | last(w1) = first(w2)): Walk(G) =
 %     w1 o rest(w2)


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

 eq_relation_eq_prewalk: LEMMA
    equivalence?(eq_prewalk?)

 eq_prewalk_length: LEMMA
    FORALL(w1, w2: prewalk): eq_prewalk?(w1, w2) IMPLIES length(w1) = length(w2)

 subwalk_is_walk : LEMMA
    FORALL (w: Walk(G)): sub_walk?(G, w, ww) IMPLIES walk?(G, ww)

 walk_o: LEMMA
    walk?(G, w1) AND walk?(G, w2) AND seq(w1)(length(w1) - 1) = seq(w2)(0)
    IMPLIES walk?(G, w1 o w2^(1, length(w2) - 1))

 edges_o_walk: LEMMA
    walk?(G, w1) AND walk?(G, w2) AND last(w1) = first(w2)
    IMPLIES edges_of(w1 o rest(w2)) = union(edges_of(w1), edges_of(w2))


END walks


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.22Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff