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
%------------------------------------------------------------------------
% Formalization of Floating Point numbers in PVS
%
% The hardware level model was developed by Paul Miner (NASA LaRC).
%   P. Miner, Defining the IEEE-854 floating-point standard in PVS,
%   NASA/TM-95-110167, NASA Langley Research Center, 1995.
%   http://techreports.larc.nasa.gov/ltrs/dublincore/1995/NASA-95-tm110167.html
%
% The high level model was developed by Sylvie Boldo (ENS-Lyon) while
% visiting NIA.
%   S. Boldo, Preuves formelles en arithmetiques a virgule flottante,
%   PhD. Thesis, Ecole Normale Superieure de Lyon, 2004.
%   http://www.ens-lyon.fr/LIP/Pub/Rapports/PhD/PhD2004/PhD2004-05.pdf
% This work has been partially funded by
% * NASA LaRC under the Research Cooperative Agreement No. NCC-1-02043
%   awarded to the National Institute of Aerospace
% * French CNRS under PICS 2533
%   awarded to the Laboratoire de l'Informatique du Parallelisme
%
% Users are invited to send feedback information to the authors
% and to [email protected]
%
% Version 1.1    11/30/2005
%
% Note: This library currently links with lnexp (non-foundational).
%       If you want,  you can change this to lnexp_fnd in theory float.
%------------------------------------------------------------------------
BEGIN

  IMPORTING % High-level model (SB)

            float, axpy,

            % Hardware-level (PyM)

            IEEE_854, IEEE_854_defs, infinity_arithmetic,
            comparison1, NaN_ops, arithmetic_ops, IEEE_854_remainder,
            IEEE_854_fp_int, real_to_fp, over_under,
            IEEE_854_values, round, fp_round_aux,
            sum_lemmas, enumerated_type_defs, sum_hack,

            % Equivalence between the two models (SB)

            IEEE_link
END top

¤ Dauer der Verarbeitung: 0.1 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.