comp.lang.ada
 help / color / mirror / Atom feed
* When a conditional expression is static, where can it be used?
@ 2010-06-30 10:39 Georg Bauhaus
  2010-06-30 11:25 ` Pascal Obry
  2010-06-30 14:39 ` Adam Beneschan
  0 siblings, 2 replies; 11+ messages in thread
From: Georg Bauhaus @ 2010-06-30 10:39 UTC (permalink / raw)


A totally meaningless example just to illustrate
the question:  What is it that a compiler must report
for the case statement below, if anything?

procedure CE is

   type DOW is (Mo, Tu, We, Th, Fr, Sa, So);

   procedure P is begin null; end P;

   D: constant DOW := We;
begin
   case D is
      when Mo | We | Fr => P;
      when (if D = We or D = Fr then So else Sa) => P;
      when Tu | Th  => P;
   end case;
end CE;



Georg



^ permalink raw reply	[flat|nested] 11+ messages in thread

* Re: When a conditional expression is static, where can it be used?
  2010-06-30 10:39 When a conditional expression is static, where can it be used? Georg Bauhaus
@ 2010-06-30 11:25 ` Pascal Obry
  2010-06-30 14:39 ` Adam Beneschan
  1 sibling, 0 replies; 11+ messages in thread
From: Pascal Obry @ 2010-06-30 11:25 UTC (permalink / raw)


Le 30/06/2010 12:39, Georg Bauhaus a �crit :
> procedure CE is
> 
>    type DOW is (Mo, Tu, We, Th, Fr, Sa, So);
> 
>    procedure P is begin null; end P;
> 
>    D: constant DOW := We;
> begin
>    case D is
>       when Mo | We | Fr => P;
>       when (if D = We or D = Fr then So else Sa) => P;
>       when Tu | Th  => P;
>    end case;
> end CE;

This should not compile I would say.

Pascal.
-- 

--|------------------------------------------------------
--| Pascal Obry                           Team-Ada Member
--| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE
--|------------------------------------------------------
--|    http://www.obry.net  -  http://v2p.fr.eu.org
--| "The best way to travel is by means of imagination"
--|
--| gpg --keyserver keys.gnupg.net --recv-key F949BD3B




^ permalink raw reply	[flat|nested] 11+ messages in thread

* Re: When a conditional expression is static, where can it be used?
  2010-06-30 10:39 When a conditional expression is static, where can it be used? Georg Bauhaus
  2010-06-30 11:25 ` Pascal Obry
@ 2010-06-30 14:39 ` Adam Beneschan
  2010-06-30 17:35   ` Dmitry A. Kazakov
  1 sibling, 1 reply; 11+ messages in thread
From: Adam Beneschan @ 2010-06-30 14:39 UTC (permalink / raw)


On Jun 30, 3:39 am, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
wrote:
> A totally meaningless example just to illustrate
> the question:  What is it that a compiler must report
> for the case statement below, if anything?

The choice "Sa" is not covered by any alternative.  Other than that, I
don't think there's anything wrong with the CASE statement, and if you
had included a "when others =>" alternative I think it would be
legal.  I'm not sure what potential problem you were trying to
illustrate.

                   -- Adam

>
> procedure CE is
>
>    type DOW is (Mo, Tu, We, Th, Fr, Sa, So);
>
>    procedure P is begin null; end P;
>
>    D: constant DOW := We;
> begin
>    case D is
>       when Mo | We | Fr => P;
>       when (if D = We or D = Fr then So else Sa) => P;
>       when Tu | Th  => P;
>    end case;
> end CE;
>
> Georg




^ permalink raw reply	[flat|nested] 11+ messages in thread

* Re: When a conditional expression is static, where can it be used?
  2010-06-30 14:39 ` Adam Beneschan
