/* Discrete derivative function using backwards differencing, which is first-order
 * accurate.  To verify with CIVL, type:
 *		civl verify derivative.cvl
 */

$input double dx;
$assume(0<dx && dx<1);
$input int num_elements;
$assume(num_elements >= 1);
$input double in[num_elements];
double out[num_elements];
// the following says rho is a function from R to R which has 2 continuous
// derivatives in the closed interval [-1,1]:
$abstract $differentiable(2, [-1,1]) $real rho($real x);

void differentiate(int n, double y[], double h, double result[]) {
  $assume(n*h<=1);
  $assume($forall (int i : 0..n-1) y[i] == rho(i*h));
  /*@ loop invariant 1<=i && i<=n;
    @ loop invariant $forall (int j : 1..i-1) result[j] == (y[j]-y[j-1])/h;
    @ loop assigns i, result[1..n-1];
    @*/
  for (int i=1; i<n; i++) {
    result[i] = (y[i] - y[i-1])/h;
  }
  result[0] = (y[1] - y[0])/h; // forward differencing used at left end-point
  $assert($uniform (int i=0..n-1) result[i]-$D[rho,{x,1}](i*h) == $O(h));
}

int main() {
  differentiate(num_elements, in, dx, out);
}