Press Release - Ada 2012 Language Standard Approved by ISO

Press Release - Ada 2012 Language Standard Approved by ISO

[Dirk Craeynest]

FOR IMMEDIATE RELEASE

Ada 2012 Language Standard Approved by ISO

Language revision adds contract-based programming, multicore support,
and other advanced features


GENEVA, Switzerland, December 18, 2012 - The Ada Resource Association
(ARA) and Ada-Europe today announced the approval and publication of
the latest version of the Ada programming language by the Geneva-based
International Organization for Standardization (ISO).  The language
revision, known as Ada 2012, was under the auspices of ISO/IEC
JTC1/SC22/WG9 and was conducted by the Ada Rapporteur Group (ARG)
subunit of WG9, with sponsorship in part from the ARA and Ada-Europe.
The formal approval of the standard was issued on November 20 by
ISO/IEC JTC 1, and the standard was published on December 15.

Ada 2012 brings significant enhancements to Ada, most notably in the
area of "contract-based programming."  New features here include the
ability to specify preconditions and postconditions for subprograms,
and invariants for private (encapsulated) types.  These take the form
of Boolean expressions that can be interpreted (under programmer
control) as run-time conditions to be checked.  The contract-based
programming features fit in smoothly with Ada's Object-Oriented
Programming model, and support the type substitutability guidance
supplied in the Object-Oriented Technologies and Related Techniques
Supplement (DO-332) to the new avionics software safety standard
DO-178C / ED-12C.

Other new features in Ada 2012 include enhancements to the containers
library, additional expressiveness through features such as conditional
expressions and more powerful iterators, and support for multicore
platforms (task affinities, and the extension of the Ravenscar profile
- standardized in Ada 2005 as an efficient and predictable tasking
subset for high-integrity real-time systems - to multiprocessor and
multicore environments).

A technical summary of Ada 2012, together with an explanation of
the language's benefits and a set of links to further information,
is available at www.ada2012.org, a website maintained by the Ada
Resource Association.

"Ada 2012 is a major advance in the state of the art in programming
languages," said Dr. Edmond Schonberg, Rapporteur of the ARG.
"The new features answer real user needs, and help cement Ada's
reputation as a language of choice for systems where reliability,
safety, and security are paramount."

"I would like to give special thanks to Randy Brukardt for his
editorial work on the Language Reference Manual, to Ed Schonberg
and the Ada Rapporteur Group (ARG) for their excellent work in
developing the language revision, and to all members of WG 9 in
producing a quality document that achieved unanimous approval from
our parent organization," said Dr. Joyce Tokar, Convenor of WG9.
"Ada 2012 is a significant technical accomplishment."

With the growing complexity of software systems in most aspects of
our daily professional and personal life, program correctness is a
paramount concern.  Ada 2012 provides outstanding solutions to that
end, which can be applied both in industry for production software
development, and in academia for teaching and research.


About the Ada Resource Association

The Ada Resource Association (ARA) is a non-profit organization
chartered to support the continued evolution of the Ada language and
its infrastructure, to serve as a source of information about Ada and
its usage, and to promote Ada as a language for effective software
engineering.  To these ends the ARA maintains the Ada Information
Clearinghouse website www.adaic.org and has provided funding for the
development and maintenance of the Ada language standard and the Ada
Conformance Assessment Test Suite.  For information about the ARA,
including sponsorship opportunities, please visit www.adaresource.com.
The ARA is headquartered in Oakton, VA (US).


About Ada-Europe

Ada-Europe is the international non-profit organization that
promotes the knowledge and use of the Ada programming language in
academia, research and industry in Europe.  Its flagship event is the
annual international conference on reliable software technologies, a
high-quality technical and scientific event that has been successfully
running in the current format for the last 17 years.  Ada-Europe has
member organizations all over the continent, in Belgium, Denmark,
France, Germany, Spain, Sweden, and Switzerland, as well as individual
members in many other countries.  For information about Ada-Europe,
its charter, activities and sponsors, please visit: www.ada-europe.org.
Ada-Europe is headquartered in Brussels, Belgium.

A PDF version of this press release is available at www.ada-europe.org.


Organization Contacts

Ada Resource Association
Ben Brosgol, ARA President
brosgol@adacore.com

Ada-Europe
Tullio Vardanega, Ada-Europe President
president@ada-europe.org


Press Contacts

Ada Resource Association
Jessie Glockner, Rainier Communications
Tel: +1-508-475-0025 x140
jglockner@rainierco.com
http://twitter.com/JessieGlockner

Ada-Europe
Dirk Craeynest, Ada-Europe Vice-president
c/o KU Leuven, Department of Computer Science
dirk.craeynest@cs.kuleuven.be

(Ada2012.1)

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Robert A Duff]

dirk@vana.cs.kuleuven.be. (Dirk Craeynest) writes:

> Ada 2012 brings significant enhancements to Ada, most notably in the
> area of "contract-based programming."  New features here include the
> ability to specify preconditions and postconditions for subprograms,
> and invariants for private (encapsulated) types.

Why does everybody neglect predicates, which are more important
than pre/post/invariant?

- Bob

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Bill Findlay]

On 18/12/2012 16:57, in article wcc8v8vti17.fsf@shell01.TheWorld.com,
"Robert A Duff" <bobduff@shell01.TheWorld.com> wrote:

> dirk@vana.cs.kuleuven.be. (Dirk Craeynest) writes:
> 
>> Ada 2012 brings significant enhancements to Ada, most notably in the
>> area of "contract-based programming."  New features here include the
>> ability to specify preconditions and postconditions for subprograms,
>> and invariants for private (encapsulated) types.
> 
> Why does everybody neglect predicates, which are more important
> than pre/post/invariant?

A bit of fun with a predicate:

-- compile with gnatmake -gnat12la pn.adb
with Ada.Text_IO;
use  Ada.Text_IO;

procedure pn is

   type candidate is range 1 .. 2**30;

   function is_prime (nr : candidate) return Boolean is
      n : constant candidate := nr;
      j :          candidate;
   begin
      if n < 2 then return False; end if;
      for d in candidate range 2..3 loop
         if n = d then
            return True;
         elsif n mod d = 0 then
            return False;
         end if;
      end loop;
      j := 5;             -- j = 6k-1, k = 1
      loop
         if n mod j = 0 then
            return False;
         end if;
         j := j + 2;      -- j = 6k+1
      exit when j >= n;
         if n mod j = 0 then
            return False;
         end if;
         j := j + 4;      -- j = 6k+5 = 6k'-1, k' = k+1
      exit when j >= n;
      end loop;
      return True;
   end is_prime;

   -- The following exemplifies a couple of new features in Ada 2012,
   --    namely predicates on subtypes,
   --       and conditional expressions (redux, after Algol 60).

   -- Only prime numbers can be successfully assigned to this subtype.
   subtype prime_number is candidate
      with Dynamic_Predicate => is_prime(prime_number);

   OK : constant prime_number := 31;  -- 31 is prime
   KO :          prime_number := 19;  -- 19 is prime

begin
   Put_Line(candidate'Image(OK) &
            (if is_prime(OK) then " is" else " is not") & " a prime");
   Flush;
   KO := 32;  -- 32 is NOT prime, so this should raise an exception!
   Put_Line(candidate'Image(OK) &
            (if is_prime(KO) then " is" else " is not") & " a prime");
   Flush;
exception
   when others =>
      Put_Line("KO was" &
               (if KO = 19 then " NOT" else " WRONGLY") & " set to 32");
      Flush;
end pn;


-- 
Bill Findlay
with blueyonder.co.uk;
use  surname & forename;

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Jeffrey Carter]

On 12/18/2012 02:12 PM, Bill Findlay wrote:
>
>        exit when j >= n;
...
>        exit when j >= n;

Can't these exit when j > n / 2?

-- 
Jeff Carter
"Friends don't let friends program in C++"
Zalman Stern
114

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Bill Findlay]

On 18/12/2012 21:36, in article kaqnkc$5df$1@dont-email.me, "Jeffrey Carter"
<spam.jrcarter.not@spam.not.acm.org> wrote:

> On 12/18/2012 02:12 PM, Bill Findlay wrote:
>> 
>>        exit when j >= n;
> ...
> 
>>        exit when j >= n;
> 
> Can't these exit when j > n / 2?

Or, better, j > sqrt(n), but I was not trying very hard to be efficient.

-- 
Bill Findlay
with blueyonder.co.uk;
use  surname & forename;

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Randy Brukardt]

"Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message
news:wcc8v8vti17.fsf@shell01.TheWorld.com...
> dirk@vana.cs.kuleuven.be. (Dirk Craeynest) writes:
>
>> Ada 2012 brings significant enhancements to Ada, most notably in the
>> area of "contract-based programming."  New features here include the
>> ability to specify preconditions and postconditions for subprograms,
>> and invariants for private (encapsulated) types.
>
> Why does everybody neglect predicates, which are more important
> than pre/post/invariant?

No idea. Perhaps it is because only "old Ada hands" really grok the idea of
a constrained subtype, and a predicate is just a constraint on steroids
(well, a more general constraint). For people that don't understand the
power of constraints, extending them seems pointless. (Or maybe its just an
oversight by the people who wrote that press release - I didn't notice the
fact it was missing when I skimmed a draft last week.)

                                                         Randy.

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Dmitry A. Kazakov]

On Tue, 18 Dec 2012 21:12:25 +0000, Bill Findlay wrote:

> On 18/12/2012 16:57, in article wcc8v8vti17.fsf@shell01.TheWorld.com,
> "Robert A Duff" <bobduff@shell01.TheWorld.com> wrote:
> 
>> dirk@vana.cs.kuleuven.be. (Dirk Craeynest) writes:
>> 
>>> Ada 2012 brings significant enhancements to Ada, most notably in the
>>> area of "contract-based programming."  New features here include the
>>> ability to specify preconditions and postconditions for subprograms,
>>> and invariants for private (encapsulated) types.
>> 
>> Why does everybody neglect predicates, which are more important
>> than pre/post/invariant?
> 
> A bit of fun with a predicate:
[...]

Take an instance of Ada.Numerics.Discrete_Random and do:

   subtype More_Fun_Number is Integer with
      Dynamic_Predicate => Random = More_Fun_Number;

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

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Georg Bauhaus]

On 19.12.12 00:24, Randy Brukardt wrote:
> "Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message
> news:wcc8v8vti17.fsf@shell01.TheWorld.com...

>> Why does everybody neglect predicates, which are more important
>> than pre/post/invariant?
>
> No idea. Perhaps it is because only "old Ada hands" really grok the idea of
> a constrained subtype, and a predicate is just a constraint on steroids
> (well, a more general constraint).

Being a function, maybe the power of a predicate is at first easier
to see by a "functional" programmer, who is used to predicates?

There is a need for a killer example, then. Maybe an algorithm that
approximates some complex result with the help of failing predicates.

For example, finding two primes related in a certain way
with the help of tasks while predicates steer the computation.

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Georg Bauhaus]

On 19.12.12 09:33, Dmitry A. Kazakov wrote:

> Take an instance of Ada.Numerics.Discrete_Random and do:
>
>     subtype More_Fun_Number is Integer with
>        Dynamic_Predicate => Random = More_Fun_Number;
>

You could use

    subtype More_Fun_Number is Integer with
      Dynamic_Predicate => At_Least_A_Thousand
                              (Random (G), More_Fun_Number);

to test whether or not your random number generator is, say,
dodging at least 1_000 numbers that your algorithm happens
to produce, and assign, in a predictable way.

This approach doesn't seem so wrong in case one cannot know
the result in advance, but operation of the program critically
depends on certain properties of those unknown parts.

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Dmitry A. Kazakov]

On Wed, 19 Dec 2012 09:35:56 +0100, Georg Bauhaus wrote:

> On 19.12.12 00:24, Randy Brukardt wrote:
>> "Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message
>> news:wcc8v8vti17.fsf@shell01.TheWorld.com...
> 
>>> Why does everybody neglect predicates, which are more important
>>> than pre/post/invariant?
>>
>> No idea. Perhaps it is because only "old Ada hands" really grok the idea of
>> a constrained subtype, and a predicate is just a constraint on steroids
>> (well, a more general constraint).
> 
> Being a function, maybe the power of a predicate is at first easier
> to see by a "functional" programmer, who is used to predicates?

