| products/sources/formale Sprachen/Coq/dev/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: real_topology.prf Sprache: PVSUntersuchung PVS© |
|
||||||
|
subgraphs[T: TYPE]: THEORY
BEGIN IMPORTING graphs[T] V: VAR set[T] G,G1,G2,SS: VAR graph[T] i: VAR T e: VAR doubleton[T] subgraph?(G1,G2): bool = subset?(vert(G1),vert(G2)) AND subset?(edges(G1),edges(G2)) equal?(G1,G2): bool = subgraph?(G1,G2) AND subgraph?(G2,G1) Subgraph(G): TYPE = {S: graph[T] | subgraph?(S,G)} finite_vert_subset: LEMMA is_finite(LAMBDA (i:T): vert(G)(i) AND V(i)) subgraph(G, V): Subgraph(G) = (G WITH [vert := {i | vert(G)(i) AND V(i)}, edges := {e | edges(G)(e) AND (FORALL (x: T): e(x) IMPLIES V(x))}]) subgraph_vert_sub: LEMMA subset?(V,vert(G)) IMPLIES vert(subgraph(G,V)) = V subgraph_lem : LEMMA subgraph?(subgraph(G,V),G) subgraph_smaller: LEMMA subgraph?(SS, G) IMPLIES size(SS) <= size(G) END subgraphs ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.29Angebot 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 |
