Q.h: support for quantifiers

`Q.h' provides support for the quantifiers of predicate logic. For example to check that all elements in a data structure have some property we would use universal (forall, upside down A) quantification. To check that one or more values in a data structure have some property we would use existential (exists, back the front E) quantification. For example:

  /* all values in a[] must be between 0 and 10 */
  I(A(int i = 0, i < n_array, i++, 0 <= a[i] && a[i] <= 10));

  /* there exists a value in linked list l which is smaller than 10 */
  I(E(node *p = l, p != NULL, p = p->next, p->data <= 10));

The first three arguments to `A' and `E' are similar to a C `for' loop which iterates over the values we wish to check. The final argument is the expression that must be true.

The only minor difference from the C `for' loop is that variables may be declared at the start of the loop, even if you are using C rather than C++ which already supports this.(8)

The `Q.h' macros can also be nested and used anywhere a boolean value is required. For example:

  if(A(int i = 0, i < MAXX, i++,
       A(int j = 0, j < MAXY, j++,
         m[i][j] == (i == j ? 1 : 0)))) { 
        /* identity matrix, i.e. all 0's except for 1's on */
        /* the diagonal */
        ...
  } else {
        /* not an identity matrix */
        ...
  }

The results from these macros can also be combined using boolean operations, e.g.

  /* the values in a[i]  are either ALL positive or ALL negative */
  I(A(int i = 0, i < MAX, i++, a[i] >= 0)
    ||
    A(int i = 0, i < MAX, i++, a[i] < 0));

Portability: note the macros in this file require the GNU CC/C++ statement expression extension of GCC to work. If your not using GNU CC then for now you are out of luck. At some time in the future we may implement a method which will work for standard C++, standard C is a bit of a challenge.

Portability: unfortunately these macros do not for the `DI' and `DL' macros since the statement expression extension has not been implemented in GDB.

Macro: bool A (init,condition,next,exprn)

For all values generated by `for(int;condition;next)' the exprn must be true.

  I(A(int i = 0, i < MAX, i++, a[i] >= 0)); /* all a[i] are +ve */

Macro: bool E (init,condition,next,exprn)

There exists at least one value for exprn generated by `for (int;condition;next)' which is true.

  /* one or more a[i] >= 0 */
  I(E(int i = 0, i < MAX, i++, a[i] >= 0));

Macro: long C (init,condition,next,exprn)

Returns the number of times the exprn is true over the values generated by `for(int;condition;next)'.

  /* 3 elements of a[] are +ve */
  I(C(int i = 0, i < MAX, i++, a[i] >= 0) == 3); 

Macro: bool E1 (init,condition,next,exprn)

There exists only one value generated by `for(int;condition;next)' for which the exprn is true.

  /* a single elements of a[] is +ve */
  I(E1(int i = 0, i < MAX, i++, a[i] >= 0)); 

Macro: typeof(exprn) S (init,condition,next,exprn)

Sum the values generated by exprn for all values given by `for(int;condition;next)'. The type of the value returned is given by the type of the exprn.(9)

  /* sum of a[] is 10 */
  I(S(int i = 0, i < MAX, i++, a[i]) == 10);

  /* sum of all +ve numbers in a[] is 10 */
  I(S(int i = 0, i < MAX, i++, a[i] >= 0 ? a[i] : 0) == 10);

Macro: typeof(exprn) P (init,condition,next,exprn)

Returns the product of the values generated by exprn for all values given by `for(int;condition;next)'. The type returned is the type of the expression.

  /* product of all the values in a[] is 10 */
  I(P(int i = 0, i < MAX, i++, a[i]) == 10); 

  /* a = x^y i.e. x*x..*x y times */
  I(P(int i = 0, i < y, i++, x) == a);

Go to the first, previous, next, last section, table of contents.