Power? Types are not supposed to solve [functional] problems, algorithms
are.

The purpose of typing is bringing structure and safety (so abstraction,
encapsulation, correctness checks etc, everything strictly non-functional).
Do dynamic predicates this? I doubt that very much.
 
> There is a need for a killer example, then. Maybe an algorithm that
> approximates some complex result with the help of failing predicates.

What sort of design should this promote? One that relies on catching
exceptions from dynamic checks? Whom is that supposed to kill? The
programmer? (:-))

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

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Dmitry A. Kazakov]

On Wed, 19 Dec 2012 10:00:57 +0100, Georg Bauhaus wrote:

> On 19.12.12 09:33, Dmitry A. Kazakov wrote:
> 
>> Take an instance of Ada.Numerics.Discrete_Random and do:
>>
>>     subtype More_Fun_Number is Integer with
>>        Dynamic_Predicate => Random = More_Fun_Number;
> 
> You could use
> 
>     subtype More_Fun_Number is Integer with
>       Dynamic_Predicate => At_Least_A_Thousand
>                               (Random (G), More_Fun_Number);
> 
> to test whether or not your random number generator is, say,
> dodging at least 1_000 numbers that your algorithm happens
> to produce, and assign, in a predictable way.
> 
> This approach doesn't seem so wrong in case one cannot know
> the result in advance, but operation of the program critically
> depends on certain properties of those unknown parts.

It is deeply wrong. A [sub]type should describe some class of entities
sharing common properties and behavior.

P.S. It is frequently said that Ada cannot not prevent you from shooting
yourself in the foot. But not with a bazooka...

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

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Georg Bauhaus]

On 19.12.12 10:19, Dmitry A. Kazakov wrote:
> It is deeply wrong. A [sub]type should describe some class of entities
> sharing common properties and behavior.

If properties and behavior are functions of physical time,
how does a [sub]type describe the class of corresponding entities?

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Dmitry A. Kazakov]

On Wed, 19 Dec 2012 10:21:51 +0100, Georg Bauhaus wrote:

> On 19.12.12 10:19, Dmitry A. Kazakov wrote:
>> It is deeply wrong. A [sub]type should describe some class of entities
>> sharing common properties and behavior.
> 
> If properties and behavior are functions of physical time,
> how does a [sub]type describe the class of corresponding entities?

They are not.

The whole idea of typing is to abstract/define/describe properties
invariant to the program state (and time, and space). They exist before and
after the program, and so are independent on whether the program is correct
(has bugs), runs, exists. This in turn allows you to design software
components independently, to have contracts, to test components before
deployment, to verify and validate components.

Things that change with time and space are not types. They are called
variables, objects etc.

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

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Georg Bauhaus]

On 19.12.12 10:38, Dmitry A. Kazakov wrote:
> On Wed, 19 Dec 2012 10:21:51 +0100, Georg Bauhaus wrote:
> 
>> On 19.12.12 10:19, Dmitry A. Kazakov wrote:
>>> It is deeply wrong. A [sub]type should describe some class of entities
>>> sharing common properties and behavior.
>>
>> If properties and behavior are functions of physical time,
>> how does a [sub]type describe the class of corresponding entities?
> 
> They are not.
> 
> The whole idea of typing is to abstract/define/describe properties
> invariant to the program state (and time, and space).

Programmers writing in language Qi might disagree, since their
programs can compute types.

In any case, if a program lets me know whether some predicate
is true for a series of object's states, it gives me a set of
values, filtered, that may be good for making the type more precise
during the next run. Attaching the Dynamic_Predicate as a subtype
constraint draws attention to it; the predicate might otherwise
be hidden in some all too ordinary conditional (no abstraction),
indistinguishable from Boolean functions. A programmer might
prefer to provide a more explicit mechanism for checking, though,
such as by defining an abstract type Filtered, with suitable
operations that triggered when now Dynamic_Predicate is triggered.

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Bill Findlay]

On 19/12/2012 08:33, in article 7wrdmbre6jw9.qww9l0uzj6mg.dlg@40tude.net,
"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:

> On Tue, 18 Dec 2012 21:12:25 +0000, Bill Findlay wrote:
> 
>> On 18/12/2012 16:57, in article wcc8v8vti17.fsf@shell01.TheWorld.com,
>> "Robert A Duff" <bobduff@shell01.TheWorld.com> wrote:
>> 
>>> dirk@vana.cs.kuleuven.be. (Dirk Craeynest) writes:
>>> 
>>>> Ada 2012 brings significant enhancements to Ada, most notably in the
>>>> area of "contract-based programming."  New features here include the
>>>> ability to specify preconditions and postconditions for subprograms,
>>>> and invariants for private (encapsulated) types.
>>> 
>>> Why does everybody neglect predicates, which are more important
>>> than pre/post/invariant?
>> 
>> A bit of fun with a predicate:
> [...]
> 
> Take an instance of Ada.Numerics.Discrete_Random and do:
> 
>    subtype More_Fun_Number is Integer with
>       Dynamic_Predicate => Random = More_Fun_Number;

Now that IS funnny!

-- 
Bill Findlay
with blueyonder.co.uk;
use  surname & forename;

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
news:7wrdmbre6jw9.qww9l0uzj6mg.dlg@40tude.net...
...
> Take an instance of Ada.Numerics.Discrete_Random and do:
>
>   subtype More_Fun_Number is Integer with
>      Dynamic_Predicate => Random = More_Fun_Number;

A predicate (or any contract) that can get different answers on successive
calls is *wrong*. Ada 2012 has a permission (11.4.2(27/3)) for
implementations to reject such expressions if they can detect it. (This
isn't required simply because we don't know of any way to characterize what
should not be allowed -- that's a work item for future versions of Ada.)

One would hope that obvious cases like this take advantage of the permission
and are rejected outright.

Functions in dynamic predicates (and all of the other contract aspects, as
well) ought to be logically pure, returning the same result for the same
parameter values.

                                         Randy.

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Anh Vo]

<< On Tuesday, December 18, 2012 1:12:25 PM UTC-8, Bill Findlay wrote:
> On 18/12/2012 16:57, in article wcc8v8vti17.fsf@shell01.TheWorld.com, "Robert A Duff" <bobduff@shell01.TheWorld.com> wrote: > dirk@vana.cs.kuleuven.be. (Dirk Craeynest) writes: > >> Ada 2012 brings significant enhancements to Ada, most begin 
   Put_Line(candidate'Image(OK) & (if is_prime(OK) then " is" else " is not") & " a prime"); 
   Flush;
   KO := 32; -- 32 is NOT prime, so this should raise an exception!
   Put_Line(candidate'Image(OK) & (if is_prime(KO) then " is" else " is not") & " a prime"); >>

Did you mean KO in place of the first occurrence of OK on the line immediately above?

A. Vo

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Bill Findlay]

On 20/12/2012 21:55, in article
5c4f3590-3fe7-41ef-8e3f-182c08576761@googlegroups.com, "Anh Vo"
<anhvofrcaus@gmail.com> wrote:

> << On Tuesday, December 18, 2012 1:12:25 PM UTC-8, Bill Findlay wrote:
>> On 18/12/2012 16:57, in article wcc8v8vti17.fsf@shell01.TheWorld.com, "Robert
>> A Duff" <bobduff@shell01.TheWorld.com> wrote: > dirk@vana.cs.kuleuven.be.
>> (Dirk Craeynest) writes: > >> Ada 2012 brings significant enhancements to
>> Ada, most begin 
>    Put_Line(candidate'Image(OK) & (if is_prime(OK) then " is" else " is not")
> & " a prime"); 
>    Flush;
>    KO := 32; -- 32 is NOT prime, so this should raise an exception!
>    Put_Line(candidate'Image(OK) & (if is_prime(KO) then " is" else " is not")
> & " a prime"); >>
> 
> Did you mean KO in place of the first occurrence of OK on the line immediately
> above?

Yes. 
8-)

-- 
Bill Findlay
with blueyonder.co.uk;
use  surname & forename;

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Dmitry A. Kazakov]

On Wed, 19 Dec 2012 19:52:33 -0600, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:7wrdmbre6jw9.qww9l0uzj6mg.dlg@40tude.net...
> ...
>> Take an instance of Ada.Numerics.Discrete_Random and do:
>>
>>   subtype More_Fun_Number is Integer with
>>      Dynamic_Predicate => Random = More_Fun_Number;
> 
> A predicate (or any contract) that can get different answers on successive
> calls is *wrong*. Ada 2012 has a permission (11.4.2(27/3)) for
> implementations to reject such expressions if they can detect it. (This
> isn't required simply because we don't know of any way to characterize what
> should not be allowed -- that's a work item for future versions of Ada.)
> 
> One would hope that obvious cases like this take advantage of the permission
> and are rejected outright.

People will readily misuse predicates, that is for sure. The bugs
introduced by dynamic checks are extremely difficult to track down.

> Functions in dynamic predicates (and all of the other contract aspects, as
> well) ought to be logically pure, returning the same result for the same
> parameter values.

Well, in my view there are only two purposes for type constraining. Both
are closely related:

1. Elimination of checks, that is when T'Class is constrained to specific a
S, so that dispatch became static, or when subtype Index is declared with
the range A'Range where A is an array etc. ["constant T" and "in T" fall
into this category, they disallow mutators eliminating checks that a
variable is not updated]

2. Influencing representation, e.g. setting bounds of an unconstrained
array, selecting variant of a record.

In essence 1 and 2 are about knowing something statically, during
compilation. Not necessarily the constraint itself, which may be dynamic,
yet allowing to prove something statically, e.g. that array index is always
within the bounds.

I don't see how predicates might be helpful for either 1 or 2.

   subtype Even is Positive with Dynamic_Predicate => Even mod 2 = 0;
   subtype Each_Second_Character is String (Even);

won't work. What I see is a yet another way to pack implementations into
declarations as Georg promptly suggested, a slippery slope...

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

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Georg Bauhaus]

On 21.12.12 10:01, Dmitry A. Kazakov wrote:
> What I see is a yet another way to pack implementations into
> declarations as Georg promptly suggested, a slippery slope...

Operational aspects of definitions, and assignments---similar to
Adjust, Initialize, or Finalize---turn a static, flat plane of
non-operational definitions into something that a programmer can
work with, because it responds to his or her efforts at
definitions. The programmer is important here, not necessarily
the program, not yet.  At a stage when programmers have no
complete understanding of the program yet, as is usually the case
outside theaters, what means of programming are better than
nothing at all?

So, constraints, Dynamic_Predictes, may have one or two other uses.

The barium platino-cyanide paper on R�ntgen's workbench was just
an aspect, at run-time. It was not deliberately a part of his
programmed experiment. It turned into an important aspect though,
because it made R�ntgen notice something, at run-time.

"And what did you think?"

"I did not think; I investigated. I assumed that the effect must
  have come from the tube, since its character indicated that it
  could come from nowhere else. I tested it.  In a few minutes
  there was no doubt about it."

R�ntgen had not even planned for paper laying there. Yet, had the
black line across the paper not revealed an aspect, one for which
he did not have proper abstractions, he would not have found X rays.

It seems foolish to assume that, during program development,
we just follow perfect notions of what we have to do.
Two programmers sitting in the corner knowing everything
about the program they intend to write---only in a pipe dream.

Consequently, placing assumptions with definitions seems an
honest thing to do. It does not kill other ways of expressing our
knowledge. It does not require that we remove parts of a later
program once they become unnecessary.

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Georg Bauhaus]

On 21.12.12 11:13, Georg Bauhaus wrote:
> It does not require that we remove parts of a later
> program once they become unnecessary.

The sentence is missing a "not".

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Dmitry A. Kazakov]

On Fri, 21 Dec 2012 11:13:38 +0100, Georg Bauhaus wrote:

> On 21.12.12 10:01, Dmitry A. Kazakov wrote:
>> What I see is a yet another way to pack implementations into
>> declarations as Georg promptly suggested, a slippery slope...
> 
> It seems foolish to assume that, during program development,
> we just follow perfect notions of what we have to do.

Still there exists a framework within which development is to be made: from
the laws of logic and physics to the language being used, i.e. Ada in this
case. The framework is fixed, not debatable, independent on the process of
development. At no stage of program development the laws of logic are
questioned.