@ 2010-06-30 17:35   ` Dmitry A. Kazakov
  2010-06-30 19:12     ` Adam Beneschan
  2010-06-30 20:05     ` Georg Bauhaus
  0 siblings, 2 replies; 11+ messages in thread
From: Dmitry A. Kazakov @ 2010-06-30 17:35 UTC (permalink / raw)


On Wed, 30 Jun 2010 07:39:24 -0700 (PDT), Adam Beneschan wrote:

> On Jun 30, 3:39�am, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
> wrote:
>> A totally meaningless example just to illustrate
>> the question: �What is it that a compiler must report
>> for the case statement below, if anything?
> 
> The choice "Sa" is not covered by any alternative.  Other than that, I
> don't think there's anything wrong with the CASE statement, and if you
> had included a "when others =>" alternative I think it would be
> legal.  I'm not sure what potential problem you were trying to
> illustrate.

Let me propose this one instead: 

 � �type DOW is (Mo, Tu, We, Th, Fr, Sa, So);

 � �case D is
 � � � when (if D = Mo then Tu else Mo) => P;
 � � � when (if D = Tu then Tu else Mo) => Q;
 � � � when We..So => R;
 � �end case;

The above is equivalent to:

 � �case D is
 � � � when Tu => P;
 � � � when Mo => Q;
 � � � when We..So => R;
 � �end case;

But as Pascal suggested, it should not compile because D is not static. 

As for the problem Georg had in mid. Maybe it is this. Let you have some
function, say Gamma function. Now,

   x : constant := 0.1;
   Gx : constant := Gamma (1.1); -- Illegal, what a pity

Let us open the table of Gamma, scan it, and write something like:

   (if x < 0.0 then ... elsif x < 0.01 then ... )

This wonderful static function can then copied and pasted everywhere you
wanted to evaluate Gamma at compile time. Is it legal?

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



^ permalink raw reply	[flat|nested] 11+ messages in thread

* Re: When a conditional expression is static, where can it be used?
  2010-06-30 17:35   ` Dmitry A. Kazakov
@ 2010-06-30 19:12     ` Adam Beneschan
  2010-06-30 20:00       ` Dmitry A. Kazakov
  2010-07-01 17:04       ` Pascal Obry
  2010-06-30 20:05     ` Georg Bauhaus
  1 sibling, 2 replies; 11+ messages in thread
From: Adam Beneschan @ 2010-06-30 19:12 UTC (permalink / raw)


On Jun 30, 10:35 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> On Wed, 30 Jun 2010 07:39:24 -0700 (PDT), Adam Beneschan wrote:
> > On Jun 30, 3:39 am, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
> > wrote:
> >> A totally meaningless example just to illustrate
> >> the question: What is it that a compiler must report
> >> for the case statement below, if anything?
>
> > The choice "Sa" is not covered by any alternative.  Other than that, I
> > don't think there's anything wrong with the CASE statement, and if you
> > had included a "when others =>" alternative I think it would be
> > legal.  I'm not sure what potential problem you were trying to
> > illustrate.
>
> Let me propose this one instead:
>
>   type DOW is (Mo, Tu, We, Th, Fr, Sa, So);
>
>   case D is
>   when (if D = Mo then Tu else Mo) => P;
>   when (if D = Tu then Tu else Mo) => Q;
>   when We..So => R;
>   end case;
>
> The above is equivalent to:
>
>   case D is
>   when Tu => P;
>   when Mo => Q;
>   when We..So => R;
>   end case;
>
> But as Pascal suggested, it should not compile because D is not static.

Ummm, not quite, because (1) Pascal didn't say anything about *why* he
thought it shouldn't compile (his entire statement was "This should
not compile I would say"), and (2) in the OP's original example, D
*is* static.  In your example, you're right that it shouldn't compile
because D is not static, but that's a different issue.  (Well, I
*assume* D isn't static.  Since your example doesn't include a
declaration of D, I can't tell.)


