/* Commandline execution:
 *		civl verify -inputnum_elements=5 derivative.cvl
 * */
#include<civlc.h>
#include<stdio.h>

$input double h;
$input int num_elements;
$input double initial[num_elements];
double working[num_elements];
$abstract $contin(2) $real rho($real x);
$assume h > 0;

void differentiate(double h, int n, double y[], double result[]){
	int i;
	
	$assume $forall {m=0 .. n-1} y[m] == rho(m*h);
	for(i = 1; i < n; i++)
	{
		result[i] = (y[i]-y[i-1])/h;
	}
	// forward at endpoint
	result[0] = (y[1] - y[0])/h;
	$assert($uniform {k=0 .. n-1} result[k]-$D[rho,{x,1}](k*h) == $O(h));
}

void main() {
	differentiate(h, num_elements, initial, working);
}