From the POV of SW development techniques Ada is supposed to facilitate,
implementations must be separated from interfaces. This is given.

> Consequently, placing assumptions with definitions seems an
> honest thing to do. It does not kill other ways of expressing our
> knowledge.

Assumption is not knowledge if not used somewhere. It is not implementation
and so it may not have any logical run-time effect. You assume certain
things which are considered true for the program as a whole. They cannot be
evaluated by the program itself without running into a contradiction. They
could be "evaluated" (logical inference is the term) by another program
(e.g. compiler) or human (e.g. programmer).

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

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:14oqoq06zhlu2.tcasif3hdyhw.dlg@40tude.net...
...
> In essence 1 and 2 are about knowing something statically, during
> compilation. Not necessarily the constraint itself, which may be dynamic,
> yet allowing to prove something statically, e.g. that array index is 
> always
> within the bounds.

Well, I obviously disagree about that. Constraints, in my view are all about 
*introducing* checks. Predicates just provide an extension of that.

> I don't see how predicates might be helpful for either 1 or 2.

I don't see how range constraints would be helpful for either 1 or 2.

>   subtype Even is Positive with Dynamic_Predicate => Even mod 2 = 0;
>   subtype Each_Second_Character is String (Even);
>
> won't work. What I see is a yet another way to pack implementations into
> declarations as Georg promptly suggested, a slippery slope...

You believe checks are part of the implementation, while I believe that they 
are something separate. There is is no real hope of agreement on that, so I 
fear there isn't much point in discussing it. But I'll try for a moment...

Checks, in my view, are things that should never fail in a correct program. 
Thus, they should not be considered part of the implementation; they're 
something separate. Indeed, the only reason that they are made dynamically 
is because checking them statically is beyond the current state of the art. 
(I would hope that by the time the next version of Ada rolls around, that 
will no longer be true.)

Your argument about them being part of the implementation comes from the 
fact that Ada confuses the role of exceptions and handlers that come from 
checks vs. those that are part of the semantics (like End_Error). IMHO, it's 
wrong to be handling exceptions raised by checks; these represent bugs and 
must be eliminated from the program, not handled. (Handling them just covers 
up bugs.) For Ada 2012, you can differentiate exceptions somewhat by what is 
present in constract aspects (preconditions, predicates, etc.) - which 
always represent checks, but of course that's not quite complete. And there 
is a similar problem for handlers: there are "last chance" handlers (which 
capture all exceptions outbound), these aren't clearly separated from those 
handlers which are semantic in nature. Last chance handlers are necessary 
for all exits, of course, but they have nothing to do with the failed check 
(the check remains failed at the end of such a handler) . (GNAT does this 
better with their "at end" handler, but of course that's not Ada.) These are 
language flaws, not fundamental to the model.

In an ideal world, all of these "checks" will get made statically. Hopefully 
that's coming. In mean time, it's important to get programmers used to the 
idea of writing checks this way, so that future tools can make the checks 
statically (there is no hope of making checks statically if they are just 
written in natural language comments).

                                     Randy.

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Dmitry A. Kazakov]

On Fri, 21 Dec 2012 19:40:57 -0600, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:14oqoq06zhlu2.tcasif3hdyhw.dlg@40tude.net...
> ...
>> In essence 1 and 2 are about knowing something statically, during
>> compilation. Not necessarily the constraint itself, which may be dynamic,
>> yet allowing to prove something statically, e.g. that array index is 
>> always within the bounds.
> 
> Well, I obviously disagree about that. Constraints, in my view are all about 
> *introducing* checks. Predicates just provide an extension of that.

We mean different "checks" here. As you have explained below, you mean a
"true" check, a thing that never fails. I meant a dynamic check, a thing
that is not statically true and need to be approached in the implementation
according to the outcome. That evil thing is to be eliminated by
introducing good things, "true checks."

>> I don't see how predicates might be helpful for either 1 or 2.
> 
> I don't see how range constraints would be helpful for either 1 or 2.

   procedure Foo (S : String) is
      subtype I is Integer range S'Range;

>>   subtype Even is Positive with Dynamic_Predicate => Even mod 2 = 0;
>>   subtype Each_Second_Character is String (Even);
>>
>> won't work. What I see is a yet another way to pack implementations into
>> declarations as Georg promptly suggested, a slippery slope...
> 
> You believe checks are part of the implementation, while I believe that they 
> are something separate. There is is no real hope of agreement on that, so I 
> fear there isn't much point in discussing it. But I'll try for a moment...
> 
> Checks, in my view, are things that should never fail in a correct program. 
> Thus, they should not be considered part of the implementation; they're 
> something separate. Indeed, the only reason that they are made dynamically 
> is because checking them statically is beyond the current state of the art. 
> (I would hope that by the time the next version of Ada rolls around, that 
> will no longer be true.)
> 
> Your argument about them being part of the implementation comes from the 
> fact that Ada confuses the role of exceptions and handlers that come from 
> checks vs. those that are part of the semantics (like End_Error). IMHO, it's 
> wrong to be handling exceptions raised by checks; these represent bugs and 
> must be eliminated from the program, not handled. (Handling them just covers 
> up bugs.) For Ada 2012, you can differentiate exceptions somewhat by what is 
> present in constract aspects (preconditions, predicates, etc.) - which 
> always represent checks, but of course that's not quite complete. And there 
> is a similar problem for handlers: there are "last chance" handlers (which 
> capture all exceptions outbound), these aren't clearly separated from those 
> handlers which are semantic in nature. Last chance handlers are necessary 
> for all exits, of course, but they have nothing to do with the failed check 
> (the check remains failed at the end of such a handler) . (GNAT does this 
> better with their "at end" handler, but of course that's not Ada.) These are 
> language flaws, not fundamental to the model.

Ah, but we are in a full agreement here.

What I said was: IF a "check" is dynamic THEN that must be an
implementation. Since a true check may not fail. Then a fluttering "check"
is something else. Bug, or an intended behavior, it is a part of the
implementation.

> In an ideal world, all of these "checks" will get made statically. Hopefully 
> that's coming. In mean time, it's important to get programmers used to the 
> idea of writing checks this way, so that future tools can make the checks 
> statically (there is no hope of making checks statically if they are just 
> written in natural language comments).

OK, this is rather a tactical disagreement then. Ada's stance was
conservative, not eager adding features impossible to implement properly.
Because somebody (Georg) could readily base his design on the faulty.

In the first step I would rather prefer means to declare user-defined
operations pure, context-dependent pure, compile-time evaluated etc. This
would be more universal than mere predicates, and "proper" predicates would
require that stuff anyway. An alternative, letting the compiler/vendor to
deduce such properties, is IMO unrealistic (an undecidable problem, I
think).

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

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Georg Bauhaus]

On 22.12.12 10:02, Dmitry A. Kazakov wrote:

>> In an ideal world, all of these "checks" will get made statically. Hopefully
>> that's coming. In mean time, it's important to get programmers used to the
>> idea of writing checks this way, so that future tools can make the checks
>> statically (there is no hope of making checks statically if they are just
>> written in natural language comments).
>
> OK, this is rather a tactical disagreement then. Ada's stance was
> conservative, not eager adding features impossible to implement properly.

Rather, history tells that Ada has been seen by some as being just a little
less improperly adventurous than Algol 68.

> Because somebody (Georg) could readily base his design on the faulty.

Don't worry, my predicates tend to be pure, are used for debugging,
and can be turned off/removed/left as documentation once the proofs
have been checked. (Letting them stay can be a Good Thing if you need
to prepare for the usual uncoordinated multi-player refactorings and
quick fixes.)

The expressions don't have significant effects as measured by the purpose
of the programs. For example, they may interrupt the normal flow, like
explicit tests, they will send a mail message with some state information
in it and ask for an optional user report. These reports are extremely helpful.

Checks can be written as if there was monitoring hardware, hence as
if they did not even have a way of toggling any of the program's bits.

> In the first step I would rather prefer means to declare user-defined
> operations pure, context-dependent pure, compile-time evaluated etc. This
> would be more universal than mere predicates, and "proper" predicates would
> require that stuff anyway. An alternative, letting the compiler/vendor to
> deduce such properties, is IMO unrealistic (an undecidable problem, I
> think).

Right, and I would like to learn what kind of restrictions Randy
is having in mind that will let compilers evaluate more expressions at
compile time.

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Dmitry A. Kazakov]

On Sat, 22 Dec 2012 23:38:21 +0100, Georg Bauhaus wrote:

> On 22.12.12 10:02, Dmitry A. Kazakov wrote:
> 
>>> In an ideal world, all of these "checks" will get made statically. Hopefully
>>> that's coming. In mean time, it's important to get programmers used to the
>>> idea of writing checks this way, so that future tools can make the checks
>>> statically (there is no hope of making checks statically if they are just
>>> written in natural language comments).
>>
>> OK, this is rather a tactical disagreement then. Ada's stance was
>> conservative, not eager adding features impossible to implement properly.
> 
> Rather, history tells that Ada has been seen by some as being just a little
> less improperly adventurous than Algol 68.

No, it is not same. Ada 83 compiler was difficult to build (then),
especially on a small machine, but there was little doubt about
practicability.

>> Because somebody (Georg) could readily base his design on the faulty.
> 
> Don't worry, my predicates tend to be pure, are used for debugging,
> and can be turned off/removed/left as documentation once the proofs
> have been checked. (Letting them stay can be a Good Thing if you need
> to prepare for the usual uncoordinated multi-player refactorings and
> quick fixes.)
> 
> The expressions don't have significant effects as measured by the purpose
> of the programs. For example, they may interrupt the normal flow, like
> explicit tests, they will send a mail message with some state information
> in it and ask for an optional user report. These reports are extremely helpful.
> 
> Checks can be written as if there was monitoring hardware, hence as
> if they did not even have a way of toggling any of the program's bits.

Actually, in a large project we deploy a similar stuff based GNAT-specific
support for tracing exceptions. It is a 50-50 game. In 50% of cases the bug
is reported by the monitor. In other 50% it causes a cascade of errors in
the monitor itself and around it, makes finding the cause more difficult
than without the monitor.

I think much, if mot all, boils down to exceptions, because it is
practically impossible to ensure safety of controlled objects against
unanticipated exceptions. It is non-testable and much too complicated for a
programmer to gasp. Contracted exceptions is an urgent need.

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

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Shark8]

On Sunday, December 23, 2012 2:08:53 AM UTC-6, Dmitry A. Kazakov wrote:
> 
>  Contracted exceptions is an urgent need.

There are contracted exceptions, of a sort -- the LRM guarantees that the predefined relational operator will not raise an exception and the predefined operators on integers will only raise NUMERIC_ERROR ( http://archive.adaic.com/standards/83lrm/html/lrm-04-05.html ) -- of course that's an external contract.

The ability to have such guarantees applied to the programer's Ada text would indeed be a boon; perhaps using an aspect of the following form:
   Exceptions => [ NOT NULL | NULL | "EXCEPTION_NAME"[, OR "EXCEPTION_NAME"]]

Where EXCEPTION_NAME would map to either predefined exceptions or visible user-defined exceptions, NULL would assert that the procedure raises no exceptions, and NOT NULL would be what we have now (subprogram can raise any exception).

The problem with the above is that there's some exceptions which are dependent on the [executing] environment at Run-time (STORAGE_ERROR springs to mind).

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[sbelmont700]

On Sunday, December 23, 2012 6:38:21 PM UTC-5, Shark8 wrote:
> On Sunday, December 23, 2012 2:08:53 AM UTC-6, Dmitry A. Kazakov wrote:
> 
> > 
> 
> >  Contracted exceptions is an urgent need.
> 
> 
> 
> There are contracted exceptions, of a sort -- the LRM guarantees that the predefined relational operator will not raise an exception and the predefined operators on integers will only raise NUMERIC_ERROR ( http://archive.adaic.com/standards/83lrm/html/lrm-04-05.html ) -- of course that's an external contract.
> 
> 
> 
> The ability to have such guarantees applied to the programer's Ada text would indeed be a boon; perhaps using an aspect of the following form:
> 
>    Exceptions => [ NOT NULL | NULL | "EXCEPTION_NAME"[, OR "EXCEPTION_NAME"]]
> 
> 
> 
> Where EXCEPTION_NAME would map to either predefined exceptions or visible user-defined exceptions, NULL would assert that the procedure raises no exceptions, and NOT NULL would be what we have now (subprogram can raise any exception).
> 
> 
> 
> The problem with the above is that there's some exceptions which are dependent on the [executing] environment at Run-time (STORAGE_ERROR springs to mind).

Recall that exception specifications in C++ was a god-awful nightmare, and has since been depreciated.  It makes it nearly impossible to write anything useful, since if subprogram A raises exception E, then any subprogram A calls during its body must also only ever raise E, and it's turtles all the way down.

-sb

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Shark8]

On Sunday, December 23, 2012 8:44:54 PM UTC-6, sbelm...@gmail.com wrote:
>
> 
> Recall that exception specifications in C++ was a god-awful nightmare, and has since been depreciated.  It makes it nearly impossible to write anything useful, since if subprogram A raises exception E, then any subprogram A calls during its body must also only ever raise E, and it's turtles all the way down.

Except that we have a superior language in Ada --  the ability to have nested subprograms can minimize that. Also, the compiler could catch-and-reject any such mistake the programmer makes.  in this regard -- we already do it for Restriction pragmas, right?

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Yannick Duchêne (Hibou57)]

