|
meng_scaff_defs[T: TYPE]: THEORY
BEGIN
IMPORTING paths[T], subgraphs[T], sep_sets[T],
path_ops[T], subgraph_paths[T]
G,HH: VAR graph[T]
w1,w2,v,s,t,z: VAR T
e: VAR doubleton[T]
V: VAR finite_set[T]
p: VAR prewalk
IMPORTING ind_paths[T]
path_comp(G,(x:T)): Subgraph(G) = subgraph(G,path_verts(G,x))
IMPORTING graph_deg[T]
H(G,(x,w1,w2:T)): Subgraph(G) = path_comp(del_vert(del_vert(G,w1),w2),x)
incident(v,G,(x,w1,w2:T)): finite_set[doubleton[T]]
= {e: doubleton[T] | (EXISTS z: edges(G)(e) AND e = dbl(v,z)
AND vert(H(G,x,w1,w2))(z))}
meng(G,(x,y: (vert(G))),(w1,w2: {t | vert(G)(t) AND t /= y})): graph[T] =
(# vert := add(y,add(w1,add(w2,vert(H(G,x,w1,w2))))),
edges := add(dbl(w1,y), add(dbl(w2,y),
union(edges(H(G,x,w1,w2)),
union(incident(w1,G,x,w1,w2),
incident(w2,G,x,w1,w2)))))
#)
in?(G,s,t,w1,w2): bool = vert(G)(s) AND vert(G)(t) AND vert(G)(w1)
AND vert(G)(w2)
disjoint?(s,t,w1,w2): bool = (s /= t AND w1 /= w2 AND w1 /= s AND w2 /= s
AND w1 /= t AND w2 /= t)
vert_H_s: LEMMA vert(G)(s) AND s /= w1 AND s /= w2
IMPLIES vert(H(G, s, w1, w2))(s)
path_H_W : LEMMA path?(H(G,s,w1,w2),p) IMPLIES
NOT verts_of(p)(w1) AND NOT verts_of(p)(w2)
% MOVED TO theory subgraph_paths
%
% walk?_subgraph : LEMMA subgraph?(HH,G) AND walk?(HH, p)
% IMPLIES walk?(G, p)
%
% path?_subgraph : LEMMA subgraph?(HH,G) AND path?(HH, p)
% IMPLIES path?(G, p)
path_comp_in : LEMMA path?(H(G,s,w1,w2),p) IMPLIES path?(G,p)
walk?_H : LEMMA walk?(G, p) AND seq(p)(0) = s AND
NOT verts_of(p)(w1) AND NOT verts_of(p)(w2)
IMPLIES walk?(H(G, s, w1, w2), p)
vert_meng_sub : LEMMA in?(G, s, t, w1, w2) AND disjoint?(s, t, w1, w2)
IMPLIES subset?(vert(meng(G, s, t, w1, w2)), vert(G))
del_vert_comm : LEMMA del_vert(del_vert(G,w2),w1) =
del_vert(del_vert(G,w1),w2)
H_comm : LEMMA H(G, t, w2, w1) = H(G, t, w1, w2)
incident_comm : LEMMA incident(v, G, t, w2, w1) = incident(v, G, t, w1, w2)
meng_comm : LEMMA vert(G)(s) AND vert(G)(t) AND
vert(G)(w1) AND w1 /= s AND
vert(G)(w2) AND w2 /= s
IMPLIES meng(G, t, s, w1, w2) = meng(G, t, s, w2, w1)
END meng_scaff_defs
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.20Angebot
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
|
