## Linear recurrence of order 2

This very simple code from numerical analysis that is a linear recurrence of order 2.

Auteurs: Sylvie Boldo

Catégories: Floating-Point Computations / Mathematics

Outils: Frama-C / Jessie / Coq

see also the index (by topic, by tool, by reference, by year)

A reasonable bound on the rounding error requires a complex property that expresses each rounding error.
```/*@ axiomatic MKP {
@  predicate mkp(double uc, double up, integer n);
@ } */

/*@ requires 2 <= N <= \pow(2,26) &&
@      \exact(u0)==u0 && \exact(u1)==u1 &&
@      \forall integer k; 0 <= k <= N ==>  \abs(u0+k*(u1-u0)) <= 1;
@ ensures  \exact(\result)==u0+N*(u1-u0) &&
@          \round_error(\result) <= N*(N+1.)/2.*\pow(2,-53);
@*/

double comput_seq(double u0, double u1, int N) {
int i;
double uprev, ucur,tmp;
uprev=u0;
ucur=u1;

/*@ loop invariant 2 <= i && i <= N+1 &&
@   \exact(ucur) ==u0+(i-1)*(u1-u0) &&
@   \exact(uprev)==u0+(i-2)*(u1-u0) &&
@   mkp(ucur,uprev,i-2);
@ loop variant N-i; */
for (i=2; i<=N; i++) {
tmp=2*ucur;
/*@ assert tmp==2.*ucur; */
tmp-=uprev;
uprev=ucur;
ucur=tmp;
}
return ucur;
}
```