Le Sun, 23 Dec 2012 09:08:53 +0100, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
> Contracted exceptions is an urgent need.

I agree this looks appealing, but Java already have the same and so some  
experiencing with it, and some Java people precisely have arguments  
against it. May be worth to pull their arguments here. One I feel to  
remember, is the exposition of implementation details which indirectly  
comes with it (at least, one of their argument). Indeed, one may argue  
they are the exceptions an implementation raise it self (either to match a  
contract or more freely) and they are the ones its dependencies may raise.  
Some exceptions are under control, some are not. Think about an hardware  
failure during some processing, as an example…

May be the contract, instead of specifying exhaustively what exceptions a  
sub‑program may raises, could instead specify it may raise “this one”, or  
must not raise “this other one”, all other exceptions being of unspecified  
occurrence.

Hope I'm clear enough (not sure to be)


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Dmitry A. Kazakov]

On Mon, 24 Dec 2012 07:44:00 +0100, Yannick Duchêne (Hibou57) wrote:

> Indeed, one may argue  
> they are the exceptions an implementation raise it self (either to match a  
> contract or more freely) and they are the ones its dependencies may raise.

The contract: "I raise if you do" is not an exposition of implementation
details.

Exception contracts must be conditional, that is clear. Otherwise closures
and things like Storage_Error will not work.
  
> Some exceptions are under control, some are not. Think about an hardware  
> failure during some processing, as an example…

Such things (faults) are not exceptions. They raise (if ever) in a context
not affected by the fault. E.g. master task, another partition, OS. There
you can contract them.

> May be the contract, instead of specifying exhaustively what exceptions a  
> sub‑program may raises, could instead specify it may raise “this one”, or  
> must not raise “this other one”, all other exceptions being of unspecified  
> occurrence.

Yes "I raise X" does not imply "I do not raise not X." It is intuitionistic
logic. You have X, a negation of X and a gray area between them. P does not
imply not P.

Furthermore exception contracts must include stuff for which people would
misuse post-conditions and predicates. That is

   sqrt(x) raises Constraint_Error if x < 0
[+ sqrt(x) may not raise Constraint_Error if x >= 0 ]

rather than weaker

   sqrt may raise Constraint_Error =
      = sqrt(x) raises Constraint_Error if <unknown>

Merry Christmas,

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

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Yannick Duchêne (Hibou57)]

Le Mon, 24 Dec 2012 10:02:47 +0100, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

> On Mon, 24 Dec 2012 07:44:00 +0100, Yannick Duchêne (Hibou57) wrote:
>
>> Indeed, one may argue
>> they are the exceptions an implementation raise it self (either to  
>> match a
>> contract or more freely) and they are the ones its dependencies may  
>> raise.
>
> The contract: "I raise if you do" is not an exposition of implementation
> details.
>
> Exception contracts must be conditional, that is clear. Otherwise  
> closures
> and things like Storage_Error will not work.

This one is fine, I see your point now.

> Merry Christmas,
>

Wish you too :) Merry Christmas Dmitry


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Exception contracts for Ada? Was: Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Peter C. Chapin]

On 12/24/2012 06:13 AM, Yannick Duchêne (Hibou57) wrote:

> This one is fine, I see your point now.

Exception contracts are a huge, HUGE topic and one that shouldn't be 
treated too lightly. I can understand their attraction in a language 
that prides itself on its suitability for robust programming. However, 
if exception contracts are ever added to Ada I pray to the Ada gods (the 
ARG?) that it is only done after an extensive review has been made of 
the issues related to them in other languages. One only needs to search 
for the topic of exception specifications in C++ and Java to find a 
mountain of discussion on the subject. Consider:

+ Should exception contracts be enforced statically or dynamically?

+ Should exception contracts be enforced at all or only produce warnings 
or logs?

+ What about backward compatibility with the existing code base? We 
don't want to force people to decorate all code with exception contracts 
before it will compile again with Ada 2020 (or whatever). Do we?

+ Should exception contracts distinguish between "impossible" exceptions 
that shouldn't occur in a correct program (like Constraint_Error) and 
"normal" exceptions that pertain to environmental problems such as 
invalid input data?

+ How should exception contracts interact with generic code?

+ Should exception contracts be a part of a subprogram's type? Consider 
access to subprogram values and their usage.

+ How should exception contracts interact with other static analysis 
techniques? For example if a subprogram has a contract that says it 
might raise exception E, but if static analysis can prove that a 
particular usage will not actually raise E, does the programmer have to 
declare a contract on the calling subprogram about E? One objection I've 
heard about exception specifications in Java is that they require 
programmers to either specify (or handle) exceptions that "clearly" can 
never actually arise at that particular program point.

Now that Ada has preconditions the last point is particularly acute. The 
precondition on a procedure P might guarantee that a called subprogram 
won't raise an exception that it might nevertheless declare in its 
exception contract. It would be really unpleasant if the programmer had 
to also add an exception contract to P stating that it might raise an 
exception that the programmer knows the precondition will prevent!

This is just a sample of some of the issues involved in the subject. 
There are those who have answers for all of these issues. That's great. 
But again I sincerely hope that if exception contracts are ever 
seriously considered for Ada that the matter be given the deep 
consideration it deserves.

Peter

Re: Exception contracts for Ada? Was: Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Dmitry A. Kazakov]

On Mon, 24 Dec 2012 10:49:39 -0500, Peter C. Chapin wrote:

> On 12/24/2012 06:13 AM, Yannick Duch�ne (Hibou57) wrote:
> 
>> This one is fine, I see your point now.
> 
> Exception contracts are a huge, HUGE topic and one that shouldn't be 
> treated too lightly. I can understand their attraction in a language 
> that prides itself on its suitability for robust programming. However, 
> if exception contracts are ever added to Ada I pray to the Ada gods (the 
> ARG?) that it is only done after an extensive review has been made of 
> the issues related to them in other languages. One only needs to search 
> for the topic of exception specifications in C++ and Java to find a 
> mountain of discussion on the subject. Consider:
> 
> + Should exception contracts be enforced statically or dynamically?

Statically. Contracts cannot be enforced dynamically, it is rubbish. What
would a violation of exception contract do? Raise another exception in
violation of what was already violated?

> + Should exception contracts be enforced at all or only produce warnings 
> or logs?

Considering it static, a violation would obviously make the program
illegal, no warnings, no code generated.

> + What about backward compatibility with the existing code base? We 
> don't want to force people to decorate all code with exception contracts 
> before it will compile again with Ada 2020 (or whatever). Do we?

No problem at all. Empty (missing) contract = any exception may propagate.
Everything would be 100% compatible. Moreover, the nice thing is that you
could hang whatever contracts (preserving the functionality, of course) on
the existing legacy libraries (e.g. Ada containers, System etc) while
keeping all legacy code 100% compatible. So long the caller is not
contracted itself it can happily ignore any contracts of the callee.

> + Should exception contracts distinguish between "impossible" exceptions 
> that shouldn't occur in a correct program (like Constraint_Error) and 
> "normal" exceptions that pertain to environmental problems such as 
> invalid input data?

There is no such distinction. A distinction exists between exceptions
required to propagate and ones that are required not to propagate. You use
the former when you can prove more (e.g. Constraint_Error if argument of
sqrt is negative) and the latter when you cannot prove (enumerate, compute)
exceptional states non reachable (e.g. End_Error when EOF).

And again, contracting sqrt to raise Constraint_Error means nothing to its
caller. You can write

   if HALT(p) then
      Y := sqrt (-1.0);
   else
      Y := sqrt (8.0);
   end if;

This is not the problem of sqrt. Neither it is a problem for the caller
*until* it would try to promise not to raise Constraint_Error.

> + How should exception contracts interact with generic code?

As any other language thing does. Generic code has "generic contracts"
which become normal contracts after instantiation.

> + Should exception contracts be a part of a subprogram's type?

There is no subprogram types in Ada so far.

> Consider 
> access to subprogram values and their usage.

No difference to usual treatment of access types. The contract of an access
type includes contracts of implicitly dereferenced target type. This is the
case for access to array indexing, access to record members.
 
> + How should exception contracts interact with other static analysis 
> techniques? For example if a subprogram has a contract that says it 
> might raise exception E, but if static analysis can prove that a 
> particular usage will not actually raise E, does the programmer have to 
> declare a contract on the calling subprogram about E? One objection I've 
> heard about exception specifications in Java is that they require 
> programmers to either specify (or handle) exceptions that "clearly" can 
> never actually arise at that particular program point.

Do you mean the case when P calls to Q which is allowed to propagate E
while P promises not to propagate E? In that case if analysis shows that P
never propagates E, no special handler is required.

[It is static. The problem exists if and only if checks are dynamic.
Dynamic checks are evil, always.]

> Now that Ada has preconditions the last point is particularly acute. The 
> precondition on a procedure P might guarantee that a called subprogram 
> won't raise an exception that it might nevertheless declare in its 
> exception contract. It would be really unpleasant if the programmer had 
> to also add an exception contract to P stating that it might raise an 
> exception that the programmer knows the precondition will prevent!

There should be no dynamic preconditions. The issue, again, is only when
checks are dynamic. Dynamic checks are inherently inconsistent.

One of the advantages of contracted exceptions is that inconsistent dynamic
preconditions can be replaced with consistent exception contracts. E.g.

   Pre => X < 0
   Post => PP

with

   Pre => True
   Post => (X < 0 and raise Constraint_Error) or else PP

> This is just a sample of some of the issues involved in the subject.

More tricky are issues involving inheritance, contracts of primitive
operations as a whole (whether you allowed to manipulate them for the
overrides), Storage_Error and Program_Error.
 
> There are those who have answers for all of these issues. That's great. 
> But again I sincerely hope that if exception contracts are ever 
> seriously considered for Ada that the matter be given the deep 
> consideration it deserves.

No less is expected from the ARG!

Merry Christmas,

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

Re: Exception contracts for Ada?

[Peter C. Chapin]

I know there be dragons down this road, but I will comment on a few of 
your points. First, I want to emphasize that I'm not necessarily 
disagreeing with you... just elaborating on some ideas.

On 12/24/2012 11:34 AM, Dmitry A. Kazakov wrote:

>> + Should exception contracts be enforced statically or dynamically?
>
> Statically. Contracts cannot be enforced dynamically, it is rubbish.

I tend to agree that exception contracts should be enforced statically 
or else you end up with the mess C++ got itself into with its exception 
specifications. The problem of what to do at runtime if the contract is 
violated seems like a show-stopper for dynamic enforcement.

>> + What about backward compatibility with the existing code base?
>
> No problem at all. Empty (missing) contract = any exception may propagate.
> Everything would be 100% compatible.

But is that what we would want? I'm not sure.

>> + Should exception contracts distinguish between "impossible" exceptions
>> that shouldn't occur in a correct program (like Constraint_Error) and
>> "normal" exceptions that pertain to environmental problems such as
>> invalid input data?
>
> There is no such distinction.

Java does not require exception specifications for certain classes of 
exceptions such as for dereferencing null pointers and similar low level 
(language support) things. If it did then virtually every method would 
need to be decorated with an exception specification.

