| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/float/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
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 ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28