adacore / ada-spark-rfcs Goto Github PK
View Code? Open in Web Editor NEWPlatform to submit RFCs for the Ada & SPARK languages
Platform to submit RFCs for the Ada & SPARK languages
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
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?
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.
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 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;
Split Ada into the embedded / system language here called Ada 1983 and into the application / RAD language Ada 202y.
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.
It is far above my level of competence to write this section.
This issue is more or less based on intuitive hunches and dreams.
Provide a possibility to handle Storage_Error
in Spark_Mode.
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
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.
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)
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.
Properties
in Ada and SPARKReplace_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),
Add(3,4) = 7
Add(3,-4) = -1
and Replace_Prefix("bla", "", "new") = "newbla"
for all I : Integer => Add(I,0) = I
andfor all p,n,r : String => Replace_Prefix(p&r, p,n) = n&r
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.
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.
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.
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:
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:
return (<>, "This is a lot better");
Allow the programmer to limit the operators available for user-defined scalar types using the scales of measurement concept (from statistics):
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;
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.
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).
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);
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.
None. This is a natural extension to Ghost semantics to allow its specification on generic formal parameters.
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;
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.
pragma Indention (ZYX, " ");
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.
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.
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
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
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;
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.
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.
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
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.
(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.
Allow for conditional expression execution.
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.
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.
Should be doable.
R := (when B /= 0.0
then A / B
else 1.0);
-- As above but focus on condition.
Ada enumerations offer several advantages over constants:
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.
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);
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.
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.
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.
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.
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.
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;
);
The motivation is the same as with other languages allowing trailing commas:
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.
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;
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.
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.
Make semicolon (';') optional in cases when statement end is known by program text context.
Lets make semicolon optional when not needed anyway..
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
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.
The semicolon (';') was introduced to help the parser.
This proposal is expected to be easy to implement in the compiler parser.
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));
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);
\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);
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)
There are two syntax aspects to this feature:
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:
"\s is a \s" with (Name, Profession)
"\s is a \s" % (Name, Profession)
"\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"\s is a \s" (Name, Profession)
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.
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?
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;
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.
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.
Not only standardize the programming language Ada but also
Furthermore, enable checking by tools, e.g. warning when function is NOT documented.
Now de facto standards exist, such as AdaDoc and GNATdoc.
However,
The documentation should support the following features
Allow a discriminant to constrain a scalar type in a record. For related MR RFC, see: #68.
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:
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.
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.
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.
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.
It should be easy to implement in the compiler.
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.