source: CIVL/examples/languageFeatures/quantifiers.cvl@ 7acd15d

/* Commandline execution:
 *              civl verify quantifiers.cvl
 * */
#include<civlc.cvh>

$input double b[10];

void main() {
  int a[5];
  
  for (int i = 0; i < 5; i++) {
    a[i] = i;
  }

  $assert($forall {int i | i >= 0 && i < 5} a[i] >= 0);
  $assert($exists {int k | k >= 0 && k < 5} a[k] > 3);
  $assert($exists {k = 0 .. 4} a[k] > 3);
  $assume($forall {int j | j >= 0 && j < 10} b[j] >= 2);
  $assert($forall {int m | m >= 3 && m <= 5} b[m] > 1);
}