بانيان فكر

حساب نقطه شناور در محاسبات مدرن همه جا وجود دارد ، زيرا ابزاري انتخابي براي تقريبي اعداد واقعي است. به دليل محدوديت و دقت محدود ، استفاده از آن مي تواند كاملاً درگير شود و به طور بالقوه منجر به خرابي هاي بيشماري شود. يكي از راه هاي افزايش اعتماد به نفس در نرم افزارهاي شناور ، تأييد صحت اثبات آن به كمك رايانه است.

اين كتاب نماي كاملي از نحوه تعيين و تأييد رسميت الگوريتم هاي روي شناور با كمك دستيار Coq را ارائه مي دهد. اين رسميت Flocq در محاسبات نقطه شناور و برخي روشها براي خودكار اثبات قضيه را توصيف مي كند. سپس مشخصات و تأييد الگوريتم هاي مختلف ، از تبديل بدون خطا به يك طرح عددي براي يك معادله ديفرانسيل جزئي را ارائه مي دهد. اين مثالها نه تنها الگوريتم هاي رياضي بلكه برنامه هاي C و همچنين مسائل مربوط به تدوين را پوشش مي دهد