In Ada there are, for example, so many ways Constraint_Error can be 
raised that requiring it to be contracted by every subprogram seems... 
wrong somehow.

>> + How should exception contracts interact with generic code?
>
> As any other language thing does. Generic code has "generic contracts"
> which become normal contracts after instantiation.

The interesting part is not the contracts on the generic code itself but 
rather on the entities used by the generic code. Are exception contracts 
on generic code to be checked when the generic code is compiled or at 
instantiation time? Will it be necessary to add syntax so that generic 
formal parameters can have their exception contracts declared?

I suppose there are similar questions surrounding the interaction of 
pre- and postconditions and generic code. I'm not sufficiently up on Ada 
2012 yet to know how those issues are currently handled but I'm guessing 
that, because they are dynamic checks, the compiler doesn't worry about 
them.

>> + Should exception contracts be a part of a subprogram's type?
>
> There is no subprogram types in Ada so far.

If I call a subprogram indirectly via an access value, what do I know 
statically about its exception contract? How can I statically check that 
the exception contracts are being honored?

I do know that, in GNAT at least, preconditions can't be declared for 
access to subprogram types. Instead the preconditions are checked as the 
pointed-to subprogram is entered. I'm not sure if that's ideal but in 
any case it seems to make some sense for dynamically checked 
preconditions. For statically checked exception contracts, though, it 
seems like something more is needed.

> Do you mean the case when P calls to Q which is allowed to propagate E
> while P promises not to propagate E? In that case if analysis shows that P
> never propagates E, no special handler is required.

Yes that's basically what I mean. What you are suggesting sounds like it 
would require mandating a certain level of static analysis in compilers. 
Otherwise how could one write a portable program? I could imagine a very 
advanced compiler saying, "I can see that Q will never raise E in this 
situation but at the level of analysis mandated by the standard it would 
not be possible to tell that. Thus I'm going to require you to put a 
contract on P anyway declaring that P might raise E (even though you and 
I both know it won't) for portability to lesser compilers who will 
require it."

It seems to me that's a case where the standard is actively interfering 
with the capabilities of an advanced compiler.

On the other hand the idea of mandating some level of static analysis 
may be an idea who's time has come. I'm thinking again about pre- and 
postconditions. Specifying it would be difficult, I imagine.

Peter

Re: Exception contracts for Ada?

[Dmitry A. Kazakov]

On Mon, 24 Dec 2012 14:45:53 -0500, Peter C. Chapin wrote:

> I know there be dragons down this road, but I will comment on a few of 
> your points. First, I want to emphasize that I'm not necessarily 
> disagreeing with you... just elaborating on some ideas.
> 
> On 12/24/2012 11:34 AM, Dmitry A. Kazakov wrote:
> 
>>> + What about backward compatibility with the existing code base?
>>
>> No problem at all. Empty (missing) contract = any exception may propagate.
>> Everything would be 100% compatible.
> 
> But is that what we would want? I'm not sure.

It must be so, even if the language were developed from scratch. The
problem is that exception checks are evidently undecidable. It means that
you must have a grey zone for the things you cannot prove either true or
false.

Of course some legacy stuff could be much better if contracted. E.g. a
promise not to raise anything in Finalize/Initialize, but that would indeed
break legacy code.
 
>>> + Should exception contracts distinguish between "impossible" exceptions
>>> that shouldn't occur in a correct program (like Constraint_Error) and
>>> "normal" exceptions that pertain to environmental problems such as
>>> invalid input data?
>>
>> There is no such distinction.
> 
> Java does not require exception specifications for certain classes of 
> exceptions such as for dereferencing null pointers and similar low level 
> (language support) things. If it did then virtually every method would 
> need to be decorated with an exception specification.
> 
> In Ada there are, for example, so many ways Constraint_Error can be 
> raised that requiring it to be contracted by every subprogram seems... 
> wrong somehow.

But a program is not required to have a specific exception contract. The
language should not enforce that. The default contract is: I can raise
anything.

>>> + How should exception contracts interact with generic code?
>>
>> As any other language thing does. Generic code has "generic contracts"
>> which become normal contracts after instantiation.
> 
> The interesting part is not the contracts on the generic code itself but 
> rather on the entities used by the generic code. Are exception contracts 
> on generic code to be checked when the generic code is compiled or at 
> instantiation time?

Yes

> Will it be necessary to add syntax so that generic 
> formal parameters can have their exception contracts declared?

Possibly, e.g. formal exception, formal set of exceptions as generic
parameters.
 
> I suppose there are similar questions surrounding the interaction of 
> pre- and postconditions and generic code. I'm not sufficiently up on Ada 
> 2012 yet to know how those issues are currently handled but I'm guessing 
> that, because they are dynamic checks, the compiler doesn't worry about 
> them.

Sure, any [object] language aspect may have a generic counterpart [in the
meta language].

That should rather bother people pushing for more generics. To me it makes
little sense to invest any efforts into further developing of obviously
lousy concept.

>>> + Should exception contracts be a part of a subprogram's type?
>>
>> There is no subprogram types in Ada so far.
> 
> If I call a subprogram indirectly via an access value, what do I know 
> statically about its exception contract? How can I statically check that 
> the exception contracts are being honored?

This looks simple. When you declare an access to subprogram type, that
declaration will have an exception contract (possibly empty). E.g.

   type P is access procedure ... with exceptions => E1;

E1 is an exception contract. Now let you declare

   procedure F ... with exceptions => E2;

Then F'Access matches P if parameters do and E2 implies E1. Since contracts
are statically checked, you can check that at compile time.

[ A very useful thing for bindings, preventing passing Ada callbacks
raising exceptions to C libraries ]

> I do know that, in GNAT at least, preconditions can't be declared for 
> access to subprogram types.

For dynamic checks there is little difference anyway. I suppose 

>> Do you mean the case when P calls to Q which is allowed to propagate E
>> while P promises not to propagate E? In that case if analysis shows that P
>> never propagates E, no special handler is required.
> 
> Yes that's basically what I mean. What you are suggesting sounds like it 
> would require mandating a certain level of static analysis in compilers.

Yes, that is the most difficult part of it, specification what is required
to be provable about exceptions = anything else is mandated to be
considered non-provable, even if you or compiler knows otherwise.

Although exception checks could be very, very conservative. I don't think
anything more sophisticated than what Ada mandates, for example, for
presence of return statements in the function body is required.

Static analysis could simply look after all calls the body does and merge
their contracts [so for any block having handlers]. One could refine this a
bit towards if- and case-statements with static expressions, but that is
not really needed, IMO.

> It seems to me that's a case where the standard is actively interfering 
> with the capabilities of an advanced compiler.

The language, especially its type system, is full of such things. When you
do

   type T is new Integer;
 
then T is treated as another type, though you and the compiler know them
same.

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

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Florian Weimer]

* sbelmont:

> Recall that exception specifications in C++ was a god-awful
> nightmare, and has since been depreciated.

But not completely.  Code which is used to implement exception
correctness cannot itself throw exceptions, and there is the noexcept
specifier to express that.

For Ada, we'd need something similar for the Finalize operation on
controlled types, and actually, for initializers, too, because the
exception handlers do not cover the declarations preceeding the block
(so that dealing with exceptions in initializers is syntactically
rather awkward).

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[sbelmont700]

This is just one programmer's opinion based on what I've seen in C++ and Java, but exception specifications are a bad path that goes nowhere.

Consider the static case, where a subprogram has to specify a superset of all the specifications of subprograms it calls.  This will be of limited value, since you almost always end up being coupled to an API that you don't have control over (gtkAda, Claw, etc), which are written pre-2012 and are not likely to be updated anytime soon.  Unless they are painstakingly revised to change the default "raises anything" (which is not going to happen, since you cut out all pre-2012 customers), then all the subprograms that call them must also 'raise anything', and those that call those must 'raise anything' as well in a viral nature, and so on and so on for everything, and you end up with all subprograms raising everything, and it's a lost cause.  The dynamic case (as in C++) is just as bad, since when an unspecified exceptions happens, the only thing left to do is continue erroneously or obfuscate things by raising a different exception than what originally happened, and you're actually worse off than before.

Secondly, the point is moot for OOP since the goal is to use classwide types.  Putting an exception specification on a parent type automatically restricts all the child types (which may not even be thought of yet, much less written) to following that same model, which is often not the case.  Similar to the guideance of making the controlling operand 'in out' to anticipate future child types that might need to make state changes, any parent type would be unwise to dictate what exceptions a future child implementation might need to raise by putting anything other than a 'raises anything'.  So even if you could put perfect exception specifications on everyting, once you start dealing with the classwide type, it's all out the window anyway.

Finally, IMHO, exceptions are NOT a property of the interface but of the implementation (we will likely have to agree to disagree on this).  You can take a subprogram that works one certain way (and potentially raises one set of exceptions), and then rework the guts to work an entirely different way but produce the same output with the same inputs, and raises a whole new set of exceptions; e.g. if you allocate and free your variables instead of declaring them, that changes the subprograms interface because now you might raise STORAGE_ERROR?  That's a side effect of the implementation, not a change to the interface.  Otherwise, you would have to go back and update the interface nearly every time you change the implementation, which defeats the purpose.

I'm of the school of thought that says every subprogram has just one inherent contract when it comes to exceptions: as long as all the parameters and pre/post conditions are met, the subprogram will *never raise anything*.  Or, to put it another way, an exception is an indication that the contract with the interface has NOT been met.  You don't need to know which ones may or may not be raised, since as long as you meet the pre-conditions they won't ever happen anyway.  If you think you need an exception specification, then IMHO what you really need is another precondition.

Just my $0.02

-sb

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1drh1q1ln2dfh$.a9hwlg01fjfy.dlg@40tude.net...
...
> In the first step I would rather prefer means to declare user-defined
> operations pure, context-dependent pure, compile-time evaluated etc. This
> would be more universal than mere predicates, and "proper" predicates 
> would
> require that stuff anyway. An alternative, letting the compiler/vendor to
> deduce such properties, is IMO unrealistic (an undecidable problem, I
> think).

Some of us wanted such capabilities in Ada 2005, but there has always been a 
strong contengent of people who do not believe in having these properties 
checked by the implementation. These misguided people are opposed by an 
equally strong group that thinks that declaring unchecked properties would 
lead to making programs less safe in the case when these properties are a 
lie (which is easy to do by mistake, especially when inheritance is 
involved).

I was also hoping to have these properties be used for task-safety as well 
(truly pure functions are automatically task-safe so long as the parameters 
are different) -- but those who think "memo functions" are important to 
allow as pure bollix up the works.

For Ada 2012, we tried an end run involving proper global in/out 
properties -- but it just got too complicated and we didn't finish it. (I 
understand that some of the tools AdaCore is working on use the proposed 
global in/out properties, so there is some hope that it will make it into 
Ada in the future).

                               Randy.

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Randy Brukardt]

<sbelmont700@gmail.com> wrote in message 
news:e9f91590-75b2-4cb4-b897-e8f06d0128e6@googlegroups.com...
>This is just one programmer's opinion based on what I've seen in C++ and 
>Java,
>but exception specifications are a bad path that goes nowhere.

I strongly disagree...although they're only useful in a subset of places 
(not everywhere).

>Consider the static case, where a subprogram has to specify a superset of 
>all the
>specifications of subprograms it calls.  This will be of limited value, 
>since you
>almost always end up being coupled to an API that you don't have control 
>over
>(gtkAda, Claw, etc), which are written pre-2012 and are not likely to be 
>updated
>anytime soon.  Unless they are painstakingly revised to change the default 
>"raises
>anything" (which is not going to happen, since you cut out all pre-2012 
>customers),
>then all the subprograms that call them must also 'raise anything', and 
>those that call
>those must 'raise anything' as well in a viral nature, and so on and so on 
>for everything,
>and you end up with all subprograms raising everything, and it's a lost 
>cause.  The
>dynamic case (as in C++) is just as bad, since when an unspecified 
>exceptions
>happens, the only thing left to do is continue erroneously or obfuscate 
>things by
>raising a different exception than what originally happened, and you're 
>actually worse
>off than before.

Exception contracts need to be static (for the reasons you mention here), 
but they're absolutely needed in reusable libraries. You mentioned Claw: it 
has an exception contract (in the form of comments) for *every* subprogram. 
Raising an exception other than one in the contract is a bug, period. And 
that's also true for language-defined packages like Text_IO and the 
containers. If a routine in any such package could raise any exception for 
any reason, it would be impossible to use safely.

