Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: top.pvs Sprache: PVS

Original von: PVS^©

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
%
%-------------------------------------------------------------------------
BEGIN
   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
      floor_div_lems,
      floor_more,
      max_below,
      max_bounded_posnat,
             max_finite_set_nat,
      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
      product_below,
      product_int,
      product_nat,
      product_posnat,
      product_upto,

             well_nat       % contains an AXIOM that is proved in the orders library

END top

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.