Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: top.pvs Sprache: PVS

Original 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.1 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.