Using constrained types in C
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 eCv’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, eCv 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\ecvtest\ecvtest7.c (13,23): Error! Refuted: Type constraint satisfied (defined at c:\escher\ecvtest\ecvtest7.c (9,39)), cannot prove: 200 <= 100. c:\escher\ecvtest\ecvtest7.c (14,16): Warning! Unable to prove: Type constraint for ‘Percentage’ satisfied, suggestion available (see c:\escher\ecvtest\ecvtest7_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.