Checking (Was: Re: New Book: CONCURRENCY)

[Ruth Ivimey-Cook <ruthc@xxxxxxxxxxxxxxxxxx>]

At 10:00 22/04/99 +0100, Jeremy Martin wrote:
>* This leads us to the point that Bryan made about state-space
>  explosion. A single input of an INT32 variable in an Occam process
>  would give rise to at least 2^32 states in the equivalent state
>  transition system, so we need to apply some sort abstraction
>  to reduce the number of states in each constitutent process.

I rather like the facility available in some languages, such as Ada,
Pascal), for both specifying limited-range datatypes and for enumerating
them. Things such as:

  integer i is (10-20)

or

  var i is (green => 2, blue => 4, red => 6)

I rather like the syntax Roger and Barry have used in their hardware
compiler, and it would allow at least the first of these; it's not hard to
imagine ways of including the second too.

One benefit of both would be that typical programs stop using loads of
int32's or int16's, and start using int3's or uint21's. Although at the
level of program checking, an int21 is still an awful lot of states, it is
still very many less than an int32.

I believe occam should include these things, both because it allows the
colpiler to check even more of the program at compile time, and because it
avoids some of the need for VAL x IS y: type declarations, and because if
we are (as I hope) moving towards formal checking of real programs this is
a good thing from that point of view too.

Regards,

Ruth