| products/sources/formale Sprachen/VDM/VDMRT/VeMoRT/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: graph-ed.vdmsl Sprache: PVSUntersuchung PVS© |
|
||||||
|
% Lattices that have a "complement" function. See also complementary_orders.
% complementary_lattices[ T: TYPE+, (IMPORTING bounded_orders[T]) <=: (lattice?[T]) ]: THEORY BEGIN IMPORTING lattices[T, <=], minmax_orders[T], function_image_extra[T, T], complementary_orders[T] t, t1, t2: VAR T C, H: VAR [T -> T] S: VAR set[T] NF: VAR non_empty_finite_set[T] % modular?(<=): bool = % FORALL (a, c: T): % a <= c => lub(<=)(a, glb(<=)(b, c)) = glb(<=)(lub(<=)(a, b), c) dual(C)(H): [T -> T] = C o H o C dual_dual : LEMMA FORALL (C: (complement?(<=))): dual(C)(dual(C)(H)) = H dual_inclusion1 : LEMMA FORALL (C: (complement?(<=))): H(C(t)) <= C(t) IFF t <= dual(C)(H)(t) dual_inclusion2 : LEMMA FORALL (C: (complement?(<=))): C(t) <= H(C(t)) IFF dual(C)(H)(t) <= t dual_inclusion3 : LEMMA FORALL (C: (complement?(<=))): H(t) <= t IFF C(t) <= dual(C)(H)(C(t)) dual_inclusion4 : LEMMA FORALL (C: (complement?(<=))): t <= H(t) IFF dual(C)(H)(C(t)) <= C(t) END complementary_lattices ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.24Angebot 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 |
