/*@ requires y/2 <= x <= 2*y && \round_error(x)==0 && \round_error(y)==0
@ ensures \round_error(\result)==0
@*/
double Sterbenz(double x, double y) {
return x-y;
}
distrib
>
Fedora
>
13
>
i386
>
media
>
os
>
by-pkgid
>
4a989cf09a4b4c5f3273c280e92c6313
>
files
>
35