The use case for exception contracts in *calling* code is not as clear --  
it's possible that they ought to be avoided outside of reusable libraries. 
(Not sure about this.)

>Secondly, the point is moot for OOP since the goal is to use classwide 
>types.
>Putting an exception specification on a parent type automatically restricts 
>all the
>child types (which may not even be thought of yet, much less written) to
>following that same model, ...

Just like using subtypes and parameter modes. Oh, the horror! :-)

LSP requires that the contract of all of the child routines are the same --  
if you allow child routines to raise random unknown exceptions (especially 
in cases that don't represent bugs - think End_Error as an example), you are 
violating LSP just the same as if your child routines have stronger 
preconditions. In which case, you can no longer reason about the class-wide 
calls -- greatly reducing the entire value of the OOP model.

>...which is often not the case.  Similar to the guideance of making the
>controlling operand 'in out' to anticipate future child types that might 
>need
>to make state changes, any parent type would be unwise to dictate what
>exceptions a future child implementation might need to raise by putting
>anything other than a 'raises anything'.  So even if you could put perfect
>exception specifications on everyting, once you start dealing with the
>classwide type, it's all out the window anyway.

This is terrible advice. As I mentioned last week, exceptions are used for 
two purposes: one is "checks", which should never fail at all. One hopes 
that they can be removed completely via static proof, but in any case they 
have to be the same (or weaker) for child routines, or else LSP is violated. 
The other kind is an exceptional termination, like End_Error -- and again, 
these have to be described as part of the contract (explicit or implicit) so 
that the caller can handle them approproately. You can't just go adding 
these to child subprograms anymore than you can add parameters (or tigher 
subtypes on existing parameters). Allowing exceptions to change willy-nilly 
is just as bad as allowing the preconditions to change that way.

>Finally, IMHO, exceptions are NOT a property of the interface but of
>the implementation (we will likely have to agree to disagree on this).

Surely we will. No subprogram should propagate any exceptions unless they're 
described in the interface of the routine. Anything else is a bug (I realize 
most of us are lax this way).

>You can take a subprogram that works one certain way (and potentially
>raises one set of exceptions), and then rework the guts to work an entirely
>different way but produce the same output with the same inputs, and raises
>a whole new set of exceptions; e.g. if you allocate and free your variables
>instead of declaring them, that changes the subprograms interface because
>now you might raise STORAGE_ERROR?

All subprograms can raise Storage_Error; in fact, "null;" can raise 
Storage_Error in Ada (formally). Storage_Error is the biggest annoyance with 
contracted exceptions, because it is virtually impossible to write any Ada 
code that does *not* have the possibility of raising Storage_Error. Thus, 
every exception contract will need to include it.

>That's a side effect of the implementation, not a change to the interface.
>Otherwise, you would have to go back and update the interface nearly every
>time you change the implementation, which defeats the purpose.

Propagating random exceptions from an implementation of a routine is a bug: 
it's either a bug because the routine isn't properly making checks 
internally (and thus is propagating failed checks -- one would hope that an 
exception contract would point out that this problem exists so that the 
implementation can be fixed), or because the interface isn't defined 
properly (to include things like Storage_Error as a possible result).

>I'm of the school of thought that says every subprogram has just one
>inherent contract when it comes to exceptions: as long as all the 
>parameters
>and pre/post conditions are met, the subprogram will *never raise 
>anything*.
>Or, to put it another way, an exception is an indication that the contract 
>with
>the interface has NOT been met.  You don't need to know which ones may
>or may not be raised, since as long as you meet the pre-conditions they 
>won't
>ever happen anyway.  If you think you need an exception specification, then
>IMHO what you really need is another precondition.

In this case, you might as well make these the exception contracts (that is, 
a contract of raising nothing), because then the compiler will statically 
tell you when you've forgotten to make the checks or define the 
preconditions necessary to avoid them. Why allow runtime failures if you can 
ensure that they don't happen?? (I realize that the quality of proof needed 
to make this work might be beyond the state-of-the-art today, but I doubt 
that will be the case by the time a new version of Ada is defined.)

The only things that should be in the exception contract are exceptions that 
are expected to be raised in cases that can't be statically proved: for 
Claw, for instance, Windows_Error is raised when Windows fails an API call; 
that *might* be a Claw bug or a usage bug, but it's impossible to tell in 
general what might cause that so we have to presume it is always possible.

Note that the preconditions/predicates etc. are (formally) evaluated at the 
call site, and exceptions raised by them (or their failure) shouldn't be 
part of the subprogram's exception contract. So if the preconditions are 
correct, then an empty exception contract should be sufficient. (And one 
hopes that they can be proved.)

                                        Randy.


Just my $0.02

-sb 

Re: Exception contracts for Ada? Was: Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Randy Brukardt]

"Peter C. Chapin" <pcc482719@gmail.com> wrote in message 
news:46idnVdMEr8J5EXN4p2dnAA@giganews.com...
...
> Exception contracts are a huge, HUGE topic and one that shouldn't be 
> treated too lightly.

We've had this discussion within the ARG. It's pretty clear to me what the 
answers are (but others may not agree). See AI12-0017-1 for my take on this. 
(The ARG has not yet discussed this AI.)

The problem in other languages is requiring them everywhere -- I'm pretty 
certain that will never work. They're critical for properly defining 
reusable code, but I'm dubious that they have much value in "top-level" code 
(the stuff that is created to use those reusable libraries). Good reusuable 
libraries are very hard work, and the more help the compiler can give the 
better...

...
Consider:
> + Should exception contracts be enforced statically or dynamically?

Statically. Dynamic enforcement is a total can of worms with no real value. 
The real question is whether the enforcement can depend on 
implementation-properties (that is, if the implementation can optimize away 
a check, can that be used in enforcing the contract), or whether it has to 
remain portable.

> + Should exception contracts be enforced at all or only produce warnings 
> or logs?

That's worthless from an language perspective; pretty much the only value 
beyond the comments that we already use is static checking. Personally, I'm 
not interested in adding features to Ada that can't be used by an Ada 
compiler (but only be separate tools).

> + What about backward compatibility with the existing code base? We don't 
> want to force people to decorate all code with exception contracts before 
> it will compile again with Ada 2020 (or whatever). Do we?

Clearly, the default has to be "raises anything", we can't make everything 
incompatible. As best as we can tell, the root problem in C++ and Java is 
that the default is more restrictive. (Stupid coding policies probably don't 
help, either.)

> + Should exception contracts distinguish between "impossible" exceptions 
> that shouldn't occur in a correct program (like Constraint_Error) and 
> "normal" exceptions that pertain to environmental problems such as invalid 
> input data?

IMHO, no. The biggest value to these contracts is proving that 
language-defined exceptions don't occur (the compiler knows far more about 
this than any tool can figure out, as only it knows whether or not a check 
is generated for a particular operation in the code). The only exception 
that defies most such proofs is Storage_Error (and it can be eliminated in 
specialized circumstances). So I think everything should be specified. In 
order to cut down the size of such contracts, I've proposed allowing 
creating "sets of exceptions", so that only the single name of the set need 
be mentioned.

> + How should exception contracts interact with generic code?

I don't see any real problem here; a formal subprogram has to have an 
optional contract, and if it does, it has to "match".

> + Should exception contracts be a part of a subprogram's type? Consider 
> access to subprogram values and their usage.

Access-to-subprograms are probably going to always be "raises anything". 
This is very similar to the way preconditions work; one might expect that 
access-to-subprograms should allow preconditions and require some sort of 
matching, but that's just too complicated so it's purely dynamic.

This will mean that access-to-subprograms won't be able to be called from 
inside of exception contracted subprograms. But the only effect of that will 
be to encourage avoiding access-to-subprogram completely (a very positive 
result, IMHO, you can't prove anything about a call to an 
access-to-subprogram in Ada 2012 and I doubt that will change).

> + How should exception contracts interact with other static analysis 
> techniques? For example if a subprogram has a contract that says it might 
> raise exception E, but if static analysis can prove that a particular 
> usage will not actually raise E, does the programmer have to declare a 
> contract on the calling subprogram about E? One objection I've heard about 
> exception specifications in Java is that they require programmers to 
> either specify (or handle) exceptions that "clearly" can never actually 
> arise at that particular program point.

See my answer to the first question. I strongly lean toward the 
implementation-defined static check (I'd be against adding the contracts at 
all if that isn't the case), but I'm pretty certain that is going to be a 
tough sell (it will harm portability, as a compiler that isn't as "smart" 
may not be able to tell that the exception isn't raised).

The alternative of mandating what Ada compilers are required to be able to 
deduce is unlikely to work; it would be fiendishly complex and would add a 
great burden to at least some implementations. (Which would cause a lot of 
resistance, I think.)

> Now that Ada has preconditions the last point is particularly acute. The 
> precondition on a procedure P might guarantee that a called subprogram 
> won't raise an exception that it might nevertheless declare in its 
> exception contract.

That would be wrong; the exception contract should not cover things included 
in the precondition. And if the precondition is necessary to prevent an 
exception from being raised by the body, then the subprogram specification 
should be declared so that the precondition cannot be ignored. (That 
shouldn't prevent the compiler from eliminating it if it is redundant, just 
that it should never be unchecked.)

> It would be really unpleasant if the programmer had to also add an 
> exception contract to P stating that it might raise an exception that the 
> programmer knows the precondition will prevent!

As above, that's not how I envision these things working. (But please keep 
in mind, most of this is my feverish musing and it hasn't been vetted by 
others yet.)

> This is just a sample of some of the issues involved in the subject. There 
> are those who have answers for all of these issues.

That would be me, editor of the ARG and the Ada Standard. ;-)

> That's great. But again I sincerely hope that if exception contracts are 
> ever seriously considered for Ada that the matter be given the deep 
> consideration it deserves.

I hope you don't think that I just wrote this up based on absolutely 
nothing -- I've been thinking about how this would work since we started 
working on Claw...and I've taken input from many members of the ARG. (As 
well as discussions on these topics that the ARG had for Ada 2005, and a 
lengthy e-mail thread that we had specifically on the topic of what Java did 
wrong here). We have not yet had a formal discussion on this particular 
proposal, and I'm certain that it isn't 100% correct at this point (I must 
have forgotten something!). But it's rather insulting to have someone claim 
that it hasn't been given proper consideration before making a proposal (or 
to imply that the ARG would simply adopt something without thinking about 
it).

                                                        Randy.

Re: Exception contracts for Ada?

[Randy Brukardt]

"Peter C. Chapin" <pcc482719@gmail.com> wrote in message 
news:XYadnZrAFoJvLUXN4p2dnAA@giganews.com...
...
>>> + What about backward compatibility with the existing code base?
>>
>> No problem at all. Empty (missing) contract = any exception may 
>> propagate.
>> Everything would be 100% compatible.
>
> But is that what we would want? I'm not sure.

There is no other possibility. One could imagine a restriction that required 
a contract on every subprogram. But as we found out with "overriding", that 
way lies dragons.

My personal opinion is that what Java got wrong was the default. "anything 
can be raised" is much friendlier than making people stick junk handlers in 
everywhere or change their contracts repeatedly. Some interfaces have to be 
designed in stone (like those for Claw, Ada.Containers, etc.), but most 
don't need that level of contracting.

>>> + Should exception contracts distinguish between "impossible" exceptions
>>> that shouldn't occur in a correct program (like Constraint_Error) and
>>> "normal" exceptions that pertain to environmental problems such as
>>> invalid input data?
>>
>> There is no such distinction.
>
> Java does not require exception specifications for certain classes of 
> exceptions such as for dereferencing null pointers and similar low level 
> (language support) things. If it did then virtually every method would 
> need to be decorated with an exception specification.

Right; here again, this is what Java got wrong. By making the default "no 
exceptions", the contracts got immediately out of hand. And they then fixed 
that by excepting some exceptions from the contracts, making the contracts 
like swiss cheese. They never worked their way out of the morass -- proving 
again that two mistakes don't make something usable. :-)

> In Ada there are, for example, so many ways Constraint_Error can be raised 
> that requiring it to be contracted by every subprogram seems... wrong 
> somehow.

No, the preconditions/predicates should prevent it from being raised, and 
the compiler should be able to prove that. So it doesn't need to be in most 
of the contracts. (If a Claw subprogram raises Constraint_Error, it's a 
bug!)

To me this is a big benefit of these contracts: you can *declare* exception 
absence, and the compiler will either prove it or fail to the code -- no 
restrictive and separate tool like Spark needed for that. (Which brings that 
particular benefit of Spark to everyone.)

>>> + How should exception contracts interact with generic code?
>>
>> As any other language thing does. Generic code has "generic contracts"
>> which become normal contracts after instantiation.
>
> The interesting part is not the contracts on the generic code itself but 
> rather on the entities used by the generic code. Are exception contracts 
> on generic code to be checked when the generic code is compiled or at 
> instantiation time? Will it be necessary to add syntax so that generic 
> formal parameters can have their exception contracts declared?

Yes, of course. Otherwise, they're "raise any". But perhaps we won't do this 
any more than we do it for preconditions. (As far as I can tell, this 
prevents any proofs of a generic unit before instantiation, and makes the 
proofs "fragile" as a different instance might fail. This is not Ada to 
me...)

> I suppose there are similar questions surrounding the interaction of pre- 
> and postconditions and generic code. I'm not sufficiently up on Ada 2012 
> yet to know how those issues are currently handled but I'm guessing that, 
> because they are dynamic checks, the compiler doesn't worry about them.

Right, and I'm pretty sure this is wrong (but too hard to fix, as it would 
require "matching" of arbitrary expressions - conformance is close but it 
doesn't work because the types would be different).

...
> I do know that, in GNAT at least, preconditions can't be declared for 
> access to subprogram types. Instead the preconditions are checked as the 
> pointed-to subprogram is entered. I'm not sure if that's ideal but in any 
> case it seems to make some sense for dynamically checked preconditions. 
> For statically checked exception contracts, though, it seems like 
> something more is needed.

More is needed for preconditions, too, unless you never want to prove 
anything and make only dynamic checks. My guess is that access-to-subprogram 
is inherently unsafe from a proof perspective, and nothing is going to fix 
that. So there is no point in adding lipstick to a pig -- especially if the 
attempt to do so would make the entire proposal too complex (a real problem 
in Ada language proposals).

...
> Yes that's basically what I mean. What you are suggesting sounds like it 
> would require mandating a certain level of static analysis in compilers. 
> Otherwise how could one write a portable program? I could imagine a very 
> advanced compiler saying, "I can see that Q will never raise E in this 
> situation but at the level of analysis mandated by the standard it would 
> not be possible to tell that. Thus I'm going to require you to put a 
> contract on P anyway declaring that P might raise E (even though you and I 
> both know it won't) for portability to lesser compilers who will require 
> it."

I think that the "solution" is that the "proof" is implementation-defined 
for language-defined checks. Which means that a program with "static" 
exception contracts might not be portable to a "dumb" compiler. That's 
annoying, but I think any alternative is going to turn out much worse (but 
I'm happy if someone wants to try to prove me wrong). Certainly, trying to 
define checks that have to be optimized away is going to be madness, and not 
using the knowledge that the compiler has is also madness. After all, 
"canonical semantics" says that
            A : Integer := 10;
might raise Constraint_Error, but I'd be amazed if there is any compiler 
that generates a check in this case.

I think only "implementation-defined" is likely to work. This is clearly the 
weak point of my proposal (and any useful exception contracts, IMHO).

> It seems to me that's a case where the standard is actively interfering 
> with the capabilities of an advanced compiler.
>
> On the other hand the idea of mandating some level of static analysis may 
> be an idea who's time has come. I'm thinking again about pre- and 
> postconditions. Specifying it would be difficult, I imagine.

I don't think it's time will ever come, simply because trying to do so will 
take up a lot of time and effort. I really have no idea how to describe that 
formally that could be understood (look at 11.6 to see how well that has 
been explained in past standards :-).

                                       Randy.

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Dmitry A. Kazakov]

On Wed, 26 Dec 2012 17:00:47 -0800 (PST), sbelmont700@gmail.com wrote:

> Consider the static case, where a subprogram has to specify a superset of
> all the specifications of subprograms it calls.

Not really. It specifies a conditional contract: "I rase E and whatever P
raises." I presume that P is explicitly stated, e.g. a callback or an
object passed.

> This will be of limited value, since you almost always end up being
> coupled to an API that you don't have control over (gtkAda, Claw, etc),

Ada API will certainly enjoy exception contracts. One of the nastiest
problems when using GtkAda is exceptions propagating into Gtk. Since GtkAda
is almost 100% user-defined Ada callbacks done from C, you *do* want to be
able to contract them not to raise anything.

> Secondly, the point is moot for OOP since the goal is to use classwide
> types.  Putting an exception specification on a parent type automatically
> restricts all the child types (which may not even be thought of yet, much
> less written) to following that same model, which is often not the case.

Exception contract must be inherited. It is governed by the LSP. Conditions
may be weakened, promises strengthened. Note that this does not mean that
the contract remains exactly same. For example, stream write might have the
contract "may raise Ada I/O exceptions." An implementation of a blocking
stream could exclude End_Error.

> Finally, IMHO, exceptions are NOT a property of the interface but of the
> implementation (we will likely have to agree to disagree on this).

This is evidently wrong because you can write an exception handler and make
the program's behavior dependent on whether the exception propagated.

> You can take a subprogram that works one certain way (and potentially
> raises one set of exceptions), and then rework the guts to work an
> entirely different way but produce the same output with the same inputs,
> and raises a whole new set of exceptions;

That would be another subprogram with another interface.

> e.g. if you allocate and free your variables instead of declaring them,
> that changes the subprograms interface because now you might raise
> STORAGE_ERROR?

Both interfaces have Storage_Error in the contract. No difference, also.

Regarding Storage_Error. The contract model should support conditional
exceptions. This is the case "I raise if you do" and for Storage_Error it
is "I don't raise if there is X free storage elements of stack and Y
elements of pool Z." The estimations would be very conservative of course
if you wanted it more portable. It is thinkable that some other measurement
unit could be deployed to make less architecture dependent. Though
Storage_Error handling is more interesting for embedded and RT
applications, which are natively less portable than others. Most users
would probably never contract Storage_Error anyway.

For recursive subprograms and other programs where memory consumption is
undecidable yet might be known from other sources (e.g. tests), the
programmer should be able to instruct the compiler using a pragma, that the
implementation satisfies the contract.

> I'm of the school of thought that says every subprogram has just one
> inherent contract when it comes to exceptions: as long as all the
> parameters and pre/post conditions are met, the subprogram will *never
> raise anything*.

Why not to state that contract, especially for those who belong to other
schools?

> Or, to put it another way, an exception is an indication that the
> contract with the interface has NOT been met.

See, there was a contract then. You are in a contradiction.

> You don't need to know which ones may or may not be raised, since as long
> as you meet the pre-conditions they won't ever happen anyway.

Yes. But you cannot put undecidable stuff into a precondition. This is the
backdoor through which End_Error and all other exceptions come in and make
themselves comfortable, at our expense of course.

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

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[sbelmont700]

On Wednesday, December 26, 2012 8:47:29 PM UTC-5, Randy Brukardt wrote:

>  As I mentioned last week, exceptions are used for two purposes: one
>  is "checks", which should never fail at all.... The other kind is an
> exceptional termination, like End_Error 


While I agree 100% with the first part, I remain extremely skeptical about the second.  I've yet to be convinced of a case where its necessary/preferable/best-structured to propogate an exception out to be handled by the client instead of making the client check it beforehand.  You show me a subprogram that raises End_Error and I'll show you a subprogram that needs a precondition "not At_End".  If you are rasising "File_Not_Found" then you need a precondition of "File_Exists".  The onus is on the interface to provide the necessary information to the client to ensure exceptions do not happen in the first place, and the onus is on the client to make sure they are met *before* the call, not to swoop in afterwards to clean up the mess.  If you can handle it (that is, correct the actual problem and continue as before), you can prevent it.

-sb

Re: Exception contracts for Ada? Was: Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Peter C. Chapin]

On 12/26/2012 09:16 PM, Randy Brukardt wrote:

> I hope you don't think that I just wrote this up based on absolutely
> nothing -- I've been thinking about how this would work since we started
> working on Claw...and I've taken input from many members of the ARG. (As
> well as discussions on these topics that the ARG had for Ada 2005, and a
> lengthy e-mail thread that we had specifically on the topic of what Java did
> wrong here). We have not yet had a formal discussion on this particular
> proposal, and I'm certain that it isn't 100% correct at this point (I must
> have forgotten something!). But it's rather insulting to have someone claim
> that it hasn't been given proper consideration before making a proposal (or
> to imply that the ARG would simply adopt something without thinking about
> it).

Randy, I think you misunderstood my comment. I was not trying to suggest 
that the ARG has been deficient in their reflections on this subject. In 
fact, I know it is the opposite and I know that you personally are very 
careful in your approach to these kinds of questions.

I actually have the utmost faith in the ARG. Things like AI12-0017-1 and 
all the conversations related to it is proof that my faith is well 
founded. In fact, my comments were actually intended to be supportive 
even if they perhaps did not come out that way. For that I apologize.

Peter

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Dmitry A. Kazakov]

On Thu, 27 Dec 2012 06:29:02 -0800 (PST), sbelmont700@gmail.com wrote:

> I've yet to be convinced of a case where its
> necessary/preferable/best-structured to propogate an exception out to be
> handled by the client instead of making the client check it beforehand.

Like checking a 100_000 x 100_000 matrix for being singular before actually
inverting it?

> You show me a subprogram that raises End_Error and I'll show you a
> subprogram that needs a precondition "not At_End".

Terminal I/O, stream I/O, sockets.

EOF is computable only once, most of the time. Hard-drive file systems
represent a rare exception from the rule. And as with the example of matrix
inversion, checking for EOF might be utterly inefficient even when dealing
with a HDD.

> If you are rasising "File_Not_Found" then you need a precondition of
>"File_Exists".

And a nice race condition coming with that! Never use File_Exists if you
can.

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

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Jeffrey Carter]

On 12/27/2012 08:30 AM, Dmitry A. Kazakov wrote:
>
>
> And a nice race condition coming with that! Never use File_Exists if you
> can.

Precisely. Multiple processes may access the file system at the same time. The 
idea that you can check the precondition to an operation and have the result 
still hold when you invoke the operation is only valid for sequential 
activities; when you're using a concurrent language like Ada then there are 
often cases when that's a race. The Get operation for a concurrent, non-blocking 
queue has the precondition "not Is_Empty", but between checking that and 
invoking Get another task may have changed the state of the queue.

-- 
Jeff Carter
"He didn't get that nose from playing ping-pong."
Never Give a Sucker an Even Break
110

compilers, was Re: Press Release - Ada 2012 Language Standard Approved by ISO

[tmoran]

> I realize that the quality of proof needed to make this work might be
> beyond the state-of-the-art today, but I doubt that will be the case by
> the time a new version of Ada is defined.
    I thought compilers were getting wider - handling more constructs -
rather than deeper - more analysis and optimization.  Is that not the case?

Re: compilers, was Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Shark8]

On Thursday, December 27, 2012 2:12:59 PM UTC-6, tmo...@acm.org wrote:
> > I realize that the quality of proof needed to make this work might be
> > beyond the state-of-the-art today, but I doubt that will be the case by
> > the time a new version of Ada is defined.
>     I thought compilers were getting wider - handling more constructs -
> rather than deeper - more analysis and optimization.  Is that not the case?

I think that that is dependent on the language you're talking about, or in MS's case [sometimes] the platform (.NET)... and that's a C-ish language.

But then again, Ada's always been more for early-error detection -- static/compile-time checking is the earliest point the compiler can point out an error in our program-text.

In that vein I like Randy's suggestion (though I think an OR separated list would be better than a comma separated list); I absolutely agree that there needs to be a facility for naming a 'set' of exceptions.

The implementation shouldn't be too hard in the case of user-defined exceptions: the most difficult part would be recognizing that the following doesn't raise CONSTRAINT_ERROR (more correctly propagate):

  Type LString is Access String;

  -- Returns true when the strings are equal or both parameters are null.
  Function "=" (Left, Right: IN LString) Return Boolean is
     Subtype Constrained_LString is Not Null LString;

     Function "="( Left : LString; Right : String ) Return Boolean is
     begin
        Return Right = Left.All;
     exception
        When CONSTRAINT_ERROR => Return False;
     end "=";

  Begin
     Return "="(Left, Right.All);
  Exception
     When CONSTRAINT_ERROR =>
        begin
           Return "="(Right,Left.All);
        Exception
           When CONSTRAINT_ERROR => Return True;
        end;
  End "=";

-- Yes, it is horrid abuse of exceptions... but it'll work even in Ada 83.

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Randy Brukardt]

"Jeffrey Carter" <spam.jrcarter.not@spam.not.acm.org> wrote in message 
news:kbi56i$plr$1@dont-email.me...
> On 12/27/2012 08:30 AM, Dmitry A. Kazakov wrote:
>>
>>
>> And a nice race condition coming with that! Never use File_Exists if you
>> can.
>
> Precisely. Multiple processes may access the file system at the same time. 
> The idea that you can check the precondition to an operation and have the 
> result still hold when you invoke the operation is only valid for 
> sequential activities; when you're using a concurrent language like Ada 
> then there are often cases when that's a race. The Get operation for a 
> concurrent, non-blocking queue has the precondition "not Is_Empty", but 
> between checking that and invoking Get another task may have changed the 
> state of the queue.

And not just tasks in your program, but processes from other programs 
running on the machine, programs from other machines accessing your file 
system, and of course, the wetware (you) running the computer can change the 
state of the file system.

Moreover, it's not just file system operations that behave this way. Almost 
any interactions with the underlying system have this property (memory 
management, networking, GUI, etc.). This was a major consideration for the 
design of Claw -- everything raises exceptions because the operation of the 
GUI is necessarily asynchonous WRT to your program: the wetware running the 
program can click on the 'x' and close a window while the program is 
referencing it. There is no sane way to stop that (you can block those 
operations for a while, but doing it for long makes the GUI unresponsive). 
You can only handle errors, you cannot prevent them beforehand.

Dmitry also touched on the fact that prechecking can be too expensive to use 
in common scenarios. For instance, End_of_File is about as costly as Get 
when using Text_IO. If your program reads single characters, you're doubling 
the I/O time if you pretest with End_of_File (and if you are reading large 
files in a tight loop, that can make a significant performance difference - 
especially as Text_IO is slow anyway).

                                     Randy.

Re: compilers, was Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Randy Brukardt]

<tmoran@acm.org> wrote in message news:kbia4b$srn$1@speranza.aioe.org...
>> I realize that the quality of proof needed to make this work might be
>> beyond the state-of-the-art today, but I doubt that will be the case by
>> the time a new version of Ada is defined.
>    I thought compilers were getting wider - handling more constructs -
> rather than deeper - more analysis and optimization.  Is that not the 
> case?

A compiler-writer that isn't making their code better is just going through 
the motions, IMHO. Optimization/code generation is the fun/rewarding part of 
compiler construction -- the rest of it is the busy work needed to support 
the fun. As such, I can't quite imagine a developer that takes pride in 
their work not trying to make that better.

And of course, the best way to generate faster checks is to prove that 
they're not needed at all. The fastest check is always the one you don't 
make! So more proof directly aids that primary goal of compiler writers. 
(For Ada, of course, it also offers the possibility of detecting more errors 
early.)

                                                      Randy.

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[J-P. Rosen]

Le 27/12/2012 22:54, Randy Brukardt a �crit :
> Dmitry also touched on the fact that prechecking can be too expensive to use 
> in common scenarios. For instance, End_of_File is about as costly as Get 
> when using Text_IO. If your program reads single characters, you're doubling 
> the I/O time if you pretest with End_of_File (and if you are reading large 
> files in a tight loop, that can make a significant performance difference - 
> especially as Text_IO is slow anyway).

And in addition to those excellent reasons, here is another one. If you
forget to check a condition (or a result code for that matter), you can
get wrong results without knowing it. If you forget to catch an
exception, the program will crash, but you'll know it.

Remember: there is only one thing worse than a program that crashes: a
program that gives wrong, but likely results.

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Yannick Duchêne (Hibou57)]

Le Thu, 27 Dec 2012 02:00:47 +0100, <sbelmont700@gmail.com> a écrit:

> Finally, IMHO, exceptions are NOT a property of the interface but of the  
> implementation (we will likely have to agree to disagree on this).

May suggest there is two kinds of exceptions. The ones which are part of  
the interface and the ones which are part of the implementation.  
Declarations in the large goes this way too.

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Yannick Duchêne (Hibou57)]

Le Thu, 27 Dec 2012 16:30:15 +0100, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
>> If you are rasising "File_Not_Found" then you need a precondition of
>> "File_Exists".
>
> And a nice race condition coming with that! Never use File_Exists if you
> can.

I don't understand this one. Is there a short example scenario to make it  
clearer?


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Yannick Duchêne (Hibou57)]

Le Thu, 27 Dec 2012 19:48:50 +0100, Jeffrey Carter  
<spam.jrcarter.not@spam.not.acm.org> a écrit:

> On 12/27/2012 08:30 AM, Dmitry A. Kazakov wrote:
>>
>>
>> And a nice race condition coming with that! Never use File_Exists if you
>> can.
>
> Precisely. Multiple processes may access the file system at the same  
> time. The idea that you can check the precondition to an operation and  
> have the result still hold when you invoke the operation is only valid  
> for sequential activities;

I disagree a bit, and this case may suggest to use locks.


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Yannick Duchêne (Hibou57)]

Le Thu, 27 Dec 2012 22:54:59 +0100, Randy Brukardt <randy@rrsoftware.com>  
a écrit:
> Dmitry also touched on the fact that prechecking can be too expensive to  
> use in common scenarios.

Yes, I like this one. Sometime the only check which is OK, is the one  
where you don't actually run the check, and prove it instead. If you  
didn't proved it or your assumption was wrong, then an exception is raised.

Pre‑check is not an Holy Grail, pre‑proving, is (when feasible).

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Dmitry A. Kazakov]

On Fri, 11 Jan 2013 12:33:58 +0100, Yannick Duch�ne (Hibou57) wrote:

> Le Thu, 27 Dec 2012 16:30:15 +0100, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a �crit:
>>> If you are rasising "File_Not_Found" then you need a precondition of
>>> "File_Exists".
>>
>> And a nice race condition coming with that! Never use File_Exists if you
>> can.
> 
> I don't understand this one. Is there a short example scenario to make it  
> clearer?

if exists then
   open old
else
   create new
end if;

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

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Dmitry A. Kazakov]

On Fri, 11 Jan 2013 12:28:50 +0100, Yannick Duch�ne (Hibou57) wrote:

> Le Thu, 27 Dec 2012 02:00:47 +0100, <sbelmont700@gmail.com> a �crit:
> 
>> Finally, IMHO, exceptions are NOT a property of the interface but of the  
>> implementation (we will likely have to agree to disagree on this).
> 
> May suggest there is two kinds of exceptions. The ones which are part of  
> the interface and the ones which are part of the implementation.  
> Declarations in the large goes this way too.

Exception is never an implementation, because its propagation or
non-propagation always changes the client's logic.

It is same as to claim than an output parameter is a part of the
implementation.

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

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Yannick Duchêne (Hibou57)]

Le Fri, 11 Jan 2013 15:21:14 +0100, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

> On Fri, 11 Jan 2013 12:28:50 +0100, Yannick Duchêne (Hibou57) wrote:
>
>> Le Thu, 27 Dec 2012 02:00:47 +0100, <sbelmont700@gmail.com> a écrit:
>>
>>> Finally, IMHO, exceptions are NOT a property of the interface but of  
>>> the
>>> implementation (we will likely have to agree to disagree on this).
>>
>> May suggest there is two kinds of exceptions. The ones which are part of
>> the interface and the ones which are part of the implementation.
>> Declarations in the large goes this way too.
>
> Exception is never an implementation, because its propagation or
> non-propagation always changes the client's logic.

Propagating vs non‑propagating, was what I had in mind (confined to some  
kind of scope or not).


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Jacob Sparre Andersen]

Yannick Duch�ne wrote:

> I disagree a bit, and this case may suggest to use locks.

Which file systems/operationg systems allow an application to take a
lock on a directory?

Greetings,

Jacob
-- 
Infinite loop: n., see loop, infinite.
Loop, infinite: n., see infinite loop.

File_Exists (Was: Press Release - Ada 2012 Language Standard Approved by ISO)

[Jacob Sparre Andersen]

Dmitry A. Kazakov wrote:

> Never use File_Exists if you can.

One of my colleagues could come up with a sensible use case for
"File_Missing": When a web service wants to know if it should ask a user
to upload a profile image (stored in a file).

Some applications use the existence of certain files as a simple
external management interface.  Although I consider this bad style and
prefer a socket based management interface, it might be considered a
reasonable use as well.

Can anybody supply some other sensible use cases for
File_Exists/File_Missing.

Greetings,

Jacob
-- 
The backhoe is the natural predator of the fiber optic cable.

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Marius Amado-Alves]

>    subtype More_Fun_Number is Integer with
> 
>       Dynamic_Predicate => Random = More_Fun_Number;

:-)

Prolog has a "maybe" that succeeds a certain percentage of calls. This could be used to implement it.

   declare
      X : More_Fun_Number;
   begin
      return Success;
   end;
exception
   when other => return Failure;

Maybe Ada will grow non-determinism.

Re: File_Exists (Was: Press Release - Ada 2012 Language Standard Approved by ISO)

[Yannick Duchêne (Hibou57)]

Le Fri, 11 Jan 2013 17:19:37 +0100, Jacob Sparre Andersen <sparre@nbi.dk>  
a écrit:

> Dmitry A. Kazakov wrote:
>
>> Never use File_Exists if you can.
>
> One of my colleagues could come up with a sensible use case for
> "File_Missing": When a web service wants to know if it should ask a user
> to upload a profile image (stored in a file).
>
> Some applications use the existence of certain files as a simple
> external management interface.  Although I consider this bad style and
> prefer a socket based management interface, it might be considered a
> reasonable use as well.
>
> Can anybody supply some other sensible use cases for
> File_Exists/File_Missing.

A build system? (not restricted to building applications). One may want to  
check if the file exist, instead of trying to create or open it for  
rewrite and only then getting an exception if the file does not exist.


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Press Release - Ada 2012 Language Standard Approved by ISO

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 796 bytes --]

"Jacob Sparre Andersen" <sparre@nbi.dk> wrote in message 
news:87sj67r941.fsf@adaheads.sparre-andersen.dk...
> Yannick Duch�ne wrote:
>
>> I disagree a bit, and this case may suggest to use locks.
>
> Which file systems/operationg systems allow an application to take a
> lock on a directory?

Don't know of any! And *assuming* that only your application can 
create/modify a file is looking for trouble, as such an assumption could be 
violated by accident (some other program using a similar file naming scheme) 
or maliciousness.

In the real world, there are lots of things that you can't know in 
advance -- you are always going to need a way to propagate run-time errors, 
which is what exceptions excel at (much better than error codes, IMHO).

                               Randy.

Re: File_Exists (Was: Press Release - Ada 2012 Language Standard Approved by ISO)

[Georg Bauhaus]

On 11.01.13 17:19, Jacob Sparre Andersen wrote:

> Can anybody supply some other sensible use cases for
> File_Exists/File_Missing.

File_Exists (and stat(1)-like access to external resources)
can be fine when a program controls an installation at each
point in time. That is, no other (instance of a) program
can interfere.

It should be possible, then, to remove from consideration any
section of the Ada run-time system that provides for input or
output to File, since it won't be needed in this part of an
Ada program.

Re: File_Exists

[Jacob Sparre Andersen]

Yannick Duch�ne wrote:
> Jacob Sparre Andersen wrote:

>> Can anybody supply some other sensible use cases for
>> File_Exists/File_Missing.
>
> A build system? (not restricted to building applications). One may
> want to check if the file exist, instead of trying to create or open
> it for  rewrite and only then getting an exception if the file does
> not exist.

But you would also be interested in knowing the time-stamp of the file
(at least in all the build systems I know of), making
Ada.Directories.Modification_Time the relevant function to call.

Greetings,

Jacob
-- 
"I don't want to gain immortality in my works.
 I want to gain it by not dying."