source: CIVL/examples/arithmetic/mean.cvl@ 6a4e2e0

$input int N_BOUND;
#pragma TASS input {N>0 && N<=N_BOUND} 
$input int N;
#pragma TASS input 
double a[N];
#pragma TASS output 
double s;

void main() {
        int i=0;
        double x=0.0;
        
        $assume 
#pragma TASS joint invariant LOOP true;
        while (i < N) {
                x = x + a[i];
                i = i + 1;
        }
        s = x/N;
}