|
%********************************************************************************%
%
% 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
%
%********************************************************************************%
% A cycle is a simple circuit; i.e., a walk without repetions except for the end points
cycles[T: TYPE]: THEORY
BEGIN
IMPORTING circuits[T]
G: VAR digraph[T]
w: VAR prewalk
% --------------------------------------------------------------------------------
% Definitions
% --------------------------------------------------------------------------------
cycle?(G: digraph[T], w: prewalk): bool =
circuit?(G,w) AND
(FORALL (i,j: below(length(w)-1)): i /= j IMPLIES w(i) /= w(j))
% --------------------------------------------------------------------------------
% Properties
% --------------------------------------------------------------------------------
cycle_is_circuit : LEMMA
FORALL (G: digraph[T], w: prewalk) : cycle?(G,w) IMPLIES circuit?(G,w)
% cycle_has_path: LEMMA FORALL (w: prewalk): cycle?(G,w) IMPLIES
% (EXISTS (j: below(length(w))): path?(G,w^(0,j)))
circuit_subwalk_cycle: LEMMA
circuit?(G, w) IMPLIES
EXISTS (w1: prewalk): sub_walk?(G, w, w1) AND cycle?(G,w1)
cycle_prefix: LEMMA
circuit?(G,w) IMPLIES
(cycle?(G,w) OR EXISTS (w1, w2 : prewalk): eq_circuit?(G, w, w1 o w2)
AND cycle?(G,w1))
cycle_o_circuit: LEMMA
circuit?(G,w) IMPLIES
(cycle?(G,w) OR EXISTS (w1, w2 : prewalk): eq_circuit?(G, w, w1 o rest(w2))
AND cycle?(G,w1) AND circuit?(G,w2))
%--------------------------------------------------------------------------------
IMPORTING digraphs, finite_sets@finite_sets_card_eq, structures@seq_pigeon
GF: VAR Digraph[T]
Pigeon_hole: THEOREM FORALL (w: Walk(GF)): length(w) > card(vert(GF)) IMPLIES
(EXISTS (i,j: below(length(w))): i /= j AND w(i) = w(j))
END cycles
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.23Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
