Gnat GPL 2010 available soon (conditional expressions)
in [ADA]
|
Prev: Ann: Generic Image Decoder v.01
Next: ANN: Tables 1.10
From: Gautier write-only on 30 Jun 2010 00:13 On 30 juin, 03:19, BrianG <briang...(a)gmail.com> wrote: > So, I guess for Ada'2w we can expect ++, --, +=, -=, and their brethren. Sure, and while the language will have become dysfunctional, it will have failed to attract people used to shortcuts, because they will want the curly brackets anyway. G.
From: Warren on 30 Jun 2010 12:46 Gautier write-only expounded in news:021332cd-73f7-47d3-8126-4ff33185e5b3 @r27g2000yqb.googlegroups.com: > On 30 juin, 03:19, BrianG <briang...(a)gmail.com> wrote: > >> So, I guess for Ada'2w we can expect ++, --, +=, -=, and their brethren. > > Sure, and while the language will have become dysfunctional, it will > have failed to attract people used to shortcuts, because they will > want the curly brackets anyway. > > G. Next, they'll want square brackets-- where will it all end? ;-) Warren
From: Peter C. Chapin on 30 Jun 2010 19:20 On 2010-06-30 00:09, Gautier write-only wrote: > I can imagine - and probably it will be usual to come across code > like : > > X( (if Condition_a then Expression_1a else Expression_2a) ):= > Y( (if Condition_b then Expression_1b else Expression_2b) ); > > with Condition_b involving X and Condition_a involving Y, for > instance... mmmh! That wouldn't be any weirder than, for example X(Y(I + 1)) := Y(X(J - 1)); I don't see how conditional expressions would make such examples any worse. Peter
From: Phil Clayton on 4 Jul 2010 21:27 On Jun 30, 4:21 am, Britt Snodgrass <britt.snodgr...(a)gmail.com> wrote: > > Yes, and I'll stick with SPARK. I expect future versions of SPARK will > resist such weirdness. For formal verification tools, conditional expressions could be useful. For example, there are two paths through if C then Y := A; else Y := B; end if; but only one path through Y := (if C then A else B); For compliance analysis, the latter could mean only one VC generated rather than two. (In an interactive proof of that one VC, yes, you could end up case splitting on the condition but you're better off because the case split would only be done if necessary and where necessary, i.e. possibly just for a part of the overall proof.) For different types of analysis with SPARK, I'm not sure what the relative merits would be. In my view, condition expressions are a step in the right direction... but I'm the sort of person who wants to write an array aggregate like (for I in 1 .. 5 => (for J in 1 .. 7 => (if I = J then 1.0 else 0.0))) Phil
From: Georg Bauhaus on 5 Jul 2010 06:26
On 05.07.10 03:27, Phil Clayton wrote: > On Jun 30, 4:21 am, Britt Snodgrass <britt.snodgr...(a)gmail.com> wrote: > For formal verification tools, conditional expressions could be > useful. For example, there are two paths through > > if C then > Y := A; > else > Y := B; > end if; > > but only one path through > > Y := (if C then A else B); Any advantage over a function---which in SPARK case will be a pure function, IIRC? Y := Find_Y (Depends => C); > In my view, condition expressions are a step in the right direction... > but I'm the sort of person who wants to write an array aggregate like > > (for I in 1 .. 5 => (for J in 1 .. 7 => (if I = J then 1.0 else > 0.0))) What kind of name would you pick for the thing? Georg |