subtype of enumeration type

subtype of enumeration type

[Maciej Sobczak]

Consider this:

    type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);

and the following standard example:

    subtype Weekday is Day range Mon .. Fri;

Now imagine that in some country children don't have to go to school on 
Wednesdays, they go there only Monday, Tuesday, Thursday and Friday.

I want to say it in Ada.

    subtype Schoolday is Day <what goes here?>;


-- 
Maciej Sobczak : http://www.msobczak.com/
Programming    : http://www.msobczak.com/prog/

Re: subtype of enumeration type

[Larry Kilgallen]

In article <dvmas1$kj8$1@sunnews.cern.ch>, Maciej Sobczak <no.spam@no.spam.com> writes:
> Consider this:
> 
>     type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
> 
> and the following standard example:
> 
>     subtype Weekday is Day range Mon .. Fri;
> 
> Now imagine that in some country children don't have to go to school on 
> Wednesdays, they go there only Monday, Tuesday, Thursday and Friday.
> 
> I want to say it in Ada.
> 
>     subtype Schoolday is Day <what goes here?>;

     type Day is (Mon, Tue, Thu, Fri, Wed, Sat, Sun);
     subtype Weekday is Day range Mon .. Wed;
     subtype Schoolday is Day range Mon .. Fri;

Some additional logic may also be in order if you print some
some human-readable output based on an iteration over the range
of Day or Weekday, such as by creating an index array Days_in_Order.

Re: subtype of enumeration type

[Maciej Sobczak]

Larry Kilgallen wrote:

>      type Day is (Mon, Tue, Thu, Fri, Wed, Sat, Sun);
>      subtype Weekday is Day range Mon .. Wed;
>      subtype Schoolday is Day range Mon .. Fri;

First of all, I might need to define the subtypes *after* Day is defined 
and I might not have write access to the module where Day is defined.

Second, let's say that in addition I get the piano lessons all Tuesdays, 
Wednesdays and Thursdays:

    subtype Pianoday is Day <what goes here?>;


> Some additional logic may also be in order if you print some
> some human-readable output based on an iteration

This additional logic would be needed only because you have changed the 
order of elements in the primary type for the purpose of defining the 
subtype, thus introducing the *reverse* source code dependency between 
these types.
In other words, the need for this "additional logic" is exactly the 
indication that this solution is not acceptable.

So - is it at all possible? If yes, how? If not, what is the sense of 
providing these kind of examples even in RM, if the concept simply does 
not work?


-- 
Maciej Sobczak : http://www.msobczak.com/
Programming    : http://www.msobczak.com/prog/

Re: subtype of enumeration type

[Robert A Duff]

Maciej Sobczak <no.spam@no.spam.com> writes:

> Consider this:
> 
>     type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
> 
> and the following standard example:
> 
>     subtype Weekday is Day range Mon .. Fri;
> 
> Now imagine that in some country children don't have to go to school on
> Wednesdays, they go there only Monday, Tuesday, Thursday and Friday.
> 
> I want to say it in Ada.
> 
>     subtype Schoolday is Day <what goes here?>;

You can't do that.

You could put "pragma Assert(Some_Day /= Wednesday)"
all over the place, but that's not quite the same thing.

Eiffel allows arbitrary conditions as invariants,
but Ada has a fairly restricted set of constraints
(ranges for discrete types, a single value for
discriminant constraints, etc).

- Bob

Re: subtype of enumeration type

[Björn Persson]

Maciej Sobczak wrote:
> Consider this:
> 
>    type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
> 
> and the following standard example:
> 
>    subtype Weekday is Day range Mon .. Fri;
> 
> Now imagine that in some country children don't have to go to school on 
> Wednesdays, they go there only Monday, Tuesday, Thursday and Friday.
> 
> I want to say it in Ada.
> 
>    subtype Schoolday is Day <what goes here?>;

I think the best you can do is:

Is_Schoolday : constant array(Day) of Boolean :=
   (True, True, False, True, True, False, False);

-- 
Bj�rn Persson                              PGP key A88682FD
                    omb jor ers @sv ge.
                    r o.b n.p son eri nu

Re: subtype of enumeration type

[Jeffrey R. Carter]

Maciej Sobczak wrote:
> 
>    type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
> 
> and the following standard example:
> 
>    subtype Weekday is Day range Mon .. Fri;
> 
> Now imagine that in some country children don't have to go to school on 
> Wednesdays, they go there only Monday, Tuesday, Thursday and Friday.
> 
> I want to say it in Ada.
> 
>    subtype Schoolday is Day <what goes here?>;

Nothing. You can't do it that way in Ada.

There are a number of options:

1. Use

subtype Schoolday is Weekday;

add a comment that Wed is invalid, check for Wed and raise an exception. Not 
very nice, but adheres to the practice of specifying preconditions and raising 
exceptions when they're violated.

However, using subtypes is cleaner. I much prefer

function F (A : Natural);

to

function F (A : Integer);
--# pre A >= 0;

which is often seen in SPARK.

2. Use a private type:

type Schoolday is private; -- Mon, Tue, Thu, Fri

function Is_Schoolday (Today : Weekday) return Boolean;
-- returns False if Today = Wed; True otherwise

