| Formal verification of numerical subroutines
[center]Write algorithm from e_log2.c in Gappa and Coq[/center] I rewrote a part of algorithm from FDLIBM e_log2.c in Gappa ------------------ url: log1.g @rnd = float< ieee_64, ne >; x = rnd(x_); . . .
|
Java library for interval computations
» General Discussion
|
March 13, 2010 05:16
by: Dmitry Nadezhin
|
| Formal verification of numerical subroutines
[center]Verification of double StrictMath.log(double x)[/center] I choose the static method java.lang.StrictMath.log(double x) as an object of verification. JDK contains two classes for computation o . . .
|
Java library for interval computations
» General Discussion
|
March 13, 2010 05:16
by: Dmitry Nadezhin
|
| Formal verification of numerical subroutines
[center]Разглядываю доказательство e0.v в Coq[/center] Посмотрю, что Gappa подготовила для Coq. Простая вещь - интервальное о . . .
|
Java library for interval computations
» General Discussion
|
March 13, 2010 05:16
by: Dmitry Nadezhin
|
| Formal verification of numerical subroutines
[center]Разглядываю Coq-файл, сгенерированный Gappa'ой[/center] Gappa находит доказательство некоторых фактов о вычислени . . .
|
Java library for interval computations
» General Discussion
|
March 13, 2010 05:16
by: Dmitry Nadezhin
|
| Formal verification of numerical subroutines
[center]com.kenai.jinterval.stdfun.RealStdFun[/center] Интервальные оценки e и π, полученные в предудущем посте, позволют узнать, что а . . .
|
Java library for interval computations
» General Discussion
|
March 13, 2010 05:16
by: Dmitry Nadezhin
|
| Formal verification of numerical subroutines
[center]Пробую Gappa для оценки констант[/center] В файле java.lang.Math определены double константы E и PI, являющиеся аппроксима . . .
|
Java library for interval computations
» General Discussion
|
March 13, 2010 05:16
by: Dmitry Nadezhin
|
| Formal verification of numerical subroutines
[center]Выбор проверяльщика доказательств[/center] Я выбрал url: Coq , потому что он был разработан в INRIA, а там я нашел ещ . . .
|
Java library for interval computations
» General Discussion
|
March 13, 2010 05:16
by: Dmitry Nadezhin
|
| Formal verification of numerical subroutines
На этом топике я буду рассказывать о моих попытках формальной верификации некоторых подпрограмм из различны . . .
|
Java library for interval computations
» General Discussion
|
March 13, 2010 05:16
by: Dmitry Nadezhin
|
| UTF-8 X Kenai mailing lists
Hi John, Here is another example of mailing list with Russian text: I sent a messages in Russian in (I believe )UTF-8 to mail-list@jinterval.kenai.com . The mail list resend this message back to me a . . .
|
Project Kenai Documentation and Training
» UI
|
May 11, 2011 01:20
by: dengdai
|
| Архитектура
Я рад, что диалог возобновляется. : Цель нашего проекта ("и вообще не зная конечной цели") указана в его полном . . .
|
Java library for interval computations
» General Discussion
|
October 04, 2009 05:37
by: Egor Tepikin
|
