Using constrained types in C

February 26, 2010

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.

  1. Matt Banham
    March 11, 2010 at 18:00

    Nice post – but I have to say (as a SPARKateer) the Ada looks neater to me!

    • March 11, 2010 at 18:14

      I don’t disagree that Ada is a better language than C to start from when it comes to defining verifiable language subsets for critical systems. If you’re into SPARK, you might be interested in our product Perfect Developer, which is currently being used in the defence industry to specify and model a SIL 4 software system prior to coding in SPARK. The client used to model in Z, but found PD more productive because of the automatic proof and ease of use. We’re in the process of adding SPARK code generation to PD to make this combination even easier to use.

  1. June 7, 2010 at 16:44
  2. June 22, 2010 at 11:23
Comments are closed.
<span>%d</span> bloggers like this: