Version 1.2 of ai12s/ai12-0238-1.txt

Unformatted version of ai12s/ai12-0238-1.txt version 1.2
Other versions for file ai12s/ai12-0238-1.txt

!standard 7.8(0)          17-10-05 AI12-0238-1/01
!class Amendment 17-10-05
!status No Action (8-0-0) 17-10-14
!status work item 17-10-05
!status received 17-09-25
!priority Very_Low
!difficulty Hard
!subject Delta package specifications
!summary
Add a mechanism, called delta package specifications, that allows one to declare additional package specifications that refine the main one.
!problem
Code maintenance considerations often involve restrictions on modifying source code base. Coding standards also often impose restrictions on the version of the Ada language accepted in the code baseline, and forbid vendor-specific pragmas and aspects. Such restrictions may be especially rigid in the case of package specifications. This prevents the programmers who maintain such code bases from taking advantage of crucial enhancements in the Ada language, such as contract programming, or vendor extensions delivered via aspects, in particular SPARK 2014. It also makes it harder to write and maintain programs for multiple architectures, when differences are limited to representation aspects.
!proposal
We propose introducing a new mechanism, the delta package specifications, that allows offloading restricted constructs to separate entities. The idea is that a new-functionality-aware compiler will consider main specification and its associated delta as a single compilation unit; at the same time delta specs may have different configuration management and coding standard rules than the main spec. Delta specs may also be entirely ignored by legacy compilers that don't support this.
!wording
Syntax
The BNF for the proposed syntax mimics the one for package specifications, and is only different by the addition of reserved word 'delta':
delta_package_declaration := delta_package_specification; delta_package_specification ::= package delta defining_program_unit_name [aspect_specification] is {basic_declarative_item} [private {basic_declarative_item}] end [[parent_unit_name.]identifier]
Legality Rules
Each basic_declarative_item that is not a representation item must "refine" some basic_declarative_item from the main specification. "Refinement" means that it corresponds to some original basic_declarative_item (following the completion rules), with potentially one or more additional aspect specifications. If the main basic_declarative_item is a package_declaration, its refinement is a delta_package_declaration. Moreover, basic_declarative_items that are basic_declarations must appear in the same order they appear in the main specification.
Static Semantics
If a partition contains both a specification and a delta specification associated with it, they form a single compilation unit, that is considered equivalent to a single specification that combines the two, according to the following rules: the additional aspect specifications introduced by a delta specification are appended to aspect specifications introduced by the main specification; the additional representation items are inserted immediately after a preceding basic_declarative_item that exists both in main and delta specification, or immediately before the first basic_declarative_item of the main spec.
Example
The following pair of package specification and delta specification:
package Rational_Numbers is
type Rational is private;
function "/" (X,Y : Integer) return Rational; function Num (R : Rational) return Integer; function Denom (R : Rational) return Integer; function "=" (X,Y : Rational) return Boolean;
private type Rational is record Numerator : Integer; Denominator : Integer; end record;
Global : Rational;
procedure Update_Global;
end Rational_Numbers;
package delta Rational_Numbers is
pragma Restrictions (No_Tasking);
function "/" (X,Y : Integer) return Rational
with Pre => Y /= 0 or else X = 0;
function "=" (X,Y : Rational) return Boolean
with Post => "="'Result = False or else
(Num (X) = Num (Y) and then Denom (X) = Denom (Y));
private
type Rational
with Type_invariant => Denominator /= 0 or else Numerator = 0;
for Rational use record
Numerator at 0 range 0 .. 31; Denominator at 4 range 0 .. 31;
end record;
Global : Rational; for Global'Size use 128;
procedure Update_Global with Global => Global, Test_Case => (Name => "test_global", Mode => Nominal);
end Rational_Numbers;
... is equivalent to the following complete specification:
package Rational_Numbers is
pragma Restrictions (No_Tasking);
type Rational is private;
function "/" (X,Y : Integer) return Rational with Pre => Y /= 0 or else X = 0; function Num (R : Rational) return Integer; function Denom (R : Rational) return Integer; function "=" (X,Y : Rational) return Boolean with Post => "="'Result = False or else (Num (X) = Num (Y) and then Denom (X) = Denom (Y));
private type Rational is record Numerator : Integer; Denominator : Integer; end record with Type_invariant => Denominator /= 0 or else Numerator = 0; for Rational use record Numerator at 0 range 0 .. 31; Denominator at 4 range 0 .. 31; end record;
Global : Rational; for Global'Size use 128;
procedure Update_Global with Global => Global, Test_Case => (Name => "test_global", Mode => Nominal);
end Rational_Numbers;
!discussion
Legality Rules
The objective is basically to only allow addition of constructs like aspect specifications in the delta specs.
To simplify implementations, the following specific basic_declaration restrictions may need to be enforced in the delta specifications: for type_declarations, only incomplete_type_declarations are allowed; task_declarations can not have task_definitions; object_declarations can not have initialization expressions; instantiations can not be refined;
...etc.
It seems beneficial to allow declaring in delta specs Ghost entities which aren't completions of any declarations in the main spec. However, Ghost entities are SPARK extensions, so crafting corresponding legality rule is tricky if Ada language itself doesn't specially recognize such entities. Does this make good case for considering Ghost aspect as a bona fide Ada aspect rather than SPARK-only extension?
!ASIS
** TBD.
!ACATS test
ACATS B-Tests and C-Tests are needed to check that the new capabilities are supported.
!appendix

From: Tucker Taft
Sent: Monday, September 25, 2017  1:55 PM

Here is an AI from an AdaCore engineer (Vasiliy Fofanov).  It has been through
a couple of levels of internal review.  Our sense is that it would be stronger
if it allowed for "ghost" declarations in the "delta," but we will need a
separate AI for the notion of "ghost" code.

[This is version /01 of this AI - Editor.]

****************************************************************

From: Jean-Pierre Rosen
Sent: Tuesday, September 26, 2017  3:22 AM

Some quick thoughts:

1) Actually, it looks a lot like a child package, except that there is not
another layer of packaging. Maybe we should build on top of the existing
child package model.

2) Following 1), I would suggest the syntax "delta package Pack is", like
"private package Pack.child is"

3) I wonder what happens if you have more than one delta package. Is it
allowed? If not, isn't it too restrictive?

****************************************************************

From: Steve Baird
Sent: Tuesday, September 26, 2017  4:35 PM

I am unconvinced that this problem should be dealt with at the level of the
Ada language definition.

In my opinion (based on the arguments I have seen presented so far), delta
packages might be a fine idea but there should be no mention of them anywhere
in the Ada language definition.

One could have a tool which produces the result of merging an original package
and a corresponding delta package. This tool could be implemented using
compiler technology, as opposed to some simple-minded textual transformation.
But there is no need for any mention of this in the Ada RM.

The RM says
   The text of a program consists of the texts of one or more
   compilations.

but it doesn't say anything beyond that about where these compilations come
from.

There have been discussions, for example, of storing library unit package
visible parts and private parts in two different files. An implementation
could choose to do this without any changes to the Ada language definition -
the Ada rules don't come into play until you reach the point where somehow
(and Ada doesn't care how) you have a compilation to present as input to the
compiler.

I see delta packages as being a similar situation.

There are, of course, good arguments against using preprocessors and similar
tools. I agree with those arguments. I claim there is no inconsistency between
this and my position.

In this case, I don't think the benefit of incorporating this construct into
the language definition (as opposed to a preprocessor-ish tool-based solution)
outweighs the costs in added language complexity.

It also seems (to me) that this is a much bigger change than it appears to be.
We don't want to take a first step down a slope without being aware that this
is what we are doing. Widely used programming languages in general (and Ada is
no exception) are not typically designed to handle something like "this source
code is frozen, but I need to change it". Coping with deficiencies in
version-control/build/configuration-management tools is just not part of the
problem domain. Having a specific proposal for a solution is, of course,
helpful but I still think we should back off and look at the bigger question
of whether the language specification is the right level for any solution to
this kind of problem.

This seems like a very un-Adaish construct. In the context of a single
partition, every client of a package spec (including the package's own spec
and body) must be aware of any corresponding delta. It's not at all like child
units, where the parent unit alone can still be sensibly referenced. It might
look at first glance as though there is some sort of separate compilation
going on here, but there isn't.

Finally, I have some detailed questions about this particular proposed
solution:

   -  Suppose we encounter a scenario where
      "we really need to change this frozen spec". So we introduce
      a delta package for it. A few years go by and now that spec
      (including the delta package) is frozen. Then the same situation
      arises. What happens now? Can more than one delta package apply
      to the same package? Do we invent "delta delta" packages?
      [Recall that "epsilon" is not an Ada reserved word.]
      In internal discussions at AdaCore, the consensus seemed to be
      "let's not worry about that case - don't let perfect be the enemy
      of good".

   -  Can a delta package be used to modify the spec of an instance of a
      generic package? I assume the answer is no - the intended
      implementation model is a source-to-source transformation,
      a preprocessor that runs ahead of the compiler front end.
      The preprocessor is still there - it's just hidden from users
      (and I think that users could be insulated from its
      existence just as well by a good IDE as opposed to hiding
      it inside the compiler).

   -  Would this be worth all the trouble it would introduce for
      tools? Adding a new kind of compilation unit has a lot of
      impact on tools, much more than most language changes.
      Consider debugging. Usually one of the benefits of supporting
      something at the language level as opposed to via a preprocessor
      is the way that developers can then debug at the source level.
      Does that apply in this case? If no, then that weakens the
      argument against using a preprocessor. If yes, then that's
      going to be a lot of work to implement and the result will
      (if it accurately reflects the original source) be ugly.
      Similar questions apply to, say, static analysis
      tools and to any tool which needs to generate messages about
      source constructs (including error messages generated
      during compilation). Or consider a vendor who provides
      a package spec and wants to provide an implementation of that
      spec in some form other than as compilable Ada source. What
      happens when some customer applies a delta package to the spec?
      Do we need a new No_Deltas restriction?
      Coping with that sort of thing would add up to a lot of work.

****************************************************************

From: Tucker Taft
Sent: Tuesday, September 26, 2017  4:51 PM

I think the main rationale for the delta package notion is to solve a problem
such as separation of proof code physically from implementation, or to
separate representation clauses and other machine-dependent annotations from
the functional code.  I agree that it is not an appropriate solution for
dealing with "frozen" code needing random patches (and it doesn't really solve
that problem in my view), but rather to deal with long-term maintenance of a
piece of code with its associated annotations of one sort or another, as two
separate version-controlled components.

****************************************************************

From: Steve Baird
Sent: Wednesday, September 27, 2017  7:42 PM

The proposed mechanism is (IMO) either too powerful or not powerful enough.

1) It is not powerful enough.
    As noted earlier, inventing a new kind of compilation unit is a very
    big change. If we are going to incur that kind of cost, I think we
    should at least talk about the ability to store visible parts and
    private parts in separate files. If we are going to incur a big
    cost, we should get a big benefit. [Note that I am not saying that
    storing the visible part and the private part of a package spec
    separately belongs in the language definition; only that it would
    be preferable (IMO) to the current proposal.]

