Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/digraphs/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 1 kB

Quelle ind_paths.pvs Sprache: PVS

ind_paths[T: TYPE]: THEORY

BEGIN

   IMPORTING paths[T]

   G: VAR digraph[T]
   u,v,s,t: VAR T
   e: VAR edgetype[T]
   V: VAR finite_set[T]
   n: VAR nat

   independent?(w1,w2: prewalk): bool =
                       (FORALL (i,j: nat): i > 0 AND i < length(w1) - 1 AND
                                           j > 0 AND j < length(w2) - 1 IMPLIES
                                    seq(w1)(i) /= seq(w2)(j))

   p1,p2: VAR prewalk
   independent?_comm: LEMMA independent?(p1,p2) IMPLIES
                                    independent?(p2,p1)

   independent_ne: LEMMA length(p1) > 2 AND independent?(p1,p2) IMPLIES p1 /= p2

   ps: VAR prewalk

   IMPORTING finite_sets

   set_of_paths(G,s,t): TYPE = finite_set[Path_from(G,s,t)]

   ind_path_set?(G,s,t,(pset: set_of_paths(G,s,t))): bool =
                   (FORALL (p1,p2: Path_from(G,s,t)):
                             pset(p1) AND pset(p2) AND  p1 /= p2
                                         IMPLIES independent?(p1,p2))

   ind_path_set_2: LEMMA FORALL (ips: set_of_paths(G,s,t)):
                                    card(ips) = 2 AND
                                    ind_path_set?(G, s, t, ips)
                              IMPLIES
                         (EXISTS (P_1,P_2: prewalk): path_from?(G, P_1, s, t) AND
                                                     path_from?(G, P_2, s, t) AND
                                                      independent?(P_1,P_2) )

   internal_verts(w: prewalk): finite_set[T] =
               {t: T | (EXISTS (i: nat): i > 0 AND i < length(w) - 1 AND w(i) = t)}

   indep?(w1,w2: prewalk): bool = empty?(intersection(internal_verts(w1),
                                                      internal_verts(w2)))

   w1,w2: VAR prewalk
   indep?_lem: LEMMA indep?(w1,w2) IFF independent?(w1,w2)

END ind_paths

quality98%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.