Next: , Previous: GDB.h, Up: Interface


4.10 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.1

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 you're 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 work 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.2

            /* 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);

Footnotes

[1] ANSI C does not allow variable declarations at the beginning of loops unlike C++. The ‘Q.h’ macros get around this by starting each loop with a new scope.

[2] This uses yet another GNU CC extension, however since we are already using statement expressions we might as well use ‘typeof’ as well.