* subtype of enumeration type
@ 2006-03-20 13:31 Maciej Sobczak
2006-03-20 14:26 ` Larry Kilgallen
` (3 more replies)
0 siblings, 4 replies; 10+ messages in thread
From: Maciej Sobczak @ 2006-03-20 13:31 UTC (permalink / raw)
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/
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: subtype of enumeration type
2006-03-20 13:31 subtype of enumeration type Maciej Sobczak
@ 2006-03-20 14:26 ` Larry Kilgallen
2006-03-20 15:18 ` Maciej Sobczak
2006-03-20 15:37 ` Robert A Duff
` (2 subsequent siblings)
3 siblings, 1 reply; 10+ messages in thread
From: Larry Kilgallen @ 2006-03-20 14:26 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: subtype of enumeration type
2006-03-20 14:26 ` Larry Kilgallen
@ 2006-03-20 15:18 ` Maciej Sobczak
0 siblings, 0 replies; 10+ messages in thread
From: Maciej Sobczak @ 2006-03-20 15:18 UTC (permalink / raw)
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/
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: subtype of enumeration type
2006-03-20 13:31 subtype of enumeration type Maciej Sobczak
2006-03-20 14:26 ` Larry Kilgallen
@ 2006-03-20 15:37 ` Robert A Duff
2006-03-20 20:29 ` Björn Persson
2006-03-20 21:41 ` Jeffrey R. Carter
3 siblings, 0 replies; 10+ messages in thread
From: Robert A Duff @ 2006-03-20 15:37 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: subtype of enumeration type
2006-03-20 13:31 subtype of enumeration type Maciej Sobczak
2006-03-20 14:26 ` Larry Kilgallen
2006-03-20 15:37 ` Robert A Duff
@ 2006-03-20 20:29 ` Björn Persson
2006-03-20 21:41 ` Jeffrey R. Carter
3 siblings, 0 replies; 10+ messages in thread
From: Björn Persson @ 2006-03-20 20:29 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: subtype of enumeration type
2006-03-20 13:31 subtype of enumeration type Maciej Sobczak
` (2 preceding siblings ...)
2006-03-20 20:29 ` Björn Persson
@ 2006-03-20 21:41 ` Jeffrey R. Carter
2006-03-21 8:37 ` subtypes and preconditions (was: subtype of enumeration type) Peter Amey
3 siblings, 1 reply; 10+ messages in thread
From: Jeffrey R. Carter @ 2006-03-20 21:41 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 10+ messages in thread
* subtypes and preconditions (was: subtype of enumeration type)
2006-03-20 21:41 ` Jeffrey R. Carter
@ 2006-03-21 8:37 ` Peter Amey
2006-03-21 17:42 ` subtypes and preconditions Jeffrey R. Carter
0 siblings, 1 reply; 10+ messages in thread
From: Peter Amey @ 2006-03-21 8:37 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: subtypes and preconditions
2006-03-21 8:37 ` subtypes and preconditions (was: subtype of enumeration type) Peter Amey
@ 2006-03-21 17:42 ` Jeffrey R. Carter
2006-03-21 19:00 ` Georg Bauhaus
0 siblings, 1 reply; 10+ messages in thread
From: Jeffrey R. Carter @ 2006-03-21 17:42 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: subtypes and preconditions
2006-03-21 17:42 ` subtypes and preconditions Jeffrey R. Carter
@ 2006-03-21 19:00 ` Georg Bauhaus
2006-03-22 1:54 ` Jeffrey R. Carter
0 siblings, 1 reply; 10+ messages in thread
From: Georg Bauhaus @ 2006-03-21 19:00 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: subtypes and preconditions
2006-03-21 19:00 ` Georg Bauhaus
@ 2006-03-22 1:54 ` Jeffrey R. Carter
0 siblings, 0 replies; 10+ messages in thread
From: Jeffrey R. Carter @ 2006-03-22 1:54 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 10+ messages in thread
end of thread, other threads:[~2006-03-22 1:54 UTC | newest]
Thread overview: 10+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2006-03-20 13:31 subtype of enumeration type Maciej Sobczak
2006-03-20 14:26 ` Larry Kilgallen
2006-03-20 15:18 ` Maciej Sobczak
2006-03-20 15:37 ` Robert A Duff
2006-03-20 20:29 ` Björn Persson
2006-03-20 21:41 ` Jeffrey R. Carter
2006-03-21 8:37 ` subtypes and preconditions (was: subtype of enumeration type) Peter Amey
2006-03-21 17:42 ` subtypes and preconditions Jeffrey R. Carter
2006-03-21 19:00 ` Georg Bauhaus
2006-03-22 1:54 ` Jeffrey R. Carter
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox