Definition 7.2.1. Failure.
A state \(\sigma\models P\) is called a failure with respect to \(p\) and \((P,Q)\) if one of the three cases is true.
unsigned min(unsigned x, unsigned y) {
if (x < y)
return y;
else
return x;
}
unsigned sum_first_n(unsigned *arr, unsigned sz, unsigned n) {
unsigned sum = 0;
n = min(n, sz);
for (unsigned i = 0; i < n; i++)
sum += arr[i];
return sum;
}
Run
sum_first_n
shall sum up the first n
, however at most sz
, elements of the array arr
.”sum_first_n
:int main() {
unsigned arr[] = { 1, 2, 3 };
unsigned r1 = sum_first_n(arr, 3, 2); // (1)
unsigned r2 = sum_first_n(arr, 3, 3); // (2)
unsigned r3 = sum_first_n(arr, 3, 4); // (3)
Run
r1
must be 3, it is however 6.sum_first_n
intends to access the array element arr + 3
which does not exist and therefore the address arr + 3
is not valid. We discussed before 7.2.2 that we cannot make any assumptions on the program's behavior in this case.min
: min
does not compute the minimum but the maximum.NDEBUG
(typically by given the command line switch -DNDEBUG
) asserts can be deactivated by defining the macro assert
to the empty text. This is typically done for production code that has been “sufficiently” tested.#include <assert.h>
unsigned min(unsigned x, unsigned y) {
unsigned m = x < y ? x : y;
assert(m <= x && m <= y && (m == x || m == y));
return m;
}
Run
assert
evaluates the argument expression. If the resulting value is 0, then the execution aborts immediately. Hence, the program aborts very close to the error location.assert(n > 0);
. In debug builds, this assertion is checked during runtime and readers of the code will see that the precondition is that we don't pass empty arrays.unsigned min_arr(unsigned* arr, unsigned n) {
assert(n > 0);
unsigned res = arr[0];
for (unsigned i = 1; i < n; i++)
res = min(res, arr[i]);
return res;
}
Run
min_idx
shall return the index of a smallest elements in an array. Of course, the function is not defined on empty arrays, because they don't have a minimum. The programmer could indicate the error situation by returning \(-1\) or something similar:int min_arr(int* arr, unsigned n) {
if (n == 0)
return -1;
int min = arr[0];
int idx = 0;
for (unsigned i = 1; i < n; i++) {
if (arr[i] < min) {
min = arr[i];
idx = i;
}
}
return idx;
}
Run
min_arr
, the programmer could have checked for the length of the array being greater than \(0\) equally well. There is nothing gained from making min_arr
“work” on all inputs. On the contrary, there is the risk of moving a possible error further away from the failure. Here, it would be best to just start min_arr
with an assertion:int min_arr(int* arr, unsigned n) {
assert (n > 0);
...
}
Run