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.14 Sekunden
(vorverarbeitet)
¤
|
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.
|
