The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

This discussion has gone way out of the scope of the coq-club mailing
list. So I'm moving it to the frama-c list. Please remove the coq-club
CC from further emails. I'm still sending this one to coq-club, so that
the original email doesn't seem unanswered to.

Le lundi 27 septembre 2010 à 11:01 +0200, Michael a écrit :
> No that everything seems to work fine, I have another short question (just 
> to
> make sure it's not a problem of something missing that should actually 
> already
> be there): I included math.h in my C source code, and calculated sqrt of 
> some
> double value, which resulted in the coq proof in a variable of which 
> nothing is
> known. I then had a look at /usr/local/share/frama-c/libc/math.h. For some
> functions (such as acos, asin) there are ACSL-annotations, however there is
> nothing for sqrt.
> 
> Are there
> a) some annotations  on how the C square root behaves anywhere, and I just
> missed them, or
> b) do I have to give specifications on my own, and take them as admitted

I don't think there are any specification for the square root yet, so
you will have to craft your own. I guess something like the following
would work. It is untested both syntactically and from a specification
point of view.

/*@
  behavior normal:
    assumes \is_finite(x) && x >= 0;
    assigns \nothing;
    ensures \is_finite(\result) && \abs(\result - \sqrt(x)) <= 0x1p-53 *
\abs(\sqrt(x));
  behavior infinite:
    assumes \is_plus_infinity(x);
    assigns \nothing;
    ensures \is_plus_infinity(\result);
  behavior edom:
    assumes \is_minus_infinity(x) || (\is_finite(x) && x < 0);
    assigns __FC_errno;
    ensures __FC_errno == 1;
  disjoint behaviors normal, infinite, edom;
 */
double sqrt(double x);

Perhaps someone else can suggest a better specification.

Best regards,

Guillaume

PS: the \abs(\sqrt(x)) expression is a bit overkill but it should make
Gappa happy.