| products/sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: PVSUntersuchung PVS© |
|
||||||
|
%------------------------------------------------------------------------------
% Properties of Lifted Orders % % Author: David Lester <[email protected]> Manchester University % % We define a lifting operator on relations, and show that this operation % preserves directed completeness and pointedness. % % Version 1.0 03/30/06 %------------------------------------------------------------------------------ lifted_orders[T:TYPE]: THEORY BEGIN rel: VAR pred[[T,T]] x,y: VAR lift[T] IMPORTING lift_props[T] lift(rel)(x,y):bool = (NOT up?(x)) OR (up?(y) AND rel(down(x),down(y))) lift_preserves_reflexive: JUDGEMENT lift(r:(reflexive?[T])) HAS_TYPE (reflexive?[lift[T]]) lift_preserves_transitive: JUDGEMENT lift(r:(transitive?[T])) HAS_TYPE (transitive?[lift[T]]) lift_preserves_antisymmetric: JUDGEMENT lift(r:(antisymmetric?[T])) HAS_TYPE (antisymmetric?[lift[T]]) lift_preserves_preorder: JUDGEMENT lift(r:(preorder?[T])) HAS_TYPE (preorder?[lift[T]]) lift_preserves_partial_order: JUDGEMENT lift(r:(partial_order?[T])) HAS_TYPE (partial_order?[lift[T]]) IMPORTING directed_orders[T], directed_orders[lift[T]] lift_lub_emptyset: LEMMA lub(lift(rel))(emptyset[lift[T]]) = bottom lift_lub_bounded: LEMMA FORALL (rel:(antisymmetric?[T]), S:(nonempty_least_bounded_above?(rel))): lub(lift(rel))(image[T,lift[T]](up,S)) = up(lub(rel)(S)) lift_preserves_directed_complete: JUDGEMENT lift(r:(directed_complete?[T])) HAS_TYPE (directed_complete?[lift[T]]) lift_preserves_directed_complete_partial_order: JUDGEMENT lift(r:(directed_complete_partial_order?[T])) HAS_TYPE (pointed_directed_complete_partial_order?[lift[T]]) END lifted_orders ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.4Angebot 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 |
