NASA logo

+ Contact NASA

  • + HOME
  • + TEAM
  • + LINKS

  • Top File of PVS ints Library

    top: THEORY
    % Integers library  
    %       Authors:   Rick Butler       NASA Langley
    %                  Paul Miner        NASA Langley
    %                  Bruno Dutertre    Royal Holloway & Bedford New College
    %                  Alfons Geser      HTWK Leipzig, Germany
    % Date: May, 2009
    % Defines "div" according to the Ada Reference Manual
    %  div                 -- Ada Reference Manual division theory
    %  rem                 -- Ada Reference Manual rem theory
    % This div truncates toward zero on a negative argument.
    % Version 1.2 Changed mod to mod_ in PVS4.0 because PVS no longer allows you to 
    %             redefine a theory defined in the prelude.
    % Version 1.3 Changed "divides" to "divides?" so as to not conflict with
    %             prelude definition
    % Version 1.4 Moved all of number_theory library to ints library
    % NOTE: The old approach of having two different definitions of "div"
    %       and "mod" defined in different theories is no longer reasonable
    %       given that "mod" is now defined in the prelude.  The alternate
    %       definitions are now named "tdiv" and "tmod"
    % NOTE: mod_ has been removed since it is now in prelude.  The additional lemmas
    %       not in prelude are now in mod_lems
    % Version 1.5  product operator theories added
       IMPORTING div,           % integer division
                 rem,           % old version of "rem", prelude version supercedes
                 mod_div_lems,  % modular arithmetic lemmas that involve div
                 mod_lems,      % modular arithmetic lemmas
    	     gcd,           % greatest common divisor
                 gcd_fractions, % division by gcd
    	     tdiv, tmod,    % versions that trunc away from zero for neg arg
                 max_upto,      % max of a set of upto
                 max_below,     % max of a set of below
                 div_nat,       % integer division over nats
                 mod_nat,       % mod over nats
                 abstract_min,  % defines min over type T satisfying P
                 abstract_max,  % defines max over type T satisfying P
    	     min_nat,       % minimum value in a set of naturals
    	     min_posnat,    % minimum value in a set of positive naturals
    	     nat_fun_props, % injective/surgective functions over nats
    	     primes,        % definition of prime numbers
                 factorial,     % factorial function (moved from reals library)
    	     pigeonhole,    % The pigeonhole principle
    %%           Since int is a subtype of reals these are really just special
    %%           cases of the theories in the reals library.  However, there is
    %%           a bug in the PVS judgments system that makes these still useful
    %%           As soon as that bug is fixed, these will be removed.
    	     product,              % generic theory
                 well_nat       % contains an AXIOM that is proved in the orders library
    END top

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