source: CIVL/mods/dev.civl.com/examples/experimental/count.cvl@ cb4d4f4

#include<civlc.cvh>

$input int n;
$output int s = 0;

void main() {
  $assume(n>0);
  for (int i=0; i<n; i++) $invariant (i<=n) {
    s += i;
  }
}