When overriding a function, the types of in and out arguments (including return arguments) can be changed according to The Liskov Substitution Principle.

In the example project attached below, the scale function of the Figure interface is a nice example

   function Scale (f : in FigureI; s : in Float) return FigureI is abstract
   overriding function Scale(c : in Circle; s : in Float) return Circle
   overriding function Scale(r : in Rectangle; s : in Float) return Rectangle

In the same example project, I tried to apply the Liskov Substitution Principle on the FigureGenerator and RectangleGenerator

function Generate (f : in FigureGeneratorI) return FigureI'Class is abstract;
overriding function Generate (r : in RectangleGenerator) return RectangleI'Class;

Despite that the compiler is aware of the relation between FigureI'Class and RectangleI'Class,
Ada doesn't support that. I get the error messages

        22:15 subprogram "Generate" is not overriding
        15:9 type must be declared abstract or "Generate" overridden
        11:15 subprogram "Generate" is not overriding

I have done a number of experiments (with/without 'Class; with/without access). All failed. Some however with another message

operation can be dispatching in only one type

Note that without the substitution of types everything is fine.

I know of other languages that do allow this.
I like the additional info on the return type and less need of type checking and casts.
E.g. currently I need this code snippet (taken from the main module of the example project)
despite the fact that I know a RectangleGenerator generates not just FigureI but even RectangleI instances.

  declare
      rg : constant RectangleGenerator.RectangleGenerator := RectangleGenerator.Make(3.0,4.0);
      f : constant FigureI'Class := rg.Generate;
   begin
       if f in Rectangle.RectangleI'Class then
         declare
            r : constant Rectangle.RectangleI'Class := Rectangle.RectangleI'Class(f);
         begin
            rectanglePut (r);
         end;
      end if;
  end;

Could Ada also support the Liskov Substitution Principle in more type hierarchies than just the overwriting type hierarchy?

The example project: OO.zip

During a meeting with AdaCore, Nexperia and ESI, we were asked by AdaCore to submit this issue to trigger a discussion to determine whether a RFC is justified.

Summary

I would like to open the discussion on a "feature" called trailing comma in Python, Rust, JavaScript, Kotlin, C99, or C++11.

Anywhere there is a comma-separated list, allow a trailing comma after the last element of the list.

For example allow:

   Plop : Array_Type (1 .. 4) := (
                                  1,
                                  2,
                                  3,
                                  4,
                                  );                               

Since this is Ada/SPARK, we could also allow trailing semi-colon:

   procedure Plop (
                   A : Natural;
                   B : Float;
                   C : Integer;
                   );

Motivation

The motivation is the same as with other languages allowing trailing commas:

• diffs that look cleaner for code reviews and version control
• easily reorder the lines
• easily comment/uncomment any item

Caveats and alternatives

At this point I don't see a negative side for this.

As far as alternatives, I've seen some codebases where people put the comma at the beginning of the list:

enum Channel {
    RED
   ,GREEN
   ,BLUE
};

Which works for adding new elements inside or at the end of the list. But the problem remains for the beginning.

Now that Ada 202x is around the corner i think it's appropriate to start talking about this.

Ada revisions take too long to come out, to the point it could affect Ada future and it's place in industry. It's time to admit that big revision every 10 years is not working anymore.

Popular programming languages have already moved on to a faster release schedule. C++ has a new revision every 3 years, Java has a new version semi-annually etc. It would be hard for Ada to remain relevant when all other languages evolve so fast. No one is going to wait for Ada 203x to have a borrow checker or pattern matching.

I'm not proposing anything, but i want to initiate a discussion on this topic. (I posted it here because Ada-comment sucks)

See #54 #55 #56 #57

The style could be enforced by:

pragma Style (Source, Original)
pragma Style (Source, Lightweight)

Problem

It's not possible to have a type that has a collection of refcounted pointers to itself as a component:

type Rec;

package Rec_Ref is new Refcounted (Rec);

package Rec_Ref_Vectors is new Ada.Containers.Vectors (Positive, Ref_Ref.Ref);

type Rec is record
   A, B : Integer;
   Children : Rec_Ref_Vectors.Vector;
end record;

Possible solution

We should investigate if it's possible to write a refcounted pointer type that works with an incomplete type. First investigations on GNATCOLL.Refcounted were inconclusive. If it's not possible, we should investigate what we can do at a language level to improve the situation.

Summary

Modern languages typically have the definition and implementation parts in one file.
Therefore, I propose .ada as extension for files in which the body part of a procedure/function is implemented where it is declared.
The .ada file may be seen as an .adb file that allows usage before declaration.

Motivation

With declaration and implementation split up, it is cumbersome to make changes to the definition.
Changing the name or type of the procedure, function, or parameter in one file must also be copied to the other.

Documenting is at the moment also suboptimal, because you mostly write documentation above/below the definition.
So you either have to copy and synchronise your documentation with the implementation, or accept the missing documentation in the implementation. Without the documentation above/below the implementation, I often need to check the declaration on what this procedure/function should do exactly.

The separation also makes formal verification more tedious, because pre- and postconditions are set in the definition.
These conditions are not copied to the implementation, where it would be helpful to know what the constraints are.
This leads to frequently jumping between .ads and .adb files.

.ada files would also keep declaration and implementation close together.
I have seen some repositories that have a separate "implementations" folder.
This makes synchronising the definition and implementation even worse.

Finally, I think .ada is a good extension for Ada language files.
Having a new extension also prevents backward compatibility issues.

Caveats and alternatives

• Compiler complexity

  I know the reason why languages like C and Ada had initially split declaration and implementation was compiler complexity.
  Since the compiler at least needs to parse everything twice to discover procedures, functions, etc. that are declared after being used.

  With modern hardware, this is not a problem anymore.

• Handling of privates

  Everything defined in the private section of an .ads file may be accessed in the implementation.

  This is still possible in .ada files, because the implementation is clearly separable from the declaration.
  So everything declared below the private marker is only accessible in the implementation parts.
  It also has the added bonus that it would be possible to use privates in pre-/postconditions.
  Which is not possible at the moment (as far as I know).
  Also the workaround with declaring private types at the top of .ads files is not needed anymore.

• Packages only used in the implementation

  At the moment declaration and implementation are split up, and packages only used in the implementation
  may not be specified in the .ads file.

  With the combination to one .ada file, this is not possible anymore.
  However, I do not see a real benefit of splitting with's for declaration and implementation.

  1. It should not affect the resulting binary
  2. Why should package includes be hidden and from whom?

• Documentation placement

  I have seen some repositories that have the documentation below the declaration.
  From what I know, the reason is "better" readability of the declaration itself.

  With the combination, having the documentation below is probably not what most want.
  This leaves two options:

  1. Only consider documentation above a declaration as documentation for this declaration(this is the case for most languages)
  2. Allow documentation between declaration and implementation (similar to Python)

Summary

Provide a possibility to handle Storage_Error in Spark_Mode.

Motivation

Currently, exception handling is not allowed in Spark. Since the abscence of all run-time errors except Storage_Error can be proven, I don't see a way to write a full program in Spark_Mode.
If one writes most code in Spark_Mode, except at program entry to handle a Storage_Error, one might lose the possibility to safely recover from the exception.

See: How to check for Storage_Error in Spark_Ada for further motivation

Caveats and alternatives

Adding full exception handling support is probably beyond any achievable scope, but maybe an alternative can be found since it is only one specific exception.
As an alternative, some kind of size check could be used to compare the available stack/heap size with the size that will be allocated, but this might result in a lot of if-checks.

During a meeting with AdaCore, Nexperia and ESI, we were asked by AdaCore to submit this issue to trigger a discussion to determine whether a RFC is justified.

Documentation as part of the Ada Language Standard

Understandability is key

• Code is more often read than written by humans.
• Documentation is as important for human understanding as the Ada code
• Documentation should be treated as a first class citizen, just as Pre and Post conditions
• We would like our source code to be the single source of truth, so documentation should be integrated with the code as much as possible.

Standardization

Not only standardize the programming language Ada but also

• Integrated documentation,
• Pre-conditions, post-conditions, invariants,
• Examples, Test cases, Properties
• ...

Furthermore, enable checking by tools, e.g. warning when function is NOT documented.

Current Situation

Now de facto standards exist, such as AdaDoc and GNATdoc.
However,

• Documentation is hidden in comment, and NOT an aspect like Pre and Post conditions
• Refactoring tooling can ignore documentation since it is NOT official part of the language. This hampers both productivity and adoption of refactoring tooling.
• The de facto standards differ not only among each other, but also with other programming languages.
  Many developers have prior experience with other languages before learning Ada. See e.g. javadoc and Doxygen. Please keep the adoption of Ada as simple as possible.
• tools differ in their implementation.
  E.g. GPS and GNATStudio treat GNATDoc differently in specific cases.

Features

The documentation should support the following features

• Documentation of declarations and their parameters.
• Support for references to language elements, such as functions and packages.
• Support for figures. Specification of state machines, UML, and SysML. (Via PlantUML or graphviz/dot)
• Control over elements in automatically generated figures, like call-graphs, to prevent too large and unreadable graphs when all elements are included.
  Examples of control include the selection based on kind, depth, and scope (file, package, set of packages).

So I was thinking about string formatting in Ada and I want to discuss the concept below. I don't know if something similar was already proposed.

The idea would be to add something that is essentially syntactic sugar.

Syntax is discussed at the end.

This:

function Plop (Name, Profession : String) return String
is ("\s is a \s" with (Name, Profession));

Whould be equivalent to this:

function Plop (Name, Profession : String) return String
is (Name & " is a " & Profession);

It would be a compile time feature, so only applicable to string literal.
This is not allowed:

function Plop (Fmt, Name, Profession : String) return String
is (Fmt with (Name, Profession));

Bonus 1 : Escape characters

We could add escape characters: \n for ASCII.LF, \t for ASCII.HT, etc.

function Plop (Name, Profession : String) return String
is ("\t\s is a \s\n" with (Name, Profession));

vs

function Plop (Name, Profession : String) return String
is (ASCII.HT & Name & " is a " & Profession & ASCII.LF);

Bonus 2 : Automatic images

\i could mean to automatically apply attribute 'Img:

function Plop (Name, Profession : String; Year : Positive) return String
is ("\t\s is a \s since \i\n" with (Name, Profession, Year));

vs

function Plop (Name, Profession : String; Year : Positive) return String
is (ASCII.HT & Name & " is a " & Profession & " since " & Year'Img & ASCII.LF);

Bonus 3 : Inserts length

We could specify the desired length for the inserted text:

function Plop (Name, Profession : String; Year : Positive) return String
is ("\t\20s is a \s since \i\n" with (Name, Profession, Year));

(I don't know an easy way to do that with current language features)

Syntax

There are two syntax aspects to this feature:

Format operator

This is the relation between the format string "\s is \s" and the strings to be inserted (Name. Profession).

I see multiple ways to do that:

• An existing keyword: "\s is a \s" with (Name, Profession)
• A new operator: "\s is a \s" % (Name, Profession)
• Attribute: "\s is a \s"'Format (Name, Profession) (the combination of double and single quote is quite ugly to be honest)
• String'Format ("\s is a \s", Name, Profession) as suggested by @clairedross
• A la subprogram call: "\s is a \s" (Name, Profession)

Token

I used \s in the example above because that is the most familiar to me and it also allows for other escape characters \n, \t, etc.
But it could be %s a la Python/Java, {0} a la C#/Rust, etc.

Summary

Split Ada into the embedded / system language here called Ada 1983 and into the application / RAD language Ada 202y.

Motivation

Ada is a big language. It could be advantageous to split it into two language branches. This will reduce toolchain, standard library, and runtime system complexities.

Ada 1983 = Ada 83 added lessons learned from Ada 95 .. Ada 2023. Without OOP, Child units.
Ada 202y = Ada 2023 subtracted low-level like real-time, pragma, atomic, representation, access, aliased

Ada 1983 will be the 'real' Ada
Ada 202y could be the base of a myriad of other languages with various syntactic traits.

Ada 1983 is for the bare metal target.
Ada 202y is for the OS target.

The two branches should work together effortlessly.

Caveats and alternatives

It is far above my level of competence to write this section.

Disclaimer

This issue is more or less based on intuitive hunches and dreams.

Summary

Allow the programmer to limit the operators available for user-defined scalar types using the scales of measurement concept (from statistics):

1. Ratio scale: Regular numeric type, no limitation on the operations available. For example, a duration in seconds can be multiplied or divided by other durations / constants / other physical magnitudes. Typical physical magnitudes have this scale, and every statistical function can be used with a set of these values (e.g. geometric mean, arithmetic mean, relative standard deviation...)
2. Interval scale: Some physical magnitudes in which the absolute value has an arbitrary origin (e.g. ambient temperature in degrees Celsius, or Unix timestamp), so cannot be multiplied or divided (by elements of this type or any other type), or to add them together (it is possible to subtract them, but the result would be a relative magnitude). For example, two Unix timestamps can be subtracted (i.e. so the arbitrary origin is cancelled), giving a duration in seconds (but has no sense to add two Unix timestamps, or to divide it by a constant or other physical magnitude). It is possible to use the arithmetic mean and standard deviation (but not the geometric mean or relative standard deviation, as interval values cannot be multiplied/divided together).
3. Ordinal scale: Typical enumerate values, which can be compared together for equality or ordering. For example, a message priority can be low, medium, and high. It is not possible to get the arithmetic mean or standard deviation (as each enum value has not a clear value), but for a set of values it can be obtained for example the median / mode / interquartile range / variation ratio...
4. Nominal scale: Restricted enumerate values without order between them, so only equality / inequality allowed (but not less than, greater than, etc.). For example, a set of colors. It is possible to get the mode or the variation ratio, but is not possible for example to get the median (as the set of values cannot be ordered).

Reference-level explanation

A possible way to add scales of measurement to the language is to create a dedicated aspect, for example:

type Relative_Temperature is digits 6 range -1_000_000.0 .. +1_000_000.0 with Measurement => Ratio_Scale;

type Absolute_Temperature_Celsius is new Relative_Temperature range -273.15 .. 1_000_000.0 with Measurement => Interval_Scale;

type Absolute_Temperature_Kelvin is new Relative_Temperature range 0.0 .. 1_000_273.15 with Measurement => Interval_Scale;

A derived type is needed because a subtype will not avoid assigning by mistake a relative temperature into an absolute temperature. It is possible to use physical units with these types (e.g. using GNAT-specific aspect Dimension_System), but only relative temperatures can be mixed with other magnitudes, it has no sense to multiply / divide / add / subtract an absolute temperature with other physical values. Note that even if Kelvin degrees has no arbitrary origin (e.g. has physical sense to multiply an absolute temperature in Kelvin by two as its origin is zero), the programmer in this case represented it with an Interval_Scale type to ensure the program doesn't mix by mistake absolute temperatures and relative temperatures.

By default, all numeric types have the Ratio_Scale (i.e. all relational and arithmetic operators allowed), but in a type with Interval_Scale is allowed to use relational operators but not arithmetical operators. To perform the few allowed arithmetical operations in variables with an interval scale, one possibility is to have dedicated attributes (as they require mixing relational and absolute variables, and it would be weird to operate / assign variables that are not subtypes).

-- Rel := Abs1 - Abs2;
Temp_Increase : Relative_Temperature := Absolute_Temperature_Celsius'Interval_Diff(Current_Abs_Temp, Previous_Abs_Temp);

-- Abs2 := Abs1 + Rel;
Max_Temp_Limit : Absolute_Temperature_Celsius := Absolute_Temperature_Celsius'Interval_Add(Current_Abs_Temp, Temp_Increase);

In this proposed syntax, the compiler must check that the type with an Interval_Scale has a parent type with a Ratio_Scale, and also that the 'Interval_Diff attribute is used only with a Interval_Scale type, receiving two values of that type, and the result has the type of the parent type (i.e. has a Ratio_Scale); and similarly for the 'Interval_Add attribute (but accepting first a parameter of that Interval_Scale type, and second a parameter of the associated parent type, i.e. with a Ratio_Scale).

In the case of enumerate types, by default the Measurement aspect is "Ordinal_Scale" (i.e. regular enum, all operations accepted). But if "Nominal_Scale" is used in an enumeration type, the compiler will reject using relational operators (except equality and inequality) and some attributes (like 'Max and 'Min). It is allowed to iterate in loops variables with Nominal_Scale (or to use 'Pred or 'Succ).

Note that it is possible to convert explicitly an interval / nominal type to a base type so the programmer can "escape" from the limitations, for example to compute the arithmetic mean value of a set of absolute temperatures it would be needed to convert them to a generic Real to add them and divide the result by the number of values (something not allowed with values of an Interval_Scale)

Finally, it would be important that generic functions / packages also support the Measurement aspect, to indicate which types are allowed when instantiating it (and which operations are allowed inside the generic implementation). For example:

generic
  -- Allowed any scalar type (can have Nominal_Scale, Ordinal_Scale, Interval_Scale, or Ratio_Scale)
  type T is (<>) with Measurement => Scale_Nominal;
  type T_Array is array(Positive range <>) of T;
function Mode(values : in T_Array) return T;

generic
  -- Allowed all scalar types except those with Nominal_Scale
  type T is (<>) with Measurement => Scale_Ordinal;
  type T_Array is array(Positive range <>) of T;
function Median(values : in T_Array) return T;

Motivation

Embedded software typically has to operate with absolute / relative quantities, as well as with enumerate values without any order. The Ada philosophy is to give the programmer tools to explicitly indicate which are the properties of each data type, so the compiler ensures at compilation time that the code has no typing mistakes.

And the scales of measurement are not only for physical quantities, for example it can be useful to define a Device_Address type of Interval_Scale (with parent type Byte_Offset of Ratio_Scale) for example to ensure addresses are not added together.

Caveats and alternatives

Currently the Ada standard library uses private types for absolute times and relative times, and a set of functions with all the allowed operators (in Ada.Calendar and Ada.Real_Time, e.g. function "+" (Left : Time; Right : Duration) return Time;). This ensures that the relative and absolute times cannot be operated incorrectly, but for the programmer it is a lot of effort to define all these functions (as well as error-prone, and with a code overhead). In addition, it is not possible that the standard library defines all possible absolute and relative types, as in some cases depends on the context (e.g. a color type can be unordered if primary colors, or ordered if following a specific colorimetry; or a company profit in dollars has an interval scale in case negative values accepted, or ratio scale if only zero or positive values accepted).

Summary

Analogous to the TLA+ EXCEPT operator (see https://lamport.azurewebsites.net/tla/book-21-07-04.pdf, section 5.2), enhance Ada delta aggregates to support updates to components of components, components of components of components, etc.

The following example demonstrates the capability, but not necessarily the best language design choice for the syntax.

This hypothetical syntax (which, again, is not necessarily the best syntax; that should be debated):

base_expression with delta '(' choice_expression1 ')' '.' component_selector_name1 '(' choice_expression2 ')' '.' component_selector_name2 => expression

Would be equivalent to this:

base_expression with delta choice_expression1 => base_expression '(' choice_expression1 ')' with delta component_selector_name1 => base_expression (' choice_expression1 ')' '.' component_selector_name1 with delta choice_expression2 => base_expression (' choice_expression1 ')' '.' component_selector_name1 '(' choice_expression2 ')' **with delta component_selector_name2 => expression

Motivation

When using SPARK to specify procedures that modify just one state variable inside a nested data structure such as shown above, one delta aggregate expression is substantially easier to comprehend than a sequence of delta expressions.

Caveats and alternatives

(1) The syntax would need to be debated. In particular, my suggestion above to use parentheses to wrap choice expressions is suspect.

(2) I have not thought through whether all current features of delta aggregates fit neatly with the proposed feature. For example, I am unclear on whether a component_choice_list with multiple component_selector_names should be supported in combination with the proposed feature.

When creating overlays with the Address attribute, default values might become an issue. For example, let's say we have the following type declaration:

    type Unsigned_8 is mod 2 ** 8 with Default_Value => 0;

    type Byte_Field is array (Natural range <>) of Unsigned_8;

If we create an overlay, the default value will be used to initialize the overlay. For example:

    procedure Use_Overlay (V : in out Integer) is
       BF : Byte_Field (1 .. V'Size / 8)
         with Address => V'Address, Volatile;
         --  BF is initialized with Default_Value of Unsigned_8
    begin
       null;
    end Use_Overlay;

We may use the Import aspect to solve this problem:

    procedure Use_Overlay (V : in out Integer) is
       BF : Byte_Field (1 .. V'Size / 8)
         with Address => V'Address, Import => True, Volatile;

There are, however, two problems with the Import aspect:

• As soon as we restrict this aspect in our configuration — using pragma Restrictions (No_Use_Of_Pragma => Import); —, the solution above won't compile anymore.

• It's non-intuitive: nothing in its name is saying that the aspect is meant to prevent default values from being used.

We could, however, introduce a distinct aspect for this case. For example:

    procedure Use_Overlay (V : in out Integer) is
       BF : Byte_Field (1 .. V'Size / 8)
         with Address => V'Address, Use_Default_Value => False, Volatile;

What do you think? Is it worth creating an RFC for this new aspect?

In ai12-0212-1 it's implied that "empty" constants (ie Empty_Vector, Empty_Set etc) should be functions now, but in current Ada 202x draft (Draft 21) they're still constants. I suspect this is not intentional. Is it a bug?

A proposal from Emmanuel Briot made a long time ago

When Variable_Indexing, Constant_Indexing and the iterators were introduced in Ada2012,
they were added to the Ada.Containers hierarchy, but somehow Ada.Strings.Unbounded got
forgotten.

This proposal is about adding those aspects to unbounded_string.
See also my blog post on GNATCOLL.Strings:
http://blog.adacore.com/admin/entries/blog/1531-user-friendly-strings-api
for an example of actual code where these aspects are used.

Tagged

Unfortunately, an unbounded string is not visibly tagged (although I can’t imagine an implementation
where it would not be tagged). The user-defined indexing aspects only apply to tagged types, so we
would perhaps need to make unbounded_string visibly tagged (unless the aspects work if the type
is tagged in the private part).

Making them visibly tagged has the added benefit that one can start using the prefix notation to call
the primitive operations.

Constant_Indexing

We want to be able to write S (1), S (2), …
This is pretty trivial to added:

type Unbounded_String is private
     with Constant_Indexing => Element;

would do the trick

Variable_Indexing

This is more complex to implement when we also have copy-on-write, although it can be done. See my
blog post for details on the impementation

Iterators

Currently, we have to write

    for Idx in 1 .. Ada.Strings.Unbounded.Length (S) loop
        C := Ada.Strings.Unbounded.Element (C);
    end loop;

We are missing the “for..of” loop:

   for C of S loop
      …
   end loop;

and perhaps a loop on the indexes:

  for Idx of S.Iterate loop
      C := S (C);   —   using the constant_indexing aspect
  end loop;

I'd like to propose using the new Static aspect for more complex functions. What do you think?

Here is a draft version of the proposal. Please let me know if there's a way to implement the use-case below using features that are already available in Ada.

Static compile-time functions

Compile-time functions are useful to initialize data that is known to be static. A common use-case (lookup tables) is presented below. In Ada, it is possible to use the new Static aspect to declare static expression functions:

   function If_Then_Else (Flag : Boolean; X, Y : Integer) return Integer is
     (if Flag then X else Y) with Static;

However, the use of this aspect is limited to expression functions. It would be very useful to allow more complex implementations, such as:

   type Float_Array is array (Natural range <>) of Float;

   function Generate_Table (First, Last : Natural) return Float_Array
     with Static;

In C++, for example, constexpr can be used for this purpose.

Lookup tables

Lookup tables are typically used in situations where the computation cost of a function is too high. This is particularly useful for embedded programming. Instead of computing a function, using pre-computed data from ROM can provide similar precision at much lower computation cost.

For example, let's say we want to implement a lookup table for the sine function. We could use this approach:

package Tab_Generator is

   type Float_Array is array (Natural range <>) of Float;

   function Gen_Sin_Tab (Last : Positive) return Float_Array;

end Tab_Generator;


with Ada.Numerics;
with Ada.Numerics.Generic_Elementary_Functions;

package body Tab_Generator is

   package Float_Elementary_Functions is new
     Ada.Numerics.Generic_Elementary_Functions (Float);

   function Gen_Sin_Tab (Last : Positive) return Float_Array
   is
      use Ada.Numerics;
      use Float_Elementary_Functions;

      F_Last  : constant Float := Float (Last);
      Half_Pi : constant := (Pi / 2.0);
   begin
      return FA : Float_Array (0 .. Last) do
         for I in FA'Range loop
            FA (I) := Sin (Float (I) / F_Last * Half_Pi);
         end loop;
      end return;
   end;

end Tab_Generator;


with Tab_Generator; use Tab_Generator;

package Math_Tabs
is
   Sin_Tab : constant Float_Array;
private
   Sin_Tab_Last : constant := 180;

   Sin_Tab : constant Float_Array := Gen_Sin_Tab (Sin_Tab_Last);
end Math_Tabs;

Here, the lookup table Sin_Tab is generated by calling Gen_Sin_Tab. The problem with this approach is that Sin_Tab won't be stored in ROM. Instead, it will be computed at run-time.

In order to have the information as static data, we could create and run a separate application that generates a package specification with that table before building the actual application. For example:

with Ada.Text_IO; use Ada.Text_IO;

with Ada.Numerics;
with Ada.Numerics.Generic_Elementary_Functions;

procedure Generate_Sin_Table is

   package Float_Elementary_Functions is new
     Ada.Numerics.Generic_Elementary_Functions (Float);

   type Float_Array is array (Natural range <>) of Float;

   function Gen_Sin_Tab (Last : Positive) return Float_Array is
      use Ada.Numerics;
      use Float_Elementary_Functions;

      F_Last : constant Float := Float (Last);
      Half_Pi : constant := (Pi / 2.0);
   begin
      return FA : Float_Array (0 .. Last) do
         for I in FA'Range loop
            FA (I) := Sin (Float (I) / F_Last * Half_Pi);
         end loop;
      end return;
   end;

   Sin_Tab_Last : constant := 180;

   Sin_Tab : constant Float_Array
     := Gen_Sin_Tab (180);

   F_Ads, F_Adb : File_Type;
begin
   Create (F_Ads, Out_File, "math_stat_tabs.ads");

   Put_Line (F_Ads, "package Math_Stat_Tabs is");
   Put_Line (F_Ads,
             "   Sin_Tab : constant array (0 .. "
             & Sin_Tab_Last'Image & ") of Float := ");

   Put_Line (F_Ads,
             "               (" & Sin_Tab (Sin_Tab'First)'Image & ",");
   for V of Sin_Tab (Sin_Tab'First + 1 .. Sin_Tab'Last - 1) loop
      Put_Line (F_Ads,
                "                " & V'Image & ",");
   end loop;
   Put_Line (F_Ads,
             "                " & Sin_Tab (Sin_Tab'Last)'Image & ");");
   Put_Line (F_Ads, "end Math_Stat_Tabs;");

   Close (F_Ads);

end Generate_Sin_Table;

After building and running this application, we'd get:

package Math_Stat_Tabs is
   Sin_Tab : constant array (0 ..  180) of Float :=
               ( 0.00000E+00,
                 8.72654E-03,

                 --  skipping some values...

                 9.99962E-01,
                 1.00000E+00);
end Math_Stat_Tabs;

Now, when building the actual application, Sin_Tab is stored as static data (in ROM).

One of the problems with this approach is that it makes the build process more complicated by requiring a pre-build step. A more elegant solution could be achieved by allowing the Static aspect for Gen_Sin_Tab. For example:

package Math_Stat_Tabs_New is

   type Float_Array is array (Natural range <>) of Float;

   function Gen_Sin_Tab (Last : Positive) return Float_Array
     with Static;

   Sin_Tab : constant Float_Array;

private
   Sin_Tab_Last : constant := 180;

   Sin_Tab : constant Float_Array := Gen_Sin_Tab (Sin_Tab_Last);

end Math_Stat_Tabs_New;

Proposal

Allow for conditional expression execution.

Examples

R := 1.0;
R := (A / B when B /= 0.0);
-- A / B is evaluated and put into R when B /= 0.0 to avoid division by zero.

R := (A / B
          when B /= 0.0
          else 1.0);
--  A / B is evaluated and put into R when B /= 0.0 to avoid division by zero. Otherwise 1.0 is put into R.

Rationale

This proposal may look like (if cond then expr1 else expr2) expression, but only then selected expressions is executed. The false branch is guaranteed to not being executed.

Implementation

Should be doable.

Alternative

R := (when B /= 0.0
           then A / B
           else 1.0);
--  As above but focus on condition.

Summary

Analogous to C++ using-declarations, and analogous to the "from" form of Python import statements, add a fourth kind of Ada use clause that uses a name from a package. For example:

	procedure Example is
		package A is
			function Foo(x : Integer) return Integer;
			function Foo(x : Float) return Float;
		end A;
		package body A is
			function Foo(x : Integer) return Integer is begin return x; end Foo;
			function Foo(x : Float) return Float is begin return x; end Foo;
		end A;
		-- New syntax:
		use A.Foo;
		-- Existing syntax:
		-- function Foo(x : Integer) return Integer renames A.Foo;
		-- function Foo(x : Float) return Float renames A.Foo;
		Result1 : Integer;
		Result2 : Float;
	begin
		Result1 := Foo(0);
		Pragma Unused(Result1);
		Result2 := Foo(0.0);
		Pragma Unused(Result2);
	end Example;

Motivation

If at some place within the scope of a use_clause, a naming conflict exists between a declaration in that scope and a declaration made potentially use-visible at that place by that use_clause, references to the identifier of the declarations may result in confusion as to which declaration is referenced through that identifier.

To mitigate this potential confusion, some critical software is compiled with configuration options that will cause compilation errors wherever such naming conflicts exist, or at least in some cases where such naming conflicts exist. For example, this effect can be achieved with the GNAT toolchain by combining the -gnatwh and -gnatwe compiler switches.

However, this approach threatens forward compatibility of the software that includes the use_clause. A naming conflict might not exist as of when the software with the use_clause is developed, but a subsequent addition to the package being used might introduce such a naming conflict. Such a naming conflict would have the undesired effect of causing compilation of the software with the use_clause to fail with errors.

Consequently, it is arguably not appropriate for critical software being developed at scale to include use_package_clauses and use all type clauses. (The same concerns do not apply to use type clauses, however, since these only make primitive operators potentially use-visible, and primitive operators are syntactically limited in ways that mitigate the risk of confusion.)

An alternative approach is for critical software to utilize package renaming declarations to define shorthand. However, for frequently used declarations within another package, package renaming declarations are syntactically suboptimal.

As shown in the example above, optimal syntax for each reference to a subprogram declaration in another package can be accomplished with subprogram renaming, but subprogram renaming is even more cumbersome to use than package renaming, given the need to reiterate subprogram parameters and return types and to cover each overloaded declaration.

The ability to use a specific name from a package would address the above concerns elegantly and in a manner consistent with other modular programming languages that prioritize "safe" importing of specific content from other modules.

It would be helpful to have "subtypes" for access to class-wide types with allows to limit allowed values to to some derived type and types derived from it, and to avoid explicit type conversion. Here is an example of type declaration:

type T1 is tagged private;
type T1_Access is access all T1'Class;

type T2 is new T1 with private;
type T2_Access is access all T2'Class;
subtype T2_Access_Subtype is T1_Access for access all T2'Class;  -- new constructuion

and its use case:

procedure P (Item : T1_Access);

X1 : T2_Access;
X2 : T2_Access_Subtype;

P (T1_Access (X1));  --  type conversion is necessary
P (X2);              --  type conversion is not needed

We at ESI perform among others code analysis.
We would like to present the code analysis results in a straight forward way.
One such way is incorporating the analysis results in the original code,
since the developers are familiar with that code.
However, we prefer to minimally change the layout of the code (including line numbers) to keep that familiarity.
In other language, we can use a comment block (e.g. /* */ in C).
Ada lacks such a feature.
The user has no control over the location where a comment ends - it always ends with a line break.
Adding comment thus enforces a line break and thus change layout and line numbers.
We are aware of the discussion on stack overflow. Yet the discussion on stackoverflow focusses only on multi line comments. We have a need for comments that are smaller than a single line.

Just to give an illustrative example:
We prefer the analysis output

function Go (D /* 3,4,7 */, F /* 100, 1000 */ : Integer) return Integer;

over

function Go (D,          -- 3,4,7 
             F : Integer -- 100, 1000
            ) return Integer;

when the original code is

function Go (D, F : Integer) return Integer;

During a meeting with AdaCore, Nexperia and ESI, we were asked by AdaCore to submit this issue to trigger a discussion to determine whether a RFC is justified.

Summary

Allow a discriminant to constrain a scalar type in a record. For related MR RFC, see: #68.

Motivation

An example of use:

   type ChangeList is array (Natural range <>) of CacheChange;
   protected type HistoryCache (CacheSize : Positive) is
      procedure add_change (a_change : in CacheChange);
      procedure remove_change (a_change : out CacheChange);
   private
      changes : ChangeList (1 .. CacheSize);
      count : Natural range 1 .. CacheSize := 0;
   end HistoryCache;

Using GNAT Community 2020 (20200818-93), the compiler will throw the following error: discriminant cannot constrain scalar type

Given that in ADA 2012 a composite type can be parameterized using a discrimant, a range (consisting of a bound based on a discriminant value) specified for a scalar field would result in a constant range declaration.

References:

• [1] Discussion on Computer-programming-forum.com
• [2] Ycombinator thread

Caveats and alternatives

As discussed in the Computer-programming-forum.com thread [1], a similar approach is employing the following construct:

  generic
    CacheSize : in POSITIVE;
  package HistoryCache is
    type count is Natural range 0 .. CacheSize;
    changes : ChangeList (1 .. CacheSize);
  end Queue;

Would love to hear some thoughts on this matter.

During a meeting with AdaCore, Nexperia and ESI, we were asked by AdaCore to submit this issue to trigger a discussion to determine whether a RFC is justified.

Support for Properties in Ada and SPARK

Current Situation

• Ada supports test case specification with GNATTest.
  However, these specifications are tool specific.
  For example, the following test cases of the Replace_Prefix function are specified for GNATTest and can't be proven by SPARK to hold.

       Test_Case => ("Empty New Prefix and Remainder", Nominal),
       Test_Case => ("All Empty", Nominal),
       Test_Case => ("String not start with Prefix, String length larger than Prefix length", Robustness),
       Test_Case => ("String not start with Prefix, String length equal to Prefix length", Robustness),

• Other languages support the specification of examples in documentation which are automatically tested or proven as part of building and releasing the code. See for example doctest.
  • For example, Add(3,4) = 7
• Other languages support the specification of test cases (not just their names as in the GNATTest example above)
  • For example, Add(3,-4) = -1 and Replace_Prefix("bla", "", "new") = "newbla"
• Other languages support the specification of properties.
  • For example, for all I : Integer => Add(I,0) = I and
    for all p,n,r : String => Replace_Prefix(p&r, p,n) = n&r
• SPARK support GHOST code.
• SPARK supports multiple problem solvers. A user can choose to either check the code using one or all problem solvers.

Desired situation

• We would like to specify properties of the code in a tool independent way.
• We would like to treat simple properties, such as examples and test cases, the same as complicate properties, e.g. with for all statements.
• We might want to use GHOST code to keep the specifications of properties concise and readable.
• Properties should be automatically verified either as part of compilation or as a seperate phase before releasing.
• We would like to specify a hierarchy of tools: provide alternatives in case a tool is unable to verify a property. For example, if SPARK can't proof a particular property, a test case generator is used to verify that property by generating a large number of test cases with random inputs.
• We would like to specify the set of hierarchy of tools to verify the properties. Confidence of the verification increases when multiple test case generators with different startegies are used. A similar requirement for SPARK resulted in the possibility to use multiple problem solvers.

Proposal

Make semicolon (';') optional in cases when statement end is known by program text context.
Lets make semicolon optional when not needed anyway..

Example

procedure semicolon is
   i, n : natural
   c : constant positive := 123

   function func (p : integer) return integer
   function func (p : integer) return integer is
   begin
       return p + 5 + c
   end

begin
   null                  -- comment
   n := 3  ; n := c + 5 -- semicolon needed
   i := func (n)
end semicolon

Parser outputs

Outputs from GNAT compiler:

semicolon.adb:2:17: missing ";"
semicolon.adb:3:31: missing ";"
semicolon.adb:5:45: missing ";"
semicolon.adb:8:22: missing ";"
semicolon.adb:9:06: missing ";"
semicolon.adb:12:08: missing ";"
semicolon.adb:13:24: missing ";"
semicolon.adb:14:17: missing ";"
semicolon.adb:15:14: missing ";"

This indicates that the semicolon is redundant in many if not most cases.

Rationale

The semicolon (';') was introduced to help the parser.

Implementation

This proposal is expected to be easy to implement in the compiler parser.

To be able to have String or any other kind of unconstrained array in a record I often use the following pattern:

type Data (Str_Len : Natural) is record
   Str : String (1 .. Str_Len);
end record;

This is convenient and works for me most of the time. However one annoying aspect is that when writing an aggregate one has to update the discriminant when changing the string.
It's ok for short strings:

return (4, "test");

return (4, "But it is annoying for long string");

So I have two suggestions to discuss here:

• 1. I think the compiler error could be improved to give the expected value for the discriminant instead of just saying "wrong length for array".
• 2. Would it be possible to allow box notation here?

     return (<>, "This is a lot better");

Summary

Ada enumerations offer several advantages over constants:

• Improves code readability
• Defines a set of values as a single type
• Improves code safety
• Limits assignment to a set of values
• Defines a namespace for constants
• Ability to iterate over its values

Enumerations also have constraints. Their values must be either a numeric or a character type. Unfortunately, this creates severe limitations, rendering it anemic compared to other languages. Enumeration values need more type flexibility to enhance their expressive capabilities.

The code below demonstrates such a limitation with a brief explanation. For a more thorough discussion, including workarounds please refer to its source on stackoverflow:

type Bakers_Dozen is range 1 to 13;  -- Indices from 1 to 6 are donuts
subtype Donut is Bakers_Dozen (Plain, Chocolate, Strawberry, Glazed, Blueberry, Cannabis);
for Donut use (Plain=>1, Chocolate=>2, Strawberry=>3, Glazed=>4, Blueberry=>5, Cannabis=>6);  

PastriesBox[Plain].Message = "Plain Donut is boring but costs less";
PastriesBox[Donut'Last].Message = "Please read contradictions and disclaimer inside box.";
PastriesBox[12].Message = "A great tasting muffin with fresh goat milk.";

The intent of the specification is to build a baker's dozen of pastries with 13 numbered slots in a pastry box. The first 6 slots are reserved exclusively for donuts based on their type. Plain donuts go into the first slot, chocolate goes into the second slot, and so on. The rest of the slots are reserved for any other type of pastries. The last few lines are a usage scenario for the model. Clearly, the Donut enumeration values are used to index the slots in the pastry box, while numeric values are used to index regular pastry items.

Even though (NPI) Donut values are numeric, they cannot be subtyped like normal integers, nor can they be the same type as Bakers_Dozen. More broadly, constraining enumerations to only single characters or numeric types gives rise to this inflexibility. There's no reason why enumerations values can't support strings or any kind of value type.

Practical Use Case

Here's a real-world example to help illustrate the use case for this feature:

type Device_Address is mod 16#0F#;          -- 16 unique address location
for Device_Address'Size use 4;              -- Use only 4 bits for the address
subtype Fixed_Address is Device_Address (Serial, Parallel, PS2, Ethernet, Game, USB_1, USB2); -- Fixed addresses for default devices
for Fixed_Address use (0,1,2,3,4,5,6,7); 

Address : Device_Address := Game; 

Unfortunately, the code above will not compile. As a workaround, using a sub-type predicate will not compile either:

type Device_Address is mod 16#0F#;          -- 16 unique address location
for Device_Address'Size use 4;              -- Use only 4 bits for address
subtype Fixed_Address is Device_Address with
Static_Predicate =>
    Fixed_Address in (Serial, Parallel, PS2, Ethernet, Game, USB_1, USB_2);

Rewriting the code using constants works, but loses the aforementioned advantages of enumerations. Specifically, the code isn't as readable, loss of namespace and inability to iterate over the constant values.

    type Device_Address is mod 16#0F#;                                   -- 16 unique address location
    for Device_Address'Size use 4;                                             -- Use only 4 bits for the address space
    subtype Fixed_Address is Device_Address range 0 .. 6;    -- Lower half reserved for fixed devices
    Serial : constant Fixed_Address := 0;
    Parallel : constant Fixed_Address := 1;
    Ethernet : constant Fixed_Address  := 2;
    PS2: constant Fixed_Address := 3
    Game: constant Fixed_Address  := 4; 
    USB_1: constant Fixed_Address := 5; 
    USB_2: constant Fixed_Address  := 6;

Or as an alternative, adding a static predicate:

subtype Fixed_Address is Device_Address with Static_Predicate =>
    Fixed_Address in (Serial, Parallel, PS2, Ethernet, Game, USB_1, USB_2);

Motivation

Ada's enumeration constraints greatly reduce its utility. It often forces awkward, less safe, and less accurate workarounds when specifying a model, which is antithetical to Ada's stated principles. Increasing the flexibility of enumerations greatly expands Ada's expressive power.

Caveats and alternatives

There are workarounds offered on StackOverflow such as using constants and other more convoluted means, but they're incapable of modeling the problem as succinctly with the same level of accuracy, safety, and readability.

So long as Ada's type rules are respected, expanding enumerations values to support a wider range of types won't compromise in Ada's type system. Moreover, enumerations are constant values and should have no real side effects. Moreover, they do not introduce any significant performance or size penalties as constant value types can be optimized away at compilation.

pragma Indention (ZYX, " ");

Proposal

Statements are changed to allow conditional execution thereof based on the value of a boolean expression.
The when keyword should be used to indicate a conditional statement.

Examples

Stop (Car, Emergency) when PB_EMCY;
--  Emergency stop Car when the pushbutton PB_EMCY is pressed.

Compile when Change or Force_Compile;

LED_05 := Set   when PB_Start;
LED_05 := Clear when PB_Stop;
--  SR Flip-Flop.

Rationale

It would be nice to be able to execute a statement depending on when a boolean expression evaluates to True.
In many cases the program text would be shorter and arguably easier to read.

Implementation

It should be easy to implement in the compiler.

Alternative

when PB_Start then LED_05 := True;
when PB_Stop  then LED_05 := False;
--  SR Flip-Flop with focus on inputs.
--  The SR-FF in exmples has focus on output.

Summary

Currently, Ada only allows specifying the Size/Object_Size/Alignment of types with static values. This makes it impossible to specify them in generics when they refer to values from formal parameters. So the following code is rejected:

--  bytes.ads
package Bytes is

   type U32 is mod 2**32;

   generic
      type Payload is private;
   function Extract (Data : Payload) return U32;

end Bytes;

--  bytes.adb
package body Bytes is

   function Extract (Data : Payload) return U32 is
      type Arr is array (1 .. Payload'Size / U32'Size) of U32
        with Size => (Payload'Size / U32'Size) * U32'Size;
      Data_Arr : Arr with Address => Data'Address;
      Res : U32 := 0;
   begin
      for Value of Data_Arr loop
         Res := Res + Value;
      end loop;
      return Res;
   end Extract;

end Bytes;

--  use_bytes.adb
with Bytes; use Bytes;

procedure Use_Bytes is

   type Rec is record
      A, B, C : Integer;
   end record;

   R : Rec := (0, 1, 41);

   function Extract_Rec is new Extract (Rec);
begin
   pragma Assert (Extract_Rec (R) = 42);
end Use_Bytes;

Even without generics, Ada only allows specifying static values for Size/Object_Size/Alignment. This makes it impossible to compute such a value based on the Size/Object_Size/Alignment of other types. So the following code is also rejected:

procedure Use_Bytes is

   type Rec is record
      A, B, C : Integer;
   end record;

   R : Rec := (0, 1, 41);

   type U32 is mod 2**32;
   subtype Payload is Rec;

   function Extract (Data : Payload) return U32 is
      type Arr is array (1 .. Payload'Size / U32'Size) of U32
        with Size => (Payload'Size / U32'Size) * U32'Size;
      Data_Arr : Arr with Address => Data'Address;
      Res : U32 := 0;
   begin
      for Value of Data_Arr loop
         Res := Res + Value;
      end loop;
      return Res;
   end Extract;

begin
   pragma Assert (Extract (R) = 42);
end Use_Bytes;

Motivation

Infrastructure software needs sometimes to interpret data through different types, without copying it. This can be done by overlaying a variable on top of another one, specifying the address of one for the other, like in the examples above. Given that the type system of Ada does not guard against reading too little or too much data here, it would be safer to specify the intended Size/Object_Size/Alignment of the overlay. This is also needed for the SPARK tool to be able to verify statically that the overlay does not allow reading past the overlaid object.

Caveats and alternatives

The alternative if to not specify the representation attributes of such types, and let the compiler decide, but check them with the GNAT-specific pragma Compile_Time_Assert, as in:

pragma Compile_Time_Error (Arr'Size /= (Payload'Size / U32'Size) * U32'Size, "unexpected size for Arr");

Note that the semantics of this pragma are subtle, as it's not guaranteed to fail at compilation if the compiler frontend cannot determine statically the value of the expression. The SPARK tool takes a stricter approach and issues a message if it cannot determine that the expression is always False. This would be the outcome currently (a message from SPARK tool), but possibly the tool could be modified to link that kind of assertions with the corresponding type, as a kind of heuristic replacement for the corresponding representation aspect or clause.

Summary

RM-3.5.4(9) imposes a symmetric base range for signed integer types. I would like to remove the need for a symmetric base range because it imposes the use of larger types to perform arithmetic operations, potentially burdening embedded applications with undesirable run-time needs and performance overhead.

My proposal for RM-3.5.4(9) would be the following rewording:

A range_integer_type_definition defines an integer type whose base range includes at least the values of the simple_expressions. A range_integer_type_definition also defines a constrained first subtype of the type, with a range whose bounds are given by the values of the simple_expressions, converted to the type being defined.

Motivation

You can define a 64-bit type containing values between 0 and 2**64-1 as:

type Unsigned_64 is range 0 .. 2**64-1 with Size => 64

Currently, the symmetric base range for signed integer types means that intermediate arithmetic operations on the previously defined 64-bit type are performed in 128-bit. It is also misleading because the Size aspect would let the coder think that it would use 64-bit operations.

Using a larger type can harm the performance of the operation, and sometimes force the operation to be implemented in software (within a run-time library) instead of hardware. This is particularly unfortunate for embedded applications. For example, on a 64-bit hardware architecture, a 64-bit multiplication can be performed with a single hardware instruction, while a 128-bit multiplication needs a series of hardware instructions working on intermediate results.

Caveats and alternatives

I do not see the value of defining a symmetric base range, but I may be missing something.

We could use a modular type definition to prevent the symmetric base range instead, but the semantics of the two integer type definitions are very different.

Summary

Currently, SPARK RM does not allow generic formal parameters. In particular, it is not possible to pass ghost subprograms as generic actual parameters in a generic instantiation. The following is illegal:

   generic
      type T is private;
      with function Precond (X : T) return Boolean;
      with procedure Callee (X : in out T);
   procedure Wrapper (X : in out T)
     with Pre => Precond (X);

   procedure Wrapper (X : in out T) is
   begin
      Callee (X);
   end Wrapper;

   function Not_Last (X : Integer) return Boolean is (X < Integer'Last)
     with Ghost;

   procedure Incr (X : in out Integer)
     with Pre => Not_Last (X)
   is
   begin
      X := X + 1;
   end Incr;

   procedure Inst_Incr is new Wrapper (Integer, Not_Last, Incr);

Motivation

Ghost and generics are two orthogonal features in SPARK that do not work ideally together currently. So that use of generics forces some logically ghost entities to be declared without the Ghost aspect, so that they can be passed as generic formal parameters.

Caveats and alternatives

None. This is a natural extension to Ghost semantics to allow its specification on generic formal parameters.