| products/sources/formale sprachen/Delphi/Bille 0.71/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: README.txt Sprache: PVSUntersuchung PVS© |
|
||||||
|
graph_deg_sum[T: TYPE]: THEORY
BEGIN IMPORTING graph_deg[T], % fslib@finite_sets_sum_real[T] finite_sets@finite_sets_sum_real[T] v: VAR T G,GS: VAR graph[T] x,y: VAR T V_reduced: VAR set[T] P : VAR pred[graph[T]] n : VAR nat e: VAR doubleton[T] S: VAR finite_set[T] f: VAR [T -> real] B: VAR real deg_lem0: LEMMA num_edges(G) = 0 IMPLIES sum(vert(G), (LAMBDA (v: T): deg(v, G))) = 0 deg_lem2: LEMMA remove(x, remove(y, vert(G))) = V_reduced AND e = dbl[T](x, y) AND nonempty?(edges(G)) AND choose(edges(G)) = e IMPLIES sum(V_reduced, (LAMBDA (v:T): deg(v,G))) = sum(V_reduced,(LAMBDA (v:T): deg(v,del_edge(G,e)))) edge_induction : LEMMA (FORALL G : P(G)) IFF (FORALL n, G: num_edges(G) = n IMPLIES P(G)) deg_thm: THEOREM sum(vert(G), (LAMBDA (v: T): deg(v,G))) = 2 * num_edges(G) IMPORTING subgraphs[T] subgraph_deg : THEOREM subgraph?(GS,G) AND vert(G)(v) IMPLIES deg(v,GS) <= deg(v,G) sum_gt_bound : THEOREM (FORALL (t: (S)): f(t) >= B) IMPLIES sum(S,f) >= B*card(S) deg_gt_one : THEOREM (FORALL (v:(vert(G))): deg(v,G) > 1) IMPLIES num_edges(G)>=size(G) END graph_deg_sum ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
