Ada conference, Ada and Spark

[Meta]

On Wednesday, 19 February 2014 at 23:55:16 UTC, bearophile wrote:
> Integral ranges and strong types:
>
>
> type Age   is range 0..125;
> type Floor is range -5 .. 15;

Is it possible to implement this using the information that's 
already available through Value Range Propagation? I think I 
remember Andrei describing it in TDPL as numeric values carrying 
around their ranges at compile time, but I don't remember exactly.

> My_Age  : Age;
> My_Floor : Floor;
> ...
> My_Age   := 10;       -- OK
> My_Floor := 10;       -- OK
> My_Age   := My_Floor; -- FORBIDDEN !

How close do you think std.typecons.Typedef is to supporting this 
functionality? Is it a sufficient replacement?

> Discriminated types:
>
>
> ype Major  is (Letters, Sciences, Technology);
> type Grade is delta 0.1 range 0.0 .. 20.0;
> type Student_Record (Name_Length : Positive;
>                      With_Major  : Major)
> is record
>    Name    : String(1 .. Name_Length); --Size depends on 
> discriminant
>    English : Grade;
>    Maths   : Grade;
>    case With_Major is     -- Variant part, according to 
> discriminant
>       when Letters =>
>          Latin : Grade;
>       when Sciences =>
>          Physics   : Grade;
>          Chemistry : Grade;
>       when Technology =>
>          Drawing : Grade;
>    end case;
> end record;

Ditto, except for with std.variant.Algebraic. It does need some 
work, but I think the important part is whether it's 
implementable in the library with a nice syntax. Then it only 
requires somebody to do the necessary work.

> Low level description of a record:
>
>
> type BitArray is array (Natural range <>) of Boolean;
> type Monitor_Info is
>     record
>         On     : Boolean;
>         Count  : Natural range 0..127;
>         Status : BitArray (0..7);
>     end record;
> for Monitor_Info use
>     record
>         On     at 0 range 0 .. 0;
>         Count  at 0 range 1 .. 7;
>         Status at 0 range 8 .. 15;
>     end record;

Isn't this the same as a struct?

> Static predicates (related to the "enum preconditions" I 
> suggested for D):
>
>
> procedure Seasons is
>     type Months is (Jan, Feb, Mar, Apr, May, Jun,
>                     Jul, Aug, Sep, Oct, Nov, Dec);
>     subtype Summer is Months
>         with Static_Predicate => Summer in Nov .. Dec |
>                                            Jan .. Apr;
>     A_Summer_Month : Summer;
> begin
>     A_Summer_Month := Jul;
> end Seasons;
>
>
> The code gives:
>
> warning: static expression fails static predicate check on 
> "Summer"

What are the limitations on what Static_Predicate can verify? It 
seems like this could be quite powerful, but not as powerful as 
runtime checks, since not everything can be checked at compile 
time.

> A kind of set syntax:
>
>
> elsif First and then C in '+' | '0' .. ’9’ then

I think this would be quite easy to do using mixins. I've also 
been thinking about list comprehensions a la Python, done with 
mixins.

> Loop variants and invariants:
>
>
> procedure Loop_Var_Loop_Invar is
>    type Total is range 1 .. 100;
>    subtype T is Total range 1 .. 10;
>    I : T := 1;
>    R : Total := 100;
> begin
>    while I < 10 loop
>       pragma Loop_Invariant (R >= 100 - 10 * I);
>       pragma Loop_Variant (Increases => I,
>                            Decreases => R);
>       R := R - I;
>       I := I + 1;
>    end loop;
> end Loop_Var_Loop_Invar;

This is a neat feature. I thought it was unique to Wiley, but I 
guess the creator of Wiley must've got it from Ada. Does the loop 
break if the invariant fails, or does it stop the program?

> An example in Spark, to clarify access to global variables (for 
> D I suggested a simpler optional @outer() attribute: 
> https://d.puremagic.com/issues/show_bug.cgi?id=5007 ):
> ...

I don't think this is quite as important, seeing as D has the 
pure keyword.