| products/Sources/formale Sprachen/Java/openjdk-20-36_src/test/langtools/tools/javac/api/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: coalition_fun.pvs Sprache: CoqOriginal von: PVS© |
|
||||||
|
mucalculus_prop [ T:TYPE ] : THEORY
%------------------------------------------------------------------- % Fixed points of monotonic functions of type [set[T] -> set[T]] % (predicate transformers) % % Shows that operators mu and nu defined in theory mucalculus % of the prelude defines the least and greatest fixpoints of % a monotonic function % % Defines dual(H) = complement o H o complement % % Shows that mu o dual = complement o nu and % nu o dual = complement o mu %------------------------------------------------------------------- BEGIN F: VAR (monotonic?[T]) p, q: VAR pred[T] A: VAR set[pred[T]] % Auxiliary functions defined in the prelude (theory mucalculus): % - relation <= is the same as the subset? relation % - glb(A) = { x:T | EXISTS (p: (A)): p(x) } % - lub(A) = { x:T | FORALL (p: (A)): p(x) } antisymmetry: LEMMA p <= q AND q <= p IMPLIES p = q reflexivity: LEMMA p <= p %--- glb(A) is the greatest lower bound of A glb_lower_bound: LEMMA FORALL (q: (A)): glb(A) <= q glb_greatest_lower_bound: LEMMA p <= glb(A) IFF FORALL (q: (A)): p <= q %--- lub(A) is the least upper bound of A lub_upper_bound: LEMMA FORALL (q: (A)): q <= lub(A) lub_least_upper_bound: LEMMA lub(A) <= p IFF FORALL (q: (A)): q <= p %--- properties of mu operator closure_mu: PROPOSITION F(mu(F)) <= mu(F) smallest_closed: PROPOSITION F(p) <= p IMPLIES mu(F) <= p fixpoint_mu1: PROPOSITION F(mu(F)) = mu(F) fixpoint_mu2: PROPOSITION fixpoint?(F)(mu(F)) least_fixpoint1: PROPOSITION F(p) = p IMPLIES mu(F) <= p least_fixpoint2: PROPOSITION fixpoint?(F)(p) IMPLIES mu(F) <= p mu_lfp: JUDGEMENT mu(F) HAS_TYPE (lfp?(F)) %--- properties of nu operator closure_nu: PROPOSITION nu(F) <= F(nu(F)) largest_closed: PROPOSITION p <= F(p) IMPLIES p <= nu(F) fixpoint_nu1: PROPOSITION F(nu(F)) = nu(F) fixpoint_nu2: PROPOSITION fixpoint?(F)(nu(F)) greatest_fixpoint1: PROPOSITION F(p) = p IMPLIES p <= nu(F) greatest_fixpoint2: PROPOSITION fixpoint?(F)(p) IMPLIES p <= nu(F) nu_gfp: JUDGEMENT nu(F) HAS_TYPE (gfp?(F)) %--- dual of a predicate transformer H: VAR [pred[T] -> pred[T]] dual(H): [pred[T] -> pred[T]] = complement o H o complement dual_dual : LEMMA dual(dual(H)) = H dual_inclusion1 : LEMMA H(complement(p)) <= complement(p) IFF p <= dual(H)(p) dual_inclusion2 : LEMMA complement(p) <= H(complement(p)) IFF dual(H)(p) <= p dual_inclusion3 : LEMMA H(p) <= p IFF complement(p) <= dual(H)(complement(p)) dual_inclusion4 : LEMMA p <= H(p) IFF dual(H)(complement(p)) <= complement(p) %--- fixed points and dual monotonic_dual_monotonic: JUDGEMENT dual(F) HAS_TYPE (monotonic?[T]) least_fixpoint_dual: PROPOSITION mu(dual(F)) = complement(nu(F)) greatest_fixpoint_dual: PROPOSITION nu(dual(F)) = complement(mu(F)) END mucalculus_prop ¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