> As for the problem Georg had in mid. Maybe it is this. Let you have some
> function, say Gamma function. Now,
>
>    x : constant := 0.1;
>    Gx : constant := Gamma (1.1); -- Illegal, what a pity
>
> Let us open the table of Gamma, scan it, and write something like:
>
>    (if x < 0.0 then ... elsif x < 0.01 then ... )
>
> This wonderful static function can then copied and pasted everywhere you
> wanted to evaluate Gamma at compile time. Is it legal?

Gamma cannot be a static function (4.9(18-22)).  You cannot write a
static function (other than an enumeration literal, which is
technically a static function).

                           -- Adam




^ permalink raw reply	[flat|nested] 11+ messages in thread

* Re: When a conditional expression is static, where can it be used?
  2010-06-30 19:12     ` Adam Beneschan
@ 2010-06-30 20:00       ` Dmitry A. Kazakov
  2010-06-30 20:16         ` Adam Beneschan
  2010-07-01 17:04       ` Pascal Obry
  1 sibling, 1 reply; 11+ messages in thread
From: Dmitry A. Kazakov @ 2010-06-30 20:00 UTC (permalink / raw)


On Wed, 30 Jun 2010 12:12:17 -0700 (PDT), Adam Beneschan wrote:

> On Jun 30, 10:35�am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> On Wed, 30 Jun 2010 07:39:24 -0700 (PDT), Adam Beneschan wrote:
>>> On Jun 30, 3:39 am, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
>>> wrote:
>>>> A totally meaningless example just to illustrate
>>>> the question: What is it that a compiler must report
>>>> for the case statement below, if anything?
>>
>>> The choice "Sa" is not covered by any alternative. �Other than that, I
>>> don't think there's anything wrong with the CASE statement, and if you
>>> had included a "when others =>" alternative I think it would be
>>> legal. �I'm not sure what potential problem you were trying to
>>> illustrate.
>>
>> Let me propose this one instead:
>>
>> � type DOW is (Mo, Tu, We, Th, Fr, Sa, So);
>>
>> � case D is
>> � when (if D = Mo then Tu else Mo) => P;
>> � when (if D = Tu then Tu else Mo) => Q;
>> � when We..So => R;
>> � end case;
>>
>> The above is equivalent to:
>>
>> � case D is
>> � when Tu => P;
>> � when Mo => Q;
>> � when We..So => R;
>> � end case;
>>
>> But as Pascal suggested, it should not compile because D is not static.
> 
> Ummm, not quite, because (1) Pascal didn't say anything about *why* he
> thought it shouldn't compile (his entire statement was "This should
> not compile I would say"), and (2) in the OP's original example, D
> *is* static.  In your example, you're right that it shouldn't compile
> because D is not static, but that's a different issue.  (Well, I
> *assume* D isn't static.  Since your example doesn't include a
> declaration of D, I can't tell.)

So, if D is static, then all choices are defined and do not overlap, hence
it must compile. Right?

>> As for the problem Georg had in mid. Maybe it is this. Let you have some
>> function, say Gamma function. Now,
>>
>> � �x : constant := 0.1;
>> � �Gx : constant := Gamma (1.1); -- Illegal, what a pity
>>
>> Let us open the table of Gamma, scan it, and write something like:
>>
>> � �(if x < 0.0 then ... elsif x < 0.01 then ... )
>>
>> This wonderful static function can then copied and pasted everywhere you
>> wanted to evaluate Gamma at compile time. Is it legal?
> 
> Gamma cannot be a static function (4.9(18-22)).  You cannot write a
> static function (other than an enumeration literal, which is
> technically a static function).

Now I do not understand you. The expression I gave is an if-operator with
only constants in it. I presume it is static. E.g., simplified:

 � �x : constant := 2.0;
 � �Gx : constant := (if x <= 1.0 then 1.0 elsif x <= 2.0 then 2.0 elsif x
<= 6.0 then 9.0 else 24.0);

We could even add linear or quadratic interpolation between the points.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



