| products/sources/formale Sprachen/PVS/scott/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: top.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
%------------------------------------------------------------------------------
% Top for Scott Topology % % All references are to BA Davey and HA Priestly "Introduction to Lattices and % Orders", CUP, 1990. % % This library defines the Scott Topology, and shows that continuous functions % are increasing and lub-preserving; and -- under pointwise-ordering -- also % form a Scott Topology. % % The main reason Computer Scientists are interested is that it constitutes a % general foundation on which to build the fixpoint theory needed for the % semantics of loops or recursion. % % Author: David Lester, Manchester University, NIA, Université Perpignan % % Version 1.0 25/12/07 Initial Version %------------------------------------------------------------------------------ top: THEORY BEGIN IMPORTING partial_function_props, % Easy-to-use partial function properties scott, % Definition of Scott Topology scott_continuity, % Definition of Continuity pointwise_orders_aux, % Extras for continuous pointwise orders scott_identity_continuity, % Identity is scott continuous scott_composition_continuity, % Composition is scott continuous fixpoints, % Definition of Fixpoints admissible, % Fixpoint induction dual_fixpoints, % Fixpoint Induction over two types scott_product % Extras for orders library %% INTEGRATED %% % % bounded_orders_aux, % Extras for orders@bounded_orders % ordered_subset_aux, % Extras for orders@ordered_subset % % New Theory files for orders library %% MOVED %% % % lift_props, % Extras for the lift datatype % directed_orders, % New theories for orders library % bounded_order_props, % Properties of bounded orders % directed_order_props, % Properties of directed orders % partial_order_props, % Properties of partial orders % partial_order_lift % lifted_orders, % Induced properties of lifted orders % sum_orders, % Induced properties of union orders % product_orders % Induced properties of product orders END top ¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
