Gnat GPL 2010 available soon
Stephen Sangwine
will be available soon:
http://libre.adacore.com/libre/
Great news, as those of with Snow Leopard on Mac OS X
currently don't have a free compiler available. It will
also support Windows 7 (I am not sure if that is new as
I haven't used Windows for a few years).
Martin
Oh yes we do! But you do have to look around a bit...
...must I really miss GPS, so that's what I looking forward to most!
I've tried to love emacs but I fear I never shall.
-- Martin
Simon Wright
http://sourceforge.net/projects/gnuada/files/GNAT_GPL%20Mac%20OS%20X/2009-snow-leopard/
Albrecht Käfer
wrote:
Oh look: “Support for Visual Studio 2008”
Ada's roots in the military are showing: Just ready for the last war when
the next one is breaking out.
Albrecht
lek...@gmail.com
--------------------------------------------------------------------------------
function Validate (Dir : in String) return String is
begin
return (if Dir (Dir'Last) = '\' then Dir else Dir & '\');
end Validate;
--------------------------------------------------------------------------------
C:\test\> gnatmake -gnat12 validate.adb
gcc -c -gnat12 validate.adb
+===========================GNAT BUG
DETECTED==============================+
| GPL 2010 (20100603) (i686-pc-mingw32) GCC
error: |
| in mostly_copy_tree_r, at gimplify.c:
893 |
| Error detected around C:/gnat/lib/gcc/i686-pc-mingw32/4.3.6/
adainclude/s-stoele.ads:65|
| Please submit a bug report by email to
rep...@adacore.com. |
| GAP members can alternatively use GNAT
Tracker: |
| http://www.adacore.com/ section 'send a
report'. |
| See gnatinfo.txt for full info on procedure for submitting
bugs. |
| Use a subject line meaningful to you and us to track the
bug. |
| Include the entire contents of this bug box in the
report. |
| Include the exact gcc or gnatmake command that you
entered. |
| Also include sources listed below in gnatchop
format |
| (concatenated together with no headers between
files). |
| Use plain ASCII or MIME
attachment. |
+==========================================================================
+
Please include these source files with error report
Note that list may not be accurate in some cases,
so please double check that the problem can still
be reproduced with the set of files listed.
Consider also -gnatd.n switch (see debug.adb).
validate.adb
compilation abandoned
gnatmake: "validate.adb" compilation error
I'll submit a bug report.
an...@anon.org
Now, to compile the Ada system this statement type must work because it
is embeded in a number of locations in the Ada.Text_IO.adb and other
Ada system packages.
So, first, try compiling without the "-gnat12" switch.
Second, try the routine without the concatenation operator "&"
or try to return a static string or a substring.
Then again this statement may be limited to numerical, characters
type values only.
If that does not work try copying "a-textio.ad*" to a local temp dir
and compile it by:
gcc -c -gnatpg a-textio.adb
You should get no errors, only a warning that your states your
recompiling the a system package.
Last, if you have or still have GNAT 2009 try compiling using 2009:
gnatmake ....
lek...@gmail.com
> Now, to compile the Ada system this statement type must work because it
> is embeded in a number of locations in the Ada.Text_IO.adb and other
> Ada system packages.
Yes. Conditional expressions do not fail everywhere. In this specific
case, both Dir & '\' and the fact that Dir is a function argument are
required to trigger the bug.
> So, first, try compiling without the "-gnat12" switch.
[...]
> Last, if you have or still have GNAT 2009 try compiling using 2009:
I've already reported the bug, so I'll let them (AdaCore) do the
debugging...
Dmitry A. Kazakov
> Well, it hasn't been hard to find the first bug.
>
> --------------------------------------------------------------------------------
> function Validate (Dir : in String) return String is
> begin
> return (if Dir (Dir'Last) = '\' then Dir else Dir & '\');
> end Validate;
> --------------------------------------------------------------------------------
[...]
> I'll submit a bug report.
(Yes, to remove that abomination from the language! (:-))
I didn't read the AI, but your code looks very strange to me. Isn't its
syntax exposed to the infamous Pascal-if flaw? I mean, where is the "end
if"? Is this legal:
(if A then X else if B then Y else Z)
P.S. Is case allowed too?
P.P.S. Didn't they forget the return statement? It would be great "fun" to
write and read this:
if return X : Boolean do
declare
...
begin
...
end:
end return;
then
...
if;
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
lek...@gmail.com
wrote:
> (Yes, to remove that abomination from the language! (:-))
I don't like it much, but I don't like
if A then
V := X;
else
V := Y;
end if;
that much either.
> I didn't read the AI, but your code looks very strange to me. Isn't its
> syntax exposed to the infamous Pascal-if flaw? I mean, where is the "end
> if"? Is this legal:
>
> (if A then X else if B then Y else Z)
Read the AI. IIRC, parenthesis are usually required, so (if A then X
else (if B then Y else Z)), but the rules for parenthesis are relaxed
in some contexts, like function arguments, so "F (if A then X else
Y);" instead of "F ((if A then X else Y));".
> P.S. Is case allowed too?
I think so, yes.
> P.P.S. Didn't they forget the return statement? It would be great "fun" to
> write and read this:
>
> if return X : Boolean do
> declare
> ...
> begin
> ...
> end:
> end return;
> then
> ...
> if;
Very funny... sort of.
an...@anon.org
The compiler blowing up is an error, but, there are always a way around
that type of error, if you find the correct syntax. Try adding parenthesis
around the output, since the compiler may see the "Dir" as value and
the " & '\'" as extra not part of the statement.
function Validate (Dir : in String) return String is
begin
return (if Dir (Dir'Last) = '\' then Dir else (Dir & '\'));
end Validate;
And until the Ada2012 RM or documentation/examples come out from Adacore,
its anyone guess on the true syntax of all additional statements. Unless
you want to spend time in reading the though the gnat Ada compiler.
now, in taking a quick look at "par_ch4.adb", Adacore did add that
"gnat12" only switch to use the following features:
1. conditional expression -- statement must be parenthesized.
(if X then Opt1 else Opt2)
where Opt1 and Opt2 must be a function or variable
-- the following two addition are not in the documentation, yet!
2. case expression -- statement must be parenthesized.
assuming syntax is like conditional expression
(case X when Opt1 => Val1
when Opt2 => Val2 when others => Val2)
where Val1 and Val2 must be a function or variable
3. from RM 4.5.2 Relational Operators and Membership Tests
Now allows the use of "Vertical_Bar" in Membership Tests
assuming from code syntax
N in X .. Y | A .. B | G .. K
Georg Bauhaus
> On Sat, 26 Jun 2010 05:04:10 -0700 (PDT), lek...@gmail.com wrote:
>
>> Well, it hasn't been hard to find the first bug.
>>
>> --------------------------------------------------------------------------------
>> function Validate (Dir : in String) return String is
>> begin
>> end Validate;
>> --------------------------------------------------------------------------------
>
> [...]
>> I'll submit a bug report.
>
> (Yes, to remove that abomination from the language! (:-))
>
> I didn't read the AI, but your code looks very strange to me. Isn't its
> syntax exposed to the infamous Pascal-if flaw? I mean, where is the "end
> if"? Is this legal:
>
> (if A then X else if B then Y else Z)
As the AI explains, you will need bracketing.
WRT syntax, the Validate above example is OK for GNAT 2009
with -gnatX, but this GNAT wants constraints on the return value.
And, yes, one may omit the "else branch" in a conditional expression
if the result should be Boolean, thus implying True...
Conditional expressions are supposed to remove the need for some single
purpose functions, see the example in the AI lekktu has mentioned.
Unlike the return object of a function, the value of a
conditional expression cannot be renamed. A special purpose
function in place of a conditional expression has to have a
return object. We can't rely on effective inlining or on
evaluation at compile time, either. If so, then in principle
there is overhead. This is solved with conditional expressions.
OTOH, we get the anonymity of conditional expressions, and
an opportunity to deviate from Ada's principle of linear reading.
But maybe the principle of linear has become outdated?
John Barnes's integration example forces the reader
up and down the nesting structure when reading, as do
some container algorithms. And they make sense!
So maybe conditional expressions deserve the same
exception from a preference for linear reading?
Consequently, conditional expressions will make Ada
more attractive for programmers who still know the joys of
clever programming constructs like syntactical inversion
of control structure. Or who have been brought up with Lisp
or Caml. If their modes of expression are not wanted on some project,
the project can use additional source code analysis tools.
These will complain when noticing nested conditional expressions,
for example.
Dmitry A. Kazakov
> On 6/26/10 11:42 PM, Dmitry A. Kazakov wrote:
>> On Sat, 26 Jun 2010 05:04:10 -0700 (PDT), lek...@gmail.com wrote:
>>
>>> Well, it hasn't been hard to find the first bug.
>>>
>>> --------------------------------------------------------------------------------
>>> function Validate (Dir : in String) return String is
>>> begin
>>> return (if Dir (Dir'Last) = '\' then Dir else Dir& '\');
>>> end Validate;
>>> --------------------------------------------------------------------------------
>>
>> [...]
>>> I'll submit a bug report.
>>
>> (Yes, to remove that abomination from the language! (:-))
>>
>> I didn't read the AI, but your code looks very strange to me. Isn't its
>> syntax exposed to the infamous Pascal-if flaw? I mean, where is the "end
>> if"? Is this legal:
>>
>> (if A then X else if B then Y else Z)
>
> As the AI explains, you will need bracketing.
Once I designed a language like that. It was out of necessity because that
specialized language had only expressions. I also used brackets, but
dropped "if", because you don't need it:
(A then B [else C])
is syntactically unambiguous and easier to read.
Anyway I do hate the idea, partially because I have been using that
language for a long time.
> Conditional expressions are supposed to remove the need for some single
> purpose functions, see the example in the AI lekktu has mentioned.
Single-purpose functions do not exist, likewise single-purpose types etc.
Thinking of something in this way will give you a design/maintenance
problem later. Ada was never designed to minimize up front thinking and
typing in mind.
> Unlike the return object of a function, the value of a
> conditional expression cannot be renamed. A special purpose
> function in place of a conditional expression has to have a
> return object. We can't rely on effective inlining or on
> evaluation at compile time, either.
can you rely on what the compiler does for if-expressions? Come on, that is
a silly argument. If inlining is a problem add pragma Enforced_Inline.
> OTOH, we get the anonymity of conditional expressions, and
> an opportunity to deviate from Ada's principle of linear reading.
towards the principle of no reading? Write and rewrite, but never read what
you wrote...
> Consequently, conditional expressions will make Ada
> more attractive for programmers who still know the joys of
> clever programming constructs like syntactical inversion
> of control structure.
Sorry, if I misunderstood you. Do you seriously mean that the goal of
language design is attracting some people?
> If their modes of expression are not wanted on some project,
> the project can use additional source code analysis tools.
> These will complain when noticing nested conditional expressions,
> for example.
In C projects you can use lint. Does it make the design of C any better?
lek...@gmail.com
> The compiler blowing up is an error, but, there are always a way around
> that type of error, if you find the correct syntax. Try adding parenthesis
> around the output, since the compiler may see the "Dir" as value and
> the " & '\'" as extra not part of the statement.
I already know a couple ways around the bug, starting from going back
to
if Dir (Dir'Last) = '\' then
return Dir;
else
return Dir & '\';
end if;
all the way to
function Validate (Dir : in String) return String is
Validated : constant String := (if Dir (Dir'Last) = '\' then Dir
else Dir & '\');
begin
return Validated;
end Validate;
> And until the Ada2012 RM or documentation/examples come out from Adacore,
> its anyone guess on the true syntax of all additional statements.
This has nothing to do with syntax, which is correct AFAICS (please
note the above example with the Validated constant string compiles
just fine). It's a plain simple bug.
> Unless you want to spend time in reading the though the gnat Ada compiler.
I often do.
lek...@gmail.com
wrote:
> dropped "if", because you don't need it:
>
> (A then B [else C])
>
> is syntactically unambiguous and easier to read.
As you can see on the relevant AI, this was in fact considered (among
lots of other things). FWIW, I'm quite glad they went for the 'if', to
me it is *much* easier to read.
Dmitry A. Kazakov
How do you know it? (:-))
BTW, in my language I also have a bracketless [infix] form:
B when A else C
where "when" and "else" are true infix operators. The above is associated
as:
((B when A) else C)
The semantics is that
B when A
is B when A is true and undefined when A is false.
X else C
is X when X is defined and C otherwise. This is a bit easier to read,
because of its symmetry.
But so far I saw no readable syntax for conditional expressions and I doubt
that it existed.
Georg Bauhaus
> On Sun, 27 Jun 2010 03:55:02 -0700 (PDT), lek...@gmail.com wrote:
>
>> On Jun 27, 10:37 am, "Dmitry A. Kazakov"<mail...@dmitry-kazakov.de>
>> wrote:
>>
>>> dropped "if", because you don't need it:
>>>
>>> (A then B [else C])
>>>
>>> is syntactically unambiguous and easier to read.
>>
>> As you can see on the relevant AI, this was in fact considered (among
>> lots of other things). FWIW, I'm quite glad they went for the 'if', to
>> me it is *much* easier to read.
>
> How do you know it? (:-))
I'd know readability of some particular syntax
from empirical evidence. People read statements.
How many times do you hear someone shout, "Ouch, this is
conditional, I didn't notice at first!" Cases in point are
when a declaration or a statement does not start with IF
but involves a conditional expression. Compare alternative
solutions.[*] (I believe Dilbert explains some kind of
WTF count for quality testing but I can't find it at the
moment.)
The situation is worse in the functional languages camp,
though. Whitaker's observations from the mid 1970s become
true again there, I think.
If you have to select software components by functionality
you must still accept it when each is written in some new
language, because ... That's where Whitaker's observations
are relevant again, I think.
Python has your syntax, too, though it didn't from the start,
see about PEP 308, where Kuchling writes, "so the order of
evaluation jumps around a bit": The expression
B if A else C
places the controlling expression in the middle of
what it is controlling. This placement seem obvious when
painting program trees but we are writing programs on single
lines. When you read linearly, IF will signal that some
case distinction is coming. When IF appears after what
it is controlling, you are reminded that what you have
just been reading is actually conditional on some program
text to follow next. And maybe there is going to be some
other thing for the other case. Or maybe not.
More about the parens around the expressions in Kuchling's
comments, too.
Python also has
[F(X) for X in I if P]
for list comprehensions, I being iterable. No else part
is allowed here. Compare
[ F(X) : X in I | P ] of SETL
(or { F(X) ... } for set comprehensions) and
[ F(X) | X <- I, P ] of Haskell.
There are more syntactic variations of the same concept of a
list comprehension in every journeyman's piece being added as
a new programming language to the list of yet another
functional programming language. No one seems to ask
the question that had obviously been asked when Algol 60
was created: What is the abstract syntax for this and how
can we make a good, satisfying concrete syntax? Based on
which criteria?
Python also has
A and B or C
meaning the same as "B if A else C". This works because all
expressions can be used as Booleans. Anyway, Python is said to
be consistent, probably because of the supply of rules
about proper contexts for using the word "if". Now add to
that single rule set the requirement to use more than
one language during daily work, each of them equipped with
IF related idiosyncrasies. Makes me mad.
If conditional expressions are needed, then at least let
the reader know that what is next is a conditional.
Ada uses the token sequence '(', IF for that.
Kuchling recommends parens for Python's conditional
expressions even when they are not strictly needed; they
are when sorting out associativity problems.
http://docs.python.org/whatsnew/2.5.html
This is the version of Python that programming Google
App Engine currently requires...
____
[*] Always important for for a language being capable of
drawing attention:
Is the equation "easy syntax" = "dumb and boring" true?
If so, we have to provide for some ASCII punctuation shuffling
in the grammar, because these are the characters that programmers
are capable of typing on their keyboards. There sole means of
distinction.
See MS's answer called F#, BTW...
Peter C. Chapin
> Python has your syntax, too, though it didn't from the start,
> see about PEP 308, where Kuchling writes, "so the order of
> evaluation jumps around a bit": The expression
>
> B if A else C
>
> places the controlling expression in the middle of
> what it is controlling. This placement seem obvious when
> painting program trees but we are writing programs on single
> lines. When you read linearly, IF will signal that some
> case distinction is coming. When IF appears after what
> it is controlling, you are reminded that what you have
> just been reading is actually conditional on some program
> text to follow next. And maybe there is going to be some
> other thing for the other case. Or maybe not.
For what it's worth, I agree that the syntax with the leading 'if' is
much more readable to me than the alternatives presented here so far.
For one thing (if A then B else C) seems pretty widely used by
functional languages (OCaml, Haskell, Scala, even Lisp after accounting
for Lisp's general syntax). It also reads well in English, which is true
of other Ada constructs.
In any case I want to know up front that what I'm about to read is
conditional. If I have to first read over some (potentially complex)
expression before I come to the syntax that signals the conditionality
of the construct, I will end up back tracking and reading the expression
again.
Also I find that when skimming program text just knowing that something
is conditional is sometimes enough for me to decide if I have to read it
more closely or not. If it says
X := (if Rare_Condition then
Complicated_Expression
else
Complicated_Expression);
I might be able to quickly tell which complicated expression I need to
look at without having to study both. But with something like
X := (Rare_Condition then
Complicated_Expression
else
Complicated_Expression);
Hera at a first glance it looks like the assignment to X is all about
Rare_Condition. Something like
X := (Complicated_Expression
when
Rare_Condition
else
Complicated_Expression);
Is even worse. Not only does it look like the assignment is about the
first complicated expression, I will probably end up studying that
expression before I even realize that is only rarely evaluated.
Of course it all comes down to what one is used to. Dmitry says the
leading 'if' makes things harder to read, but I find his examples much
more difficult.
Peter
Dmitry A. Kazakov
> Also I find that when skimming program text just knowing that something
> is conditional is sometimes enough for me to decide if I have to read it
> more closely or not. If it says
>
> X := (if Rare_Condition then
> Complicated_Expression
> else
> Complicated_Expression);
In comparable cases earlier Ada's choices were opposite:
Complicated_Expression and then Complicated_Expression
Complicated_Expression or else Complicated_Expression
(Type with Complicated_List)
> I might be able to quickly tell which complicated expression I need to
> look at without having to study both.
Do not use complicated expressions, that is the point! Note that you have
to format the expression so that it looked like a normal if. What is the
gain? It is unreadable when written as one line. It is as verbose as normal
if when formatted. And it does not save you writing a function in real-life
cases:
File_Name := <add extension ".txt" if absent, do lower case, remove
forward "./"> Argument (1);
> Of course it all comes down to what one is used to. Dmitry says the
> leading 'if' makes things harder to read, but I find his examples much
> more difficult.
If you like prefix notation, then why not:
generic -- Built-in intrinsic generic for each type
Type (<>) is limited private;
function "if" (Condition : Boolean; Then, Else : Type) return Type;
used as:
if (A, B, C)
if (A, then => B, else => C)
mahdert
I installed the latest version of GNAT GPL on windows 7 and i cannot
get it to work. It seems that it is not compatible, so I will jave to
see if this new version can work well.
Peter C. Chapin
> Do not use complicated expressions, that is the point! Note that you have
> to format the expression so that it looked like a normal if. What is the
> gain?
As I mentioned before, I think the real point of the conditional
expressions in Ada is to support the new pre- and post-condition
features. My understanding is that statements are not allowed in that
context. Sure involved cases might look like a normal if, but that's
better than not being able to express a conditional at all. That is, the
point of conditional expressions is not to somehow make the code shorter.
The use of conditional expressions in "normal" code is optional (I
think) but I can see that once you add them to the language, forbidding
them from normal code would seem oddly inconsistent.
Peter
Georg Bauhaus
>> The use of conditional expressions in "normal" code is optional (I
>> think) but I can see that once you add them to the language, forbidding
>> them from normal code would seem oddly inconsistent.
>
> Yes. This is exactly same as anonymous access types and other "workaround"
> things. Once you let them in, they won't leave.
Conditional expressions will not be everywhere if your project uses
a source code analysis tool with suitable settings.
Dmitry A. Kazakov
The only code analysis tool is the compiler, otherwise the language is to
be fixed.
Georg Bauhaus
Or let industry decide which Ada language profiles they would like
standardized.
A language profile such as the subset of Ada defined by SPARK,
with recursion and named pointers added. Maybe including generics
with formal types only.
Dmitry A. Kazakov
> On 28.06.10 18:36, Dmitry A. Kazakov wrote:
>> On Mon, 28 Jun 2010 16:47:50 +0200, Georg Bauhaus wrote:
>>
>>> On 29.06.10 16:08, Dmitry A. Kazakov wrote:
>>>
>>>>> The use of conditional expressions in "normal" code is optional (I
>>>>> think) but I can see that once you add them to the language, forbidding
>>>>> them from normal code would seem oddly inconsistent.
>>>>
>>>> Yes. This is exactly same as anonymous access types and other "workaround"
>>>> things. Once you let them in, they won't leave.
>>>
>>> Conditional expressions will not be everywhere if your project uses
>>> a source code analysis tool with suitable settings.
>>
>> The only code analysis tool is the compiler, otherwise the language is to
>> be fixed.
>
> Or let industry decide which Ada language profiles they would like
> standardized.
I don't think that industry is capable of making wise decisions. So far
they have chosen MISRA C.
> A language profile such as the subset of Ada defined by SPARK,
> with recursion and named pointers added. Maybe including generics
> with formal types only.
I don't like the idea of breaking language into many clades. Especially
Ada, of which user base is pretty thin.
In my view instead of specifying undesired constructs (the profile), the
programmer should do what he wants to be proved. The compiler should try
and then, if proof is not possible, because of the construct X, point this
out to the programmer. I like to compare this with:
My_Real is digits 6 range 0.0...100.0;
-- This is what I need, tell me if you cannot
vs.
double
// This is what limits me, guess why.
IMO, the first is the Ada way.
Randy Brukardt
news:4c276114$0$2378$4d3e...@news.sover.net...
...
> Also I find that when skimming program text just knowing that something
> is conditional is sometimes enough for me to decide if I have to read it
> more closely or not. If it says
>
> X := (if Rare_Condition then
> Complicated_Expression
> else
> Complicated_Expression);
>
> I might be able to quickly tell which complicated expression I need to
> look at without having to study both.
Note that one advantage of conditional expressions is that they can avoid
duplicating code. For instance,
X(Index_Expression*Index_Base + 1) :=
(if Condition then
Complicated_Expression
else
Other_Complicated_Expression);
Probably is preferable to
if Condition then
X(Index_Expression*Index_Base + 1) := Complicated_Expression;
else
X(Index_Expression*Index_Base - 1) := Other_Complicated_Expression;
end if;
because it is much less likely to have a subtle error (like the second
example I wrote above). I find that I write quite a bit of code of the
second form, and I know I'd save time debugging if I had the first.
Randy.
P.S. But the resolution of conditional expressions is surprisingly complex.
I think we've got it right, finally.
BrianG
> "Peter C. Chapin" <pcc4...@gmail.com> wrote in message
> news:4c276114$0$2378$4d3e...@news.sover.net...
> ...
> duplicating code. For instance,
>
So, I guess for Ada'2w we can expect ++, --, +=, -=, and their brethren.
That's the same argument that's always been used there.
This is one case (maybe the first) I agree with Dmitry. It's an ugly
addition.
Maybe it's a good thing my current project is stuck on Ada'95.
--Brian
Britt Snodgrass
>
> This is one case (maybe the first) I agree with Dmitry. It's an ugly
> addition.
That was my reaction to seeing it. Its rather horrid to look at.
>
> Maybe it's a good thing my current project is stuck on Ada'95.
>
Yes, and I'll stick with SPARK. I expect future versions of SPARK will
resist such weirdness.
- Britt
Gautier write-only
> P.S. But the resolution of conditional expressions is surprisingly
> complex. I think we've got it right, finally.
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!
G.
Gautier write-only
> 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.
Warren
@r27g2000yqb.googlegroups.com:
Next, they'll want square brackets-- where will it all end? ;-)
Warren
Peter C. Chapin
> 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
Phil Clayton
>
> 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
Georg Bauhaus
> On Jun 30, 4:21 am, Britt Snodgrass <britt.snodgr...@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
Dmitry A. Kazakov
> 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)))
(for I in 1..5 => (for J in 1..7 => Float (Boolean'Pos (I = J))))
Phil Clayton
wrote:
> On 05.07.10 03:27, Phil Clayton wrote:
>
> > On Jun 30, 4:21 am, Britt Snodgrass <britt.snodgr...@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);
Not much advantage over a function, only that you don't have the
overheads of introducing the new function and ensuring its
specification has sufficient information. I wasn't really considering
the possibility of introducing new functions as a general
alternative. For example, I would rather see certain conditional
expressions inline and not tucked away inside functions, for
readability.
(Correct, SPARK does not allow functions to have side effects.)
> > 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?
I suppose I'd call it a 'tabulation'..
Phil
Phil Clayton
wrote:
> On Sun, 4 Jul 2010 18:27:04 -0700 (PDT), Phil Clayton wrote:
> > 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)))
>
> (for I in 1..5 => (for J in 1..7 => Float (Boolean'Pos (I = J))))
Yep, I should have seen that one coming straight back... and taken
steps to avoid it :)
Phil
Dmitry A. Kazakov
BTW, is your construct 1) a macro expansion (as I remember PL/1
preprocessor also had %for statement alike) and how far are you ready to go
allowing "for" macros? Loops unrolling? Or else 2) it is an attempt to name
the components of an array element index. In the latter case
(I, J : others => <an expression involving I,J>)
(I : 1..5 => <an expression involving I>)
(Odd : 1 | 3 | 5 | 7 => <an expression involving Odd>, others => 0.0)
etc
looks to me more consistent with existing Ada, e.g. when Error : others =>
in exception handlers.
Georg Bauhaus
> BTW, is your construct 1) a macro expansion (as I remember PL/1
> preprocessor also had %for statement alike) and how far are you ready to go
> allowing "for" macros? Loops unrolling? Or else 2) it is an attempt to name
> the components of an array element index. In the latter case
>
> (I, J : others => <an expression involving I,J>)
> (I : 1..5 => <an expression involving I>)
> (Odd : 1 | 3 | 5 | 7 => <an expression involving Odd>, others => 0.0)
> etc
>
> looks to me more consistent with existing Ada, e.g. when Error : others =>
> in exception handlers.
I think that AI 05 177 might be on topic.
http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai05s/ai05-0177-1.txt
Phil Clayton
wrote:
> On Mon, 5 Jul 2010 15:47:41 -0700 (PDT), Phil Clayton wrote:
> > On Jul 5, 2:12 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> > wrote:
> >> On Sun, 4 Jul 2010 18:27:04 -0700 (PDT), Phil Clayton wrote:
> >>> 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)))
>
> >> (for I in 1..5 => (for J in 1..7 => Float (Boolean'Pos (I = J))))
>
> > Yep, I should have seen that one coming straight back... and taken
> > steps to avoid it :)
>
> BTW, is your construct 1) a macro expansion (as I remember PL/1
> preprocessor also had %for statement alike) and how far are you ready to go
> allowing "for" macros? Loops unrolling? Or else 2) it is an attempt to name
> the components of an array element index.
Definitely the latter...
> In the latter case
>
> (I, J : others => <an expression involving I,J>)
> (I : 1..5 => <an expression involving I>)
> (Odd : 1 | 3 | 5 | 7 => <an expression involving Odd>, others => 0.0)
> etc
>
> looks to me more consistent with existing Ada, e.g. when Error : others =>
> in exception handlers.
Interesting. So, considering the difference between
1. X : T
2. for X in T
My take on Ada is that [1] just declares a new variable X of subtype T
(which may be initialized depending on context) whilst [2] is used
when declaring a new variable X of subtype T and then giving X the
values of T in some specified order, i.e. introducing some iteration
scheme. If that is a fair assessment of things, then perhaps
(for I in 1 .. 5 => F(I))
is more in keeping with existing Ada? (If I'm talking absolute
drivel, please let me know...)
The concept of an order is important because the function F could have
side effects in the above example (though I would not advocate that as
good practice). However, we would be able to write
(for I in reverse A'Range => A(I))
to represent the reverse of the array A is perhaps a little confusing.
Also, it really only makes sense to have one variable holding the
array index. For example, if we could write
(I, J : 1 .. 5 => ...)
surely I and J would always be equal: there are only 5 elements in the
array. Having
(for I in 1 .. 5 => ...)
syntactically rules out multiple variables.
Phil
Dmitry A. Kazakov
> The concept of an order is important because the function F could have
> side effects in the above example (though I would not advocate that as
> good practice).
AFAIK, presently the order is not defined. So though this is legal
X : String (1..80) := (others => Character'Read (Stream'Access));
It is not a good idea.
> However, we would be able to write
>
> (for I in reverse A'Range => A(I))
>
> to represent the reverse of the array A is perhaps a little confusing.
The effect is undefined. Theoretically the compiler could initialize array
elements concurrently on a multi-core processor.
> Also, it really only makes sense to have one variable holding the
> array index. For example, if we could write
>
> (I, J : 1 .. 5 => ...)
>
> surely I and J would always be equal: there are only 5 elements in the
> array. Having
>
> (for I in 1 .. 5 => ...)
>
> syntactically rules out multiple variables.
Yes, but many other things as well. However I prefer an absolutely
different approach anyway, e.g. proper index types. In my world a diagonal
would be initialized like:
(Diagonal (5, 5) => 1.0, others => 0.0)
where Diagonal is a proper function.
Phil Clayton
wrote:
> On Tue, 6 Jul 2010 09:31:05 -0700 (PDT), Phil Clayton wrote:
> > The concept of an order is important because the function F could have
> > side effects in the above example (though I would not advocate that as
> > good practice).
>
> AFAIK, presently the order is not defined. So though this is legal
>
> X : String (1..80) := (others => Character'Read (Stream'Access));
>
> It is not a good idea.
It would be good if the order was not defined because that would
prevent people depending on it, so making it easier for a compiler to
parallelize.
> > However, we would be able to write
>
> > (for I in reverse A'Range => A(I))
>
> > to represent the reverse of the array A is perhaps a little confusing.
>
> The effect is undefined. Theoretically the compiler could initialize array
> elements concurrently on a multi-core processor.
There are really two concepts here:
1. the order of evaluation of the expressions for each index
2. the value the bound variable I gets for each index
I didn't make it clear that I was switching from [1] to [2], sorry.
This above reverse example was really about [2] to show that the use
of the keyword 'reverse' would result in I having the value A'Last at
index A'First, A'Last - 1 at index A'First + 1, etc. I don't think it
matters whether A(I) is evaluated for each index in parallel, so I
think the expression should be well defined.
> > Also, it really only makes sense to have one variable holding the
> > array index. For example, if we could write
>
> > (I, J : 1 .. 5 => ...)
>
> > surely I and J would always be equal: there are only 5 elements in the
> > array. Having
>
> > (for I in 1 .. 5 => ...)
>
> > syntactically rules out multiple variables.
>
> Yes, but many other things as well. However I prefer an absolutely
> different approach anyway, e.g. proper index types. In my world a diagonal
> would be initialized like:
>
> (Diagonal (5, 5) => 1.0, others => 0.0)
>
> where Diagonal is a proper function.
Interesting.. how would you make the expression a function of the
index? For example, how would you write
(for I in 3 .. 8 => A(I) + B(I - 2))
?
Phil
Dmitry A. Kazakov
> On Jul 6, 6:18 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> On Tue, 6 Jul 2010 09:31:05 -0700 (PDT), Phil Clayton wrote:
>>> The concept of an order is important because the function F could have
>>> side effects in the above example (though I would not advocate that as
>>> good practice).
>>
>> AFAIK, presently the order is not defined. So though this is legal
>>
>> X : String (1..80) := (others => Character'Read (Stream'Access));
>>
>> It is not a good idea.
>
> It would be good if the order was not defined because that would
> prevent people depending on it, so making it easier for a compiler to
> parallelize.
But then the language should define pure functions (relatively to the given
context) and prohibit usage of impure ones in the constructs like above.
>>> However, we would be able to write
>>
>>> (for I in reverse A'Range => A(I))
>>
>>> to represent the reverse of the array A is perhaps a little confusing.
>>
>> The effect is undefined. Theoretically the compiler could initialize array
>> elements concurrently on a multi-core processor.
>
> There are really two concepts here:
> 1. the order of evaluation of the expressions for each index
> 2. the value the bound variable I gets for each index
>
> I didn't make it clear that I was switching from [1] to [2], sorry.
> This above reverse example was really about [2] to show that the use
> of the keyword 'reverse' would result in I having the value A'Last at
> index A'First, A'Last - 1 at index A'First + 1, etc.
OK. The objection is that in this case I is not the array's index, but a
mapping of. That looks totally obscure.
>>> Also, it really only makes sense to have one variable holding the
>>> array index. For example, if we could write
>>
>>> (I, J : 1 .. 5 => ...)
>>
>>> surely I and J would always be equal: there are only 5 elements in the
>>> array. Having
>>
>>> (for I in 1 .. 5 => ...)
>>
>>> syntactically rules out multiple variables.
>>
>> Yes, but many other things as well. However I prefer an absolutely
>> different approach anyway, e.g. proper index types. In my world a diagonal
>> would be initialized like:
>>
>> (Diagonal (5, 5) => 1.0, others => 0.0)
>>
>> where Diagonal is a proper function.
>
> Interesting.. how would you make the expression a function of the
> index?
I don't want such expressions at all. I mean if these are necessary it must
be a function returning an array. Reading aggregates containing some
inlined code is not readable to me.
This is yet another topic, but I favor user-defined aggregates instead of
hard coded special stuff like index dependent expressions. E.g. if you have
some frequently used special type of "array literals" you should be able
to provide a custom aggregate of. For example, let you deal with band
matrices. The language should allow you to define a custom aggregate like
A : Square_Matrix :=
( Upper => (1.0, 2.4),
Diagonal => (7.3, 8.0, 9.1),
Lower => (3.0, 2.1) );
P.S. This issue boils down to the interfaces. The point is that you should
be able to implement interface of any type for the given one. A record of
arrays is an interface which has aggregates like above. Hang it on
Square_Matrix and you will be able to do above aggregates and other useful
stuff, like A.Upper.