Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: min_walks.pvs Sprache: PVS

Original von: PVS^©

min_walks[T: TYPE]: THEORY

BEGIN

   IMPORTING graphs[T]

   IMPORTING walks[T], abstract_min

   v1,v2,x,y: VAR T
   G: VAR graph[T]

   gr_walk(v1,v2): TYPE = {G: graph[T] | vert(G)(v1) AND vert(G)(v2) AND
                                         (EXISTS (w: Seq(G)):
                                           walk_from?(G,w,v1,v2))}

   min_walk_from(x,y,(Gw:gr_walk(x,y))): Walk(Gw) =
                        min[Seq(Gw),(LAMBDA (w: Seq(Gw)): length(w)),
                                (LAMBDA (w: Seq(Gw)): walk_from?(Gw,w,x,y))]

   is_min(G,(w: Seq(G)),x,y): bool = walk?(G,w) AND
                       (FORALL (ww: Seq(G)): walk_from?(G,ww,x,y) IMPLIES
                                                        length(w) <= length(ww))

   min_walk_def: LEMMA FORALL (Gw: gr_walk(x,y)):
                          walk_from?(Gw,min_walk_from(x,y,Gw),x,y) AND
                          is_min(Gw, min_walk_from(x,y,Gw),x,y)

   min_walk_in : LEMMA FORALL (Gw: gr_walk(x,y)):
                          walk_from?(Gw,min_walk_from(x,y,Gw),x,y)

   min_walk_is_min: LEMMA FORALL (Gw: gr_walk(x,y), ww: Seq(Gw)):
                              walk_from?(Gw,ww,x,y) IMPLIES
                                        length(min_walk_from(x,y,Gw)) <= length(ww)

END min_walks

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.