[prev] [index] [next]

Testing Example #1

Consider some code to test whether an array int A[N] is ordered:

ordered(A[N]):  forall i:1..N-1,  A[i] >= A[i-1]

and print "Yes" if ordered, or print "No" otherwise.

ordered = 1; /* assume that it *is* ordered */
for (i = 1; i < N; i++) {
    if (A[i] > A[i-1])
        /* ok ... still ordered */;
    else
        ordered = 0; /* found counter-example */
}
printf("%s\n", ordered ? "Yes" : "No");

To test this, we need to embed it in a program to set up the array.

We fix the array size (9) and get the values from the command line.