^ permalink raw reply	[flat|nested] 11+ messages in thread

* Re: When a conditional expression is static, where can it be used?
  2010-06-30 17:35   ` Dmitry A. Kazakov
  2010-06-30 19:12     ` Adam Beneschan
@ 2010-06-30 20:05     ` Georg Bauhaus
  2010-06-30 20:29       ` Adam Beneschan
  2010-06-30 20:45       ` Dmitry A. Kazakov
  1 sibling, 2 replies; 11+ messages in thread
From: Georg Bauhaus @ 2010-06-30 20:05 UTC (permalink / raw)


On 30.06.10 19:35, Dmitry A. Kazakov wrote:
> On Wed, 30 Jun 2010 07:39:24 -0700 (PDT), Adam Beneschan wrote:
> 
>> On Jun 30, 3:39 am, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
>> wrote:
>>> A totally meaningless example just to illustrate
>>> the question:  What is it that a compiler must report
>>> for the case statement below, if anything?
>>
>> The choice "Sa" is not covered by any alternative.  Other than that, I
>> don't think there's anything wrong with the CASE statement, and if you
>> had included a "when others =>" alternative I think it would be
>> legal.  I'm not sure what potential problem you were trying to
>> illustrate.

The questions I had asked myself (a little too quick, I suppose)
were along these lines:

Is it possible to invalidate a case construct by simply
changing the value of a static constant used in determining
conditional static case values?  Yes, it is possible even without
conditional expressions, but do these introduce failures that
are much more tricky to straighten out?

If parts of the language will have new (static) possibilities,
what modes of (careful) thinking will these necessitate?

In the case of a case statement, programmers using a static
conditional expression in a case_statement_alternative will be
executing a forward-branching compile time program *and*
need to be backtracking in order to see how other branches of
the case statements will be affected, depending on the
conditional.

The complication is one of the issues that mattered to me,
kind of "second order evaluation" in the programmer's
head (the first order being simple perception of
unconditional values).  It feels a bit like recursive macro
expansion.

All this about static conditional expressions in case_statement_alternative
is probably a somewhat artificial argument, since a conditional
expression in such a place is something Ada programmers will
just not write.  Right?


> Let me propose this one instead: 
> 
>     type DOW is (Mo, Tu, We, Th, Fr, Sa, So);
> 
>     case D is
>        when (if D = Mo then Tu else Mo) => P;
>        when (if D = Tu then Tu else Mo) => Q;
>        when We..So => R;
>     end case;

D: constant DOW := We;
case D is  -- replace D with {We}
   when (if {We} = Mo then Tu else Mo) => P;  -- Mo
   when (if {We} = Tu then Tu else Mo) => Q;  -- Mo
   when We .. So = => R;  -- I should have written Su, sorry
end case;

Tu is not covered, then, is it?  If so, then something else
is equivalent:
> The above is equivalent to:
> 
>     case D is
>        when Tu => P;
>        when Mo => Q;
>        when We..So => R;
>     end case;
> 
> But as Pascal suggested, it should not compile because D is not static. 

I think D is static. D is a constant initialized by a static
function (an enumeration value).


> This wonderful static function can then copied and pasted everywhere you
> wanted to evaluate Gamma at compile time. Is it legal?

Should we have "bigger" static functions?

The 'Constraint or invariant things being worked out for subtypes
are, I guess, potentially static.  How far can one push the
compiler *and* the programmer computing or specifying conditional
expressions, resp.?
(And not have one's head spin too much, or introduce programs
that surprise when changed?)




^ permalink raw reply	[flat|nested] 11+ messages in thread

* Re: When a conditional expression is static, where can it be used?
  2010-06-30 20:00       ` Dmitry A. Kazakov
