Quelle top.pvs Sprache: 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 Marc.Daumas@ENS-Lyon.Fr
%
% 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

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.