2) It is too powerful.
    Although we might recommend that this capability only be used for the
    purposes that you describe, this isn't enforced and that detracts
    from code readability/maintainability.
    The idea that it is safe to ignore a delta package if you only care
    about "the functional code" relies on unenforced conventions.

    The elaboration of the following package

      package Delta_Test is
        subtype S is Integer range 1 .. 999
          -- with Static_Predicate => S /= 123
        ;

        Dim : constant := 1 + Boolean'Pos (123 in S);

        type Index1 is range 11 .. 22;
        type Index2 is range 33 .. 44;

        type Matrix is array (Index1, Index2) of Boolean;

        procedure Fire (Nuclear_Missile_Count : Index1);
        procedure Fire (Pottery_Vase_Count    : Index2);
     end;

     with Text_IO; use Text_IO;
     package body Delta_Test is
        procedure Fire (Nuclear_Missile_Count : Index1) is
        begin
           Put_Line ("Launching"
                     & Nuclear_Missile_Count'Image & " missiles.");
        end;
        procedure Fire (Pottery_Vase_Count    : Index2) is
        begin
           Put_Line ("Firing up kiln for"
                     & Pottery_Vase_Count'Image & " vases");
        end;
     begin
        Fire (Matrix'First (Dim));
     end;

   produces the output line
      Firing up kiln for 33 vases

   If we add a delta package which has the effect of uncommenting
   the commented out Static_Predicate aspect specification, the output
   changes to
     Launching 11 missiles.

   The delta package has changed the result of name resolution so that
   a different subprogram is being called (in addition to changing the
   value of a static expression, which is a readability/maintainability
   problem all by itself). This is a pretty fundamental change.

   If you are debugging unfamiliar code that is not behaving as you
   expect it to, you don't want to have to spend effort ruling out
   the possibility that somehow a delta package has invalidated your
   understanding of some package spec. Ada was designed with an
   emphasis on readability. Delta packages seem inconsistent with this
   design goal.

****************************************************************

From: Randy Brukardt
Sent: Friday, September 29, 2017  9:44 PM

> The proposed mechanism is (IMO) either too powerful or not powerful 
> enough.

I agree fully with Steve.

This mechanism appears to be an attempt to deal with the limitations of
typical version control. I've been saying for DECADES that version control
at the level of a source file is the wrong level of abstraction. (It never
worked well for Janus/Ada development, for example, we have many files that
are mostly the same but have a few differences for different hosts or targets.
In such a case, if maintenance is needed in the "same" part, it is likely that
the other versions will get out of sync.)

But this is NOT a language problem; it's a problem that is caused by outside
tools and thus should be fixed by outside tools.

I'm especially concerned about the maintainance problem that Steve mentions
under "too powerful". I don't know how anyone would be able to trust anything
with the possible presence of these modifying packages. You'd need a standard
tool that eliminated the effect of any such packages in order to have any idea
of what a particular package's declarations are. That seems to fly in the face
of "plain text" source code as typically thought of. (And if you have such a
tool, why not use it to create the Ada source code and forget about changing
the language?)

Perhaps such an idea limited to very specific cases (for instance, just
contract aspects) would make sense, but even there, the issue seems to be more
with overly limiting version control rather than expressive power of the
language.

As defined, it seems like an awful lot of work (definitionally and for
implementations) just to damage one of the primary goals (readability) of the
Ada language.

****************************************************************

From: Steve Baird
Sent: Friday, September 29, 2017  10:01 PM

> Perhaps such an idea limited to very specific cases (for instance, 
> just contract aspects) would make sense, but even there, the issue 
> seems to be more with overly limiting version control rather than 
> expressive power of the language.

And if the point is just getting clutter out of the way to improve readability,
that seems more like an IDE issue than a language issue.

****************************************************************


Questions? Ask the ACAA Technical Agent