Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Sprache: Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/ACCoRD/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: declare.ml Sprache: SML

Untersuchung PVS^©

cycles[T: TYPE]: THEORY

BEGIN

   IMPORTING paths[T]

   G: VAR graph[T]

   cycle?(G: graph[T], (w: Seq(G))): bool = pre_circuit?(G,w) AND length(w) > 1 AND
                          w(1) /= w(length(w)-2) AND
                          (FORALL (i,j: below(length(w))):
                             w(i) = w(j) IMPLIES (i = j OR
                                         (endpoint?(i,w) AND endpoint?(j,w))))

   cycle_l_gt_3: LEMMA (FORALL (w: Seq(G)): cycle?(G,w) IMPLIES length(w) > 3)

   cycle_has_path: LEMMA FORALL (w: Seq(G)): cycle?(G,w) IMPLIES
                            (EXISTS (j: below(length(w))): path?(G,w^(0,j)))

%% -- the term "w(1) /= w(length(w)-2)" rules out length(w) = 2 AND length(w) = 3 --


   cycle_gt3: LEMMA FORALL (w: Seq(G)):  cycle?(G,w) IMPLIES length(w) > 3

   cycle_def: LEMMA FORALL (w: Seq(G)): cycle?(G,w) IFF
                          pre_circuit?(G,w) AND length(w) > 3 AND
                          (FORALL (i,j: below(length(w))):
                             w(i) = w(j) IMPLIES (i = j OR
                                         (endpoint?(i,w) AND endpoint?(j,w))))


END cycles