@ 2010-06-30 20:16         ` Adam Beneschan
  0 siblings, 0 replies; 11+ messages in thread
From: Adam Beneschan @ 2010-06-30 20:16 UTC (permalink / raw)


On Jun 30, 1:00 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> On Wed, 30 Jun 2010 12:12:17 -0700 (PDT), Adam Beneschan wrote:
> > On Jun 30, 10:35 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> > wrote:
> >> On Wed, 30 Jun 2010 07:39:24 -0700 (PDT), Adam Beneschan wrote:
> >>> On Jun 30, 3:39 am, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
> >>> wrote:
> >>>> A totally meaningless example just to illustrate
> >>>> the question: What is it that a compiler must report
> >>>> for the case statement below, if anything?
>
> >>> The choice "Sa" is not covered by any alternative. Other than that, I
> >>> don't think there's anything wrong with the CASE statement, and if you
> >>> had included a "when others =>" alternative I think it would be
> >>> legal. I'm not sure what potential problem you were trying to
> >>> illustrate.
>
> >> Let me propose this one instead:
>
> >> type DOW is (Mo, Tu, We, Th, Fr, Sa, So);
>
> >> case D is
> >> when (if D = Mo then Tu else Mo) => P;
> >> when (if D = Tu then Tu else Mo) => Q;
> >> when We..So => R;
> >> end case;
>
> >> The above is equivalent to:
>
> >> case D is
> >> when Tu => P;
> >> when Mo => Q;
> >> when We..So => R;
> >> end case;
>
> >> But as Pascal suggested, it should not compile because D is not static.
>
> > Ummm, not quite, because (1) Pascal didn't say anything about *why* he
> > thought it shouldn't compile (his entire statement was "This should
> > not compile I would say"), and (2) in the OP's original example, D
> > *is* static.  In your example, you're right that it shouldn't compile
> > because D is not static, but that's a different issue.  (Well, I
> > *assume* D isn't static.  Since your example doesn't include a
> > declaration of D, I can't tell.)
>
> So, if D is static, then all choices are defined and do not overlap, hence
> it must compile. Right?

No; it depends on what D is.  On looking over your post more
carefully, I'm beginning to think you accidentally left out some key
information, or made some other error.  You said earlier:

> >> case D is
> >> when (if D = Mo then Tu else Mo) => P;
> >> when (if D = Tu then Tu else Mo) => Q;
> >> when We..So => R;
> >> end case;
>
> >> The above is equivalent to:
>
> >> case D is
> >> when Tu => P;
> >> when Mo => Q;
> >> when We..So => R;
> >> end case;

Those are equivalent only if D is static and is equal to Mo.  If D=Tu,
then it's equivalent to

case D is
when Mo => P;
when Tu => Q;
when We..So => R;
end case;

If D is anything else, then it's equivalent to

case D is
when Mo => P;
when Mo => Q;
when We..So => R;
end case;

which of course will not compile.


> >> As for the problem Georg had in mid. Maybe it is this. Let you have some
> >> function, say Gamma function. Now,
>
> >> x : constant := 0.1;
> >> Gx : constant := Gamma (1.1); -- Illegal, what a pity
>
> >> Let us open the table of Gamma, scan it, and write something like:
>
> >> (if x < 0.0 then ... elsif x < 0.01 then ... )
>
> >> This wonderful static function can then copied and pasted everywhere you
> >> wanted to evaluate Gamma at compile time. Is it legal?
>
> > Gamma cannot be a static function (4.9(18-22)).  You cannot write a
> > static function (other than an enumeration literal, which is
> > technically a static function).
>
> Now I do not understand you. The expression I gave is an if-operator with
> only constants in it.

No, the expression you gave was an if-operator with a bunch of
ellipses in it.  I had no idea what you meant by it, and you were
talking about a function named Gamma.  Please excuse me if I had
trouble figuring out what you were trying to say.

> I presume it is static. E.g., simplified:
>
>   x : constant := 2.0;
>   Gx : constant := (if x <= 1.0 then 1.0 elsif x <= 2.0 then 2.0 elsif x
> <= 6.0 then 9.0 else 24.0);
>
> We could even add linear or quadratic interpolation between the points.

OK, that expression is legal, and Gx is a static constant that can be
used anywhere.  I don't see any relationship to Georg's question, nor
what point anybody is trying to make.

                     -- Adam




^ permalink raw reply	[flat|nested] 11+ messages in thread

* Re: When a conditional expression is static, where can it be used?
  2010-06-30 20:05     ` Georg Bauhaus
