| products/sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: nth_derivatives.pvs Sprache: PVSUntersuchung PVS© |
|
||||||
|
% Ordered sets (T, <=) that have a "complement" function, i.e.,
% an involutorian, anti-monotone function from T to T. % complementary_orders[T: TYPE+]: THEORY BEGIN IMPORTING bounded_orders[T] rel: VAR pred[[T, T]] C: VAR [T -> T] t, t1, t2: VAR T S: VAR set[T] complement?(rel)(C): bool = C o C = id[T] & preserves(C, rel, converse(rel)) % complement_is_bijective: JUDGEMENT % (complement?(rel)) SUBTYPE_OF (bijective?[T, T]) complement_complement: LEMMA FORALL (C: (complement?(rel))): C(C(t)) = t image_complement: LEMMA FORALL (C: (complement?(rel))): image(C, image(C, S)) = S inverse_complement: LEMMA FORALL (C: (complement?(rel))): inverse[T, T](C) = C % inverse_complement_is_complement: JUDGEMENT % inverse[T, T](C: (complement?(rel))) HAS_TYPE (complement?(rel)) le_complement: LEMMA FORALL (C: (complement?(rel))): rel(C(t1), C(t2)) IFF rel(t2, t1) upper_bound_complement: LEMMA FORALL (C: (complement?(rel))): upper_bound?[T](t, S, rel) IFF lower_bound?[T](C(t), image(C, S), rel) bounded_above_complement: LEMMA FORALL (C: (complement?(rel))): bounded_above?[T](S, rel) IFF bounded_below?[T](image(C, S), rel) least_upper_bound_complement: LEMMA FORALL (C: (complement?(rel))): least_upper_bound?[T](t, S, rel) IFF greatest_lower_bound?[T](C(t), image(C, S), rel) least_bounded_above_complement: LEMMA FORALL (C: (complement?(rel))): least_bounded_above?[T](S, rel) IFF greatest_bounded_below?[T](image(C, S), rel) lub_complement: LEMMA FORALL (rel: (antisymmetric?[T]), C: (complement?(rel)), S: (least_bounded_above?(rel))): lub[T](rel)(S) = C(glb[T](rel)(image(C, S))) glb_complement: LEMMA FORALL (rel: (antisymmetric?[T]), C: (complement?(rel)), S: (greatest_bounded_below?(rel))): glb[T](rel)(S) = C(lub[T](rel)(image(C, S))) END complementary_orders ¤ 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 |
