|
paths[T: TYPE]: THEORY
BEGIN
IMPORTING graphs[T], walks[T]
G: VAR graph[T]
x,y,s,t: VAR T
i,j: VAR nat
p,ps: VAR prewalk
path?(G,ps): bool = walk?(G,ps) AND (FORALL (i,j: below(length(ps))):
i /= j IMPLIES ps(i) /= ps(j))
Path(G): TYPE = {p: prewalk | path?(G,p)}
path_from?(G,ps,s,t): bool = path?(G,ps) AND from?(ps,s,t)
Path_from(G,s,t): TYPE = {p: prewalk | path_from?(G,p,s,t)}
endpoint?(i: nat, w: prewalk): bool = (i = 0) OR (i = length(w)-1)
path_verts(G,(x:T)): set[T] = {v: T | EXISTS (w: prewalk): walk_from?(G,w,x,v)}
path?_verts : LEMMA path?(G,ps) IMPLIES verts_in?(G,ps)
path_from_l : LEMMA path_from?(G,ps,s,t) AND s /= t IMPLIES length(ps) >= 2
path_from_in : LEMMA path_from?(G, ps, s, t) IMPLIES
vert(G)(s) AND vert(G)(t)
path?_caret : LEMMA i <= j AND j < length(ps) AND path?(G,ps)
IMPLIES path?(G,ps^(i,j))
path_from?_caret: LEMMA i <= j AND j < length(ps) AND path_from?(G, ps, s, t)
IMPLIES path_from?(G, ps^(i, j),seq(ps)(i),seq(ps)(j))
path?_rev : LEMMA path?(G,ps) IMPLIES path?(G,rev(ps))
path?_gen_seq2 : LEMMA vert(G)(x) AND vert(G)(y) AND
edge?(G)(x,y) IMPLIES path?(G,gen_seq2(G,x,y))
path?_add1 : LEMMA path?(G,p) AND vert(G)(x)
AND edge?(G)(seq(p)(length(p)-1),x)
AND NOT verts_of(p)(x)
IMPLIES path?(G,add1(p,x))
path?_trunc1 : LEMMA path?(G,p) AND length(p) > 1 IMPLIES
path_from?(G,trunc1(p),seq(p)(0),seq(p)(length(p)-2))
END paths
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.28Angebot
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
|
