NASA logo

+ Contact NASA



  • + HOME
  • + WELCOME
  • + QUICK PAGE
  • + PHILOSOPHY
  • + TEAM
  • + RESEARCH
  • + LINKS

  • Top File of PVS scott Library

     
    %------------------------------------------------------------------------------
    % 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
    

    The tag [*] identifies links that are outside the NASA domain