David Crocker's Verification Blog

When writing critical software, one of the advantages cited for using Ada rather than C is that Ada lets you define constrained types, like this:

type Percentage is Integer range 0 .. 100;

The Ada compiler inserts a run-time check whenever the program assigns a value to a variable of type Percentage that might be less than 0 or greater than 100, and in other similar situations such as when passing parameters.

C doesn’t support constrained types. Fortunately, there are ways round this. One is to use ArC’s constrained typedef syntax:

typedef int invariant(0 <= value; value <= 100) Percentage;

We met the invariant macro in an earlier post – it expands to nothing when your program is compiled, making the constraint invisible to a regular C or C++ compiler. So you won’t get run-time checking of the constraint. However, ArC will try to prove that the constraint is obeyed. For example, the following function:

void foo(bool b, Percentage *score) {
if (b) { *score = 200; }
else { *score += 1; }
}

gives rise to these verification errors:

c:\escher\arctest\arctest7.c (13,23): Error! Refuted: Type constraint satisfied (defined at c:\escher\arctest\arctest7.c (9,39)), cannot prove: 200 <= 100.

c:\escher\arctest\arctest7.c (14,16): Warning! Unable to prove: Type constraint for ‘Percentage’ satisfied, suggestion available (see C:\Escher\ArcTest\arctest7_unproven.htm#1), cannot prove: (1 + *score) <= 100.

and if you follow the suggestion link in the second message, it suggests a suitable function precondition.

If you want run-time checking of constraints, then the best way is to use a C++ class:

class Percentage {
int value;

public:
Percentage(int arg) : value(arg) {
if (arg < 0 || arg > 100) { ... }
}

Percentage& operator = (int arg) {
if (arg < 0 || arg > 100) { ... }
value = arg;
}

operator int() const { return value; }
}

I’ve made Percentage type-compatible with int, but ensured that any attempt to assign or convert an int to a Percentage is subject to a range check (replace “...” with whatever you want to do when a range check fails).

If your C++ compiler supports templates, then you can define a class template with selectable minimum and maximum values. This makes it trivial to introduce new types like Percentage with a simple typedef.