function "+" (Right : Weekday) return Schoolday;
-- pre Right /= Wed; raise Constraint_Error if violated

function "+" (Right : Schoolday) return Weekday;

procedure Op (Today : in Schoolday);

This is similar to the previous example, but the checking only needs to be on 
the conversion function.

3. Use sets of Day; Schoolday is a set with Mon, Tue, Thu, and Fri as members.

4. Use 2 subtypes:

subtype Early_Schoolday is Day range (Mon .. Tue);
subtype Late_Schoolday  is Day range (Thu .. Fri);

What you do will depend on the requirements of your application. In general, 
there is no way to specify Day that will allow subtypes for all possible uses of 
days of the week.

-- 
Jeff Carter
"From this day on, the official language of San Marcos will be Swedish."
Bananas
28

subtypes and preconditions (was: subtype of enumeration type)

[Peter Amey]

Jeff,

Jeffrey R. Carter wrote:
[snip]
> However, using subtypes is cleaner. I much prefer
> 
> function F (A : Natural);
> 
> to
> 
> function F (A : Integer);
> --# pre A >= 0;
> 
> which is often seen in SPARK.
> 

I strongly agree.  Thoughtful use of subtypes is one of the most useful 
things to do in SPARK programs, it greatly assists with exception 
freedom proofs.

I suspect the latter form of your function arises because, many years 
ago, the SPARK Examiner did not carry type information into verification 
conditions.  In those far-off days it wouldn't have known that A was >= 
0 even if the subype Natural was given.  Since about the mid 90s the 
Examiner makes full use of all the information deducible from type and 
subtype ranges.

[snip]

Peter

Re: subtypes and preconditions

[Jeffrey R. Carter]

Peter Amey wrote:
> 
> I strongly agree.  Thoughtful use of subtypes is one of the most useful 
> things to do in SPARK programs, it greatly assists with exception 
> freedom proofs.
> 
> I suspect the latter form of your function arises because, many years 
> ago, the SPARK Examiner did not carry type information into verification 
> conditions.  In those far-off days it wouldn't have known that A was >= 
> 0 even if the subype Natural was given.  Since about the mid 90s the 
> Examiner makes full use of all the information deducible from type and 
> subtype ranges.

Right. The 2 forms are equivalent when doing proofs. Yet I keep seeing examples 
that use preconditions rather than subtypes. For example, Barnes (2003) gives 
the example of Divide (p 70):

procedure Divide (M, N : in Integer; Q, R : out Integer);
--# derives Q, R from M, N;
--# pre (M >= 0) and (N > 0);
--# post (M = Q * N + R) and (R < N) and (R >= 0);

rather than

procedure Divide (Dividend : in  Natural; Divisor   : in  Positive;
                   Quotient : out Natural; Remainder : out Natural);
--# derives Quotient, Remainder from Dividend, Divisor;
--# post Dividend = Quotient * Divisor + Remainder and Remainder < Divisor;

The "R >= 0" in the assertion also becomes unnecessary with appropriate subtypes.

Similarly, he has (pp 77-78)

procedure GCD (M, N : in Integer; G : out Integer);
--# derives G from M, N;
--# pre M >= 0 and N > 0
--# post G > 0 and (M rem G = 0) and (N rem G = 0);

rather than

procedure GCD (M : in Natural; N : in Positive; G : out Positive);
--# derives G from M, N;
--# post M rem G = 0 and N rem G = 0;

-- 
Jeff Carter
"You empty-headed animal-food-trough wiper."
Monty Python & the Holy Grail
04

Re: subtypes and preconditions

[Georg Bauhaus]

Jeffrey R. Carter wrote:

> Yet I keep seeing
> examples that use preconditions rather than subtypes. For example,
> Barnes (2003) gives the example of Divide (p 70):
> 
> procedure Divide (M, N : in Integer; Q, R : out Integer);
> --# derives Q, R from M, N;
> --# pre (M >= 0) and (N > 0);
> --# post (M = Q * N + R) and (R < N) and (R >= 0);
> 
> rather than
> 
> procedure Divide (Dividend : in  Natural; Divisor   : in  Positive;
>                   Quotient : out Natural; Remainder : out Natural);
> --# derives Quotient, Remainder from Dividend, Divisor;
> --# post Dividend = Quotient * Divisor + Remainder and Remainder < Divisor;

WRT  M: Natural  versus  M: Integer >= 0, I think that in an
introductory example to reasoning about SPARK programs it
might in fact be good to leave out Ada subtypes' implications.

The reason is that you needn't know about the niceties of Ada's
subtypes in order to understand that M being >= 0 is important.
IOW, you already know what M >= 0 means, but you do not yet know
what M: Natural implies, unless you already know Ada.

_And_ you have to assume that Natural has not been redefined.
Redifining 0 is a lot more difficult :-)



Georg 

Re: subtypes and preconditions

[Jeffrey R. Carter]

Georg Bauhaus wrote:
> 
> _And_ you have to assume that Natural has not been redefined.
> Redifining 0 is a lot more difficult :-)

You have to assume that Integer has not been redefined, too.

-- 
Jeff Carter
"You empty-headed animal-food-trough wiper."
Monty Python & the Holy Grail
04