@ 2010-06-30 20:29       ` Adam Beneschan
  2010-06-30 20:45       ` Dmitry A. Kazakov
  1 sibling, 0 replies; 11+ messages in thread
From: Adam Beneschan @ 2010-06-30 20:29 UTC (permalink / raw)


On Jun 30, 1:05 pm, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
wrote:

> >> The choice "Sa" is not covered by any alternative.  Other than that, I
> >> don't think there's anything wrong with the CASE statement, and if you
> >> had included a "when others =>" alternative I think it would be
> >> legal.  I'm not sure what potential problem you were trying to
> >> illustrate.
>
> The questions I had asked myself (a little too quick, I suppose)
> were along these lines:
>
> Is it possible to invalidate a case construct by simply
> changing the value of a static constant used in determining
> conditional static case values?  Yes, it is possible even without
> conditional expressions, but do these introduce failures that
> are much more tricky to straighten out?

Of course, your case doesn't illustrate this; your case statement
could not have been valid for any possible value of D, so there's no
question of invalidating it by changing D.


> If parts of the language will have new (static) possibilities,
> what modes of (careful) thinking will these necessitate?

It means you have to be careful to write code that will be valid for
any possible value of the static constant(s) used in the conditional
expression.  But this hardly seems earth-shattering.  Nor do I expect
it would cause a problem in real life.  Sure, it's possible to create
code that will fail when a static value is changed and that might be
tricky to straighten out; but I suspect that this won't happen unless
a programmer was trying to be tricky in the first place.  Which I
don't recommend.  Write straightforward code and leave the tricks to
dog trainers.

                     -- Adam




^ permalink raw reply	[flat|nested] 11+ messages in thread

* Re: When a conditional expression is static, where can it be used?
  2010-06-30 20:05     ` Georg Bauhaus
  2010-06-30 20:29       ` Adam Beneschan
@ 2010-06-30 20:45       ` Dmitry A. Kazakov
  1 sibling, 0 replies; 11+ messages in thread
From: Dmitry A. Kazakov @ 2010-06-30 20:45 UTC (permalink / raw)


On Wed, 30 Jun 2010 22:05:25 +0200, Georg Bauhaus wrote:

> On 30.06.10 19:35, Dmitry A. Kazakov wrote:
>> On Wed, 30 Jun 2010 07:39:24 -0700 (PDT), Adam Beneschan wrote:
>> 
>>> On Jun 30, 3:39 am, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
>>> wrote:
>>>> A totally meaningless example just to illustrate
>>>> the question:  What is it that a compiler must report
>>>> for the case statement below, if anything?
>>>
>>> The choice "Sa" is not covered by any alternative.  Other than that, I
>>> don't think there's anything wrong with the CASE statement, and if you
>>> had included a "when others =>" alternative I think it would be
>>> legal.  I'm not sure what potential problem you were trying to
>>> illustrate.
> 
> The questions I had asked myself (a little too quick, I suppose)
> were along these lines:
> 
> Is it possible to invalidate a case construct by simply
> changing the value of a static constant used in determining
> conditional static case values?  Yes, it is possible even without
> conditional expressions, but do these introduce failures that
> are much more tricky to straighten out?

Yep, as the example shows.

> All this about static conditional expressions in case_statement_alternative
> is probably a somewhat artificial argument, since a conditional
> expression in such a place is something Ada programmers will
> just not write.  Right?

Hopefully. But the problem is that static expressions are non-testable. You
don't know if the expression is right until you substitute another value.
This is same problem as with the C++ templates and more and more with Ada
generics. This is why I don't like either and it seems that if-operators
move us in wrong direction.

>> Let me propose this one instead: 
>> 
>>     type DOW is (Mo, Tu, We, Th, Fr, Sa, So);
>> 
>>     case D is
>>        when (if D = Mo then Tu else Mo) => P;
>>        when (if D = Tu then Tu else Mo) => Q;
>>        when We..So => R;
>>     end case;
> 
> D: constant DOW := We;
> case D is  -- replace D with {We}
>    when (if {We} = Mo then Tu else Mo) => P;  -- Mo
>    when (if {We} = Tu then Tu else Mo) => Q;  -- Mo
>    when We .. So = => R;  -- I should have written Su, sorry
> end case;

Shame on me. (A perfect illustration to the point)
 
>> This wonderful static function can then copied and pasted everywhere you
>> wanted to evaluate Gamma at compile time. Is it legal?
> 
> Should we have "bigger" static functions?

Certainly yes to solve problems like measurement units support. And also to
encourage the programmer not to use these awful if-operators or at least to
refactor some of them.

At the same time static functions would be obviously exposed to the same
problem of non-testability and utter obscureness.

> The 'Constraint or invariant things being worked out for subtypes
> are, I guess, potentially static.  How far can one push the
> compiler *and* the programmer computing or specifying conditional
> expressions, resp.?
> (And not have one's head spin too much, or introduce programs
> that surprise when changed?)

The only solution I see is requiring proofs of correctness in static
contexts. I.e. if you wrote:

   case X is
      when F (...) => -- F,G are complicated user-defined static functions
      when G (...) =>
   end case;

then the language should require that F and G would make the case statement
correct by any possible combination of their arguments, rather than by only
the current one.

In short, the static meta-language of Ada must be at least like SPARK.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



^ permalink raw reply	[flat|nested] 11+ messages in thread

* Re: When a conditional expression is static, where can it be used?
  2010-06-30 19:12     ` Adam Beneschan
  2010-06-30 20:00       ` Dmitry A. Kazakov
@ 2010-07-01 17:04       ` Pascal Obry
  1 sibling, 0 replies; 11+ messages in thread
From: Pascal Obry @ 2010-07-01 17:04 UTC (permalink / raw)


Le 30/06/2010 21:12, Adam Beneschan a �crit :
> Ummm, not quite, because (1) Pascal didn't say anything about *why* he
> thought it shouldn't compile (his entire statement was "This should
> not compile I would say"), 

Because Sa is not covered by the alternatives.

And if you ask me I find this quite a bad style. I hope GNAT will have
some options to disallow if conditional expression in cases
alternatives. This makes the code hard to read.

Pascal.

-- 

--|------------------------------------------------------
--| Pascal Obry                           Team-Ada Member
--| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE
--|------------------------------------------------------
--|    http://www.obry.net  -  http://v2p.fr.eu.org
--| "The best way to travel is by means of imagination"
--|
--| gpg --keyserver keys.gnupg.net --recv-key F949BD3B




^ permalink raw reply	[flat|nested] 11+ messages in thread

end of thread, other threads:[~2010-07-01 17:04 UTC | newest]

Thread overview: 11+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2010-06-30 10:39 When a conditional expression is static, where can it be used? Georg Bauhaus
2010-06-30 11:25 ` Pascal Obry
2010-06-30 14:39 ` Adam Beneschan
2010-06-30 17:35   ` Dmitry A. Kazakov
2010-06-30 19:12     ` Adam Beneschan
2010-06-30 20:00       ` Dmitry A. Kazakov
2010-06-30 20:16         ` Adam Beneschan
2010-07-01 17:04       ` Pascal Obry
2010-06-30 20:05     ` Georg Bauhaus
2010-06-30 20:29       ` Adam Beneschan
2010-06-30 20:45       ` Dmitry A. Kazakov

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox