www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Ada conference, Ada and Spark

reply "bearophile" <bearophileHUGS lycos.com> writes:
Related to the Mars lander software thread.

They have released the slides for the FOSDEM 2014 (1 February 
2014) conference about Ada and related things 
(http://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/1
/140201-fosdem.html 
).

Two interesting slide packs, one introduction about modern Ada 
2012, and the other about SPARK 2014, the latest version of a 
more formal language based on Ada:

http://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/14/140201-fosdem/01-ada-introduction.pdf

http://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/14/140201-fosdem/03-ada-spark.pdf


The slides contain many interesting examples, the first ones are 
Ada, the last two about Spark.

The "safety and correctness" given by Ada/Spark type systems, 
semantics and syntax are quite different from the "safety" given 
by Haskell. They share some qualities, but they are also based on 
quite different principles, and they have quite different 
purposes. I have seen lot of people write about the correctness 
and safety of Haskell programs, but they usually don't even keep 
in mind the existence of Ada/Spark. I don't fully understand this 
situation.

I think regarding "safety and correctness" D is midway between 
C++ and Ada.

One important thing that should be kept in mind when you think 
about the "success" of D contract programming (beside the current 
lack of old/pre-state in D) is that there are many kinds of D 
code: small script-like programs, GUIs, video games, heavy 
numeric software, large applications, and so on. Some of those 
kinds of code don't need much contracts. But in larger programs 
or in programs where you need a partial integrity (where you can 
also use Ada), it's useful.

--------------------------------------------

Integral ranges and strong types:


type Age   is range 0..125;
type Floor is range -5 .. 15;
My_Age  : Age;
My_Floor : Floor;
...
My_Age   := 10;       -- OK
My_Floor := 10;       -- OK
My_Age   := My_Floor; -- FORBIDDEN !

--------------------------------------------

Ranged not-integral value with optional delta:


type Density is delta 1.0/256.0 range 0.0 .. 1.0;

(So Density is represented with a single byte, despite it looks 
like a not integer number.)

--------------------------------------------

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;

--------------------------------------------

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;

--------------------------------------------

Example usage of both floating point ranges and invariants:


package Places is
     type Disc_Point is private;
     -- various operations on disc points
private
     type Disc_Point is
         record
             X, Y : Float range -1.0 .. +1.0;
         end record
         with Invariant => Disc_Point.X ** 2 +
                           Disc_Point.Y ** 2 <= 1.0;
end Places;

--------------------------------------------

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"

--------------------------------------------

A kind of set syntax:


elsif First and then C in '+' | '0' .. ’9’ then

--------------------------------------------

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;

--------------------------------------------

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 ):


with Global => null;       -- Not reference to global items
with Global => V;          -- V is an input of the subprogram
with Global => (X, Y, Z);  -- X, Y and Z are inputs of the 
subprogram

with Global => (Input  => V); -- V is an input of the subprogram.
with Global => (Input  => (X, Y, Z)); -- X, Y and Z are inputs of 
the
                                       -- subprogram
with Global => (Output => (A, B, C)); -- A, B and C are outputs 
of the
                                       -- subprogram
with Global => (In_Out => (D, E, F)); -- D, E and F are both 
inputs and
                                       -- outputs of the subprogram

with Global => (Proof_In => (G, H)); -- G and H are only used in 
assertion
                                      -- expressions within the 
subprogram

with Global => (Input    => (X, Y, Z),
                 Output   => (A, B, C),
                 In_Out   => (P, Q, R),
                 Proof_In => (T, U));
                 -- A global aspect with all types of global
                 -- specification

--------------------------------------------

To clarify information flow:


procedure P (X, Y, Z : in Integer; A, B, C : in out Integer; D, E 
out Integer)
   with Depends => ((A, B) =>+ (A, X, Y),
                    C      =>+ null,
                    D      =>  Z,
                    E      =>  null);
-- The "+" sign attached to the arrow indicates self-dependency
-- The exit value of A depends on the entry value of A as well as 
the entry
-- values of X and Y.
-- Similarly, the exit value of B depends on the entry value of B 
as well as
--  the entry values of A, X and Y.
-- The exit value of C depends only on the entry value of C.
-- The exit value of D depends on the entry value of Z.
-- The exit value of E does not depend on any input value.

--------------------------------------------

Bye,
bearophile
Feb 19 2014
next sibling parent "Meta" <jared771 gmail.com> writes:
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.
Feb 19 2014
prev sibling next sibling parent "bearophile" <bearophileHUGS lycos.com> writes:
Meta:

 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.

In Ada there is Dynamic_Predicate for the other cases :-)
 Does the loop break if the invariant fails, or does it stop the 
 program?

Ada has an elaborate infrastructure to allow you to choose how to react to failures, how to handle them, what failures to ignore, etc. At least, it stops the program.
 I don't think this is quite as important, seeing as D has the 
 pure keyword.

Purity means you can't use mutable values from outer scopes. The point of those Spark annotations (and outer()) is to do the opposite: to specify the flow of information in system programming when you are not using purity. Bye, bearophile
Feb 19 2014
prev sibling next sibling parent reply "Paulo Pinto" <pjmlp progtools.org> writes:
On Wednesday, 19 February 2014 at 23:55:16 UTC, bearophile wrote:
 Related to the Mars lander software thread.

 They have released the slides for the FOSDEM 2014 (1 February 
 2014) conference about Ada and related things 
 (http://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/1
/140201-fosdem.html 
 ).

 ...

I have been following Ada at FOSDEM for the last years, and its use seems to be increasing in Europe for safety critical systems, mainly thanks to C and C++ issues. Maybe this is an area where D could be pushed as well. -- Paulo
Feb 20 2014
parent Paulo Pinto <pjmlp progtools.org> writes:
Am 21.02.2014 16:57, schrieb Thiez:
 On Friday, 21 February 2014 at 14:27:48 UTC, Paulo Pinto wrote:
 On Friday, 21 February 2014 at 13:08:37 UTC, Francesco Cattoglio wrote:
 On Friday, 21 February 2014 at 12:56:32 UTC, Paulo Pinto wrote:
 That is easy to answer, I doubt they could with their rule of not
 having more than 5 characters per keyword. :)

ahahahha... are they stuck to the 70's? :D

Yes really, http://forum.dlang.org/post/glnafbocwjodiwrqwmbv forum.dlang.org I just cannot find the Reddit thread any longer.

That is not true, Rust has several keywords that are more than 5 characters, such as 'continue'. The full list is here: http://static.rust-lang.org/doc/master/rust.html#keywords . It is true that they prefer short keywords over long ones. It used to be the case that 'loop' could mean 'continue' but people found it confusing so it was fixed.

What I was arguing in that old thread was things like pub vs public, mut vs mutable and so on. I have a strong ML background as my university teachers were quite found of ML and we had a few courses using Caml Light. So I do like Rust and my issue back then was why to short those keywords and similar. Then again as I come from Pascal family of languages and always liked a bit verbosity, instead of the write only way of C. -- Paulo
Feb 21 2014
prev sibling next sibling parent "renoX" <renozyx gmail.com> writes:
On Thursday, 20 February 2014 at 08:03:47 UTC, Paulo Pinto wrote:
[cut]
 I have been following Ada at FOSDEM for the last years, and its 
 use seems to be increasing in Europe for safety critical 
 systems, mainly thanks to C and C++ issues.

 Maybe this is an area where D could be pushed as well.

I don't think so: given that D is "C++ done right", it would require many (unlikely to happen) changes to become an interesting alternative for Ada: for example changing the semantic of integers! That said, one question I should ask to Rust devs is why they didn't base Rust on Ada given their goals.. renoX
Feb 21 2014
prev sibling next sibling parent "Paulo Pinto" <pjmlp progtools.org> writes:
On Friday, 21 February 2014 at 10:01:41 UTC, renoX wrote:
 On Thursday, 20 February 2014 at 08:03:47 UTC, Paulo Pinto 
 wrote:
 [cut]
 I have been following Ada at FOSDEM for the last years, and 
 its use seems to be increasing in Europe for safety critical 
 systems, mainly thanks to C and C++ issues.

 Maybe this is an area where D could be pushed as well.

I don't think so: given that D is "C++ done right", it would require many (unlikely to happen) changes to become an interesting alternative for Ada: for example changing the semantic of integers! That said, one question I should ask to Rust devs is why they didn't base Rust on Ada given their goals.. renoX

That is easy to answer, I doubt they could with their rule of not having more than 5 characters per keyword. :) -- Paulo
Feb 21 2014
prev sibling next sibling parent "Francesco Cattoglio" <francesco.cattoglio gmail.com> writes:
On Friday, 21 February 2014 at 12:56:32 UTC, Paulo Pinto wrote:
 That is easy to answer, I doubt they could with their rule of 
 not having more than 5 characters per keyword. :)

ahahahha... are they stuck to the 70's? :D
Feb 21 2014
prev sibling next sibling parent "Paulo Pinto" <pjmlp progtools.org> writes:
On Friday, 21 February 2014 at 13:08:37 UTC, Francesco Cattoglio 
wrote:
 On Friday, 21 February 2014 at 12:56:32 UTC, Paulo Pinto wrote:
 That is easy to answer, I doubt they could with their rule of 
 not having more than 5 characters per keyword. :)

ahahahha... are they stuck to the 70's? :D

Yes really, http://forum.dlang.org/post/glnafbocwjodiwrqwmbv forum.dlang.org I just cannot find the Reddit thread any longer.
Feb 21 2014
prev sibling next sibling parent "Brian Rogoff" <brogoff gmail.com> writes:
On Friday, 21 February 2014 at 14:27:48 UTC, Paulo Pinto wrote:
 On Friday, 21 February 2014 at 13:08:37 UTC, Francesco 
 Cattoglio wrote:
 On Friday, 21 February 2014 at 12:56:32 UTC, Paulo Pinto wrote:
 That is easy to answer, I doubt they could with their rule of 
 not having more than 5 characters per keyword. :)

ahahahha... are they stuck to the 70's? :D

Yes really, http://forum.dlang.org/post/glnafbocwjodiwrqwmbv forum.dlang.org I just cannot find the Reddit thread any longer.

Obviously, there is no rule in Rust that keywords have no more than 5 letters (return, extern, ...) but the designers favor short keywords, maybe a bit much for my taste. OTOH, I prefer their preference for favoring immutability and expression oriented style to D's statement oriented preference. The latest version of Ada tries to fix Ada a bit in this regard http://www.ada-auth.org/standards/12rat/html/Rat12-1-3-2.html but it's a bit late. I'm glad to hear that Ada use is increasing somewhere, but I don't see it in any market I look at. The Rust designers are targetting C and C++ users, with a different vision than Walter and Andrei's as to what constitutes "C++ done right", and some specific applications, like Servo. -- Brian
Feb 21 2014
prev sibling next sibling parent "Thiez" <thiezz gmail.com> writes:
On Friday, 21 February 2014 at 14:27:48 UTC, Paulo Pinto wrote:
 On Friday, 21 February 2014 at 13:08:37 UTC, Francesco 
 Cattoglio wrote:
 On Friday, 21 February 2014 at 12:56:32 UTC, Paulo Pinto wrote:
 That is easy to answer, I doubt they could with their rule of 
 not having more than 5 characters per keyword. :)

ahahahha... are they stuck to the 70's? :D

Yes really, http://forum.dlang.org/post/glnafbocwjodiwrqwmbv forum.dlang.org I just cannot find the Reddit thread any longer.

That is not true, Rust has several keywords that are more than 5 characters, such as 'continue'. The full list is here: http://static.rust-lang.org/doc/master/rust.html#keywords . It is true that they prefer short keywords over long ones. It used to be the case that 'loop' could mean 'continue' but people found it confusing so it was fixed.
Feb 21 2014
prev sibling next sibling parent "Francesco Cattoglio" <francesco.cattoglio gmail.com> writes:
On Friday, 21 February 2014 at 15:57:32 UTC, Thiez wrote:
 That is not true, Rust has several keywords that are more than 
 5 characters, such as 'continue'. The full list is here: 
 http://static.rust-lang.org/doc/master/rust.html#keywords . It 
 is true that they prefer short keywords over long ones.

keywords short" sounds really stupid to me. No offence to designers, but I really don't think we should save some spar characters in 2014... I do all my coding on a remote SSH, but still I have plenty of screen space to spare ;) My first glance: "priv" instead of "private"... bleah! At least it's clear enough "mut"... what is this? "mutable", "mutex", perhaps "mute"? "impl" could be several different things, too, but I guess it's "implements" And "continue" being a different keyword some time ago. In the end they changed it. Tons of discussions and stuff; was it worth saving 3 characters, after all? I hope their standard library is at least WAY more verbose... Otherwise I pity casual Rust programmers :D
Feb 21 2014
prev sibling next sibling parent "Tobias Pankrath" <tobias pankrath.net> writes:
On Friday, 21 February 2014 at 17:25:48 UTC, Francesco Cattoglio 
wrote:
 On Friday, 21 February 2014 at 15:57:32 UTC, Thiez wrote:
 That is not true, Rust has several keywords that are more than 
 5 characters, such as 'continue'. The full list is here: 
 http://static.rust-lang.org/doc/master/rust.html#keywords . It 
 is true that they prefer short keywords over long ones.

keywords short" sounds really stupid to me. No offence to designers, but I really don't think we should save some spar characters in 2014... I do all my coding on a remote SSH, but still I have plenty of screen space to spare ;) My first glance: "priv" instead of "private"... bleah! At least it's clear enough "mut"... what is this? "mutable", "mutex", perhaps "mute"? "impl" could be several different things, too, but I guess it's "implements" And "continue" being a different keyword some time ago. In the end they changed it. Tons of discussions and stuff; was it worth saving 3 characters, after all? I hope their standard library is at least WAY more verbose... Otherwise I pity casual Rust programmers :D

Depends on how often and where you write those keywords. mut seems to be quite common and even in D I would not like 'reference' more than 'ref', especially since it is used in parameter lists.
Feb 21 2014
prev sibling next sibling parent Matej Nanut <matejnanut gmail.com> writes:
--f46d043c814c818aff04f2f02c70
Content-Type: text/plain; charset=UTF-8

On 21 February 2014 20:00, Tobias Pankrath <tobias pankrath.net> wrote:

 Depends on how often and where you write those keywords. mut seems to be
 quite common and even in D I would not like 'reference' more than 'ref',
 especially since it is used in parameter lists.

I think Rust's "pub", "priv" and "fn" are just silly. But I don't mind "mut". However it might've been nicer if you didn't have to write "let mut" but just "mut". What made Rust a no-go for me was when I tried to write a generic sort. I still can't figure out how to swap two elements in an array ("vector"). The implementation in their std lib for "swap" has an unsafe block... (And I don't want a GC or RC requirement for the array.) --f46d043c814c818aff04f2f02c70 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable <div dir=3D"ltr"><div class=3D"gmail_extra"><div class=3D"gmail_quote">On 2= 1 February 2014 20:00, Tobias Pankrath <span dir=3D"ltr">&lt;<a href=3D"mai= lto:tobias pankrath.net" target=3D"_blank">tobias pankrath.net</a>&gt;</spa= n> wrote:<br> <blockquote class=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:1p= x #ccc solid;padding-left:1ex"><div class=3D"HOEnZb"><div class=3D"h5"><br>= </div></div> Depends on how often and where you write those keywords. mut seems to be qu= ite common and even in D I would not like &#39;reference&#39; more than &#3= 9;ref&#39;, especially since it is used in parameter lists.<br> </blockquote></div><br></div><div class=3D"gmail_extra">I think Rust&#39;s = &quot;pub&quot;, &quot;priv&quot; and &quot;fn&quot; are just silly. But I = don&#39;t mind &quot;mut&quot;. However it might&#39;ve been nicer if you d= idn&#39;t have to write &quot;let mut&quot; but just &quot;mut&quot;.<br> <br></div><div class=3D"gmail_extra">What made Rust a no-go for me was when= I tried to write a generic sort. I still can&#39;t figure out how to swap = two elements in an array (&quot;vector&quot;). The implementation in their = std lib for &quot;swap&quot; has an unsafe block... (And I don&#39;t want a= GC or RC requirement for the array.)<br> </div></div> --f46d043c814c818aff04f2f02c70--
Feb 21 2014
prev sibling parent Ziad Hatahet <hatahet gmail.com> writes:
--001a11c3fbbae6bd7f04f303e299
Content-Type: text/plain; charset=ISO-8859-1

On Fri, Feb 21, 2014 at 12:06 PM, Matej Nanut <matejnanut gmail.com> wrote:

  However it might've been nicer if you didn't have to write "let mut" but
 just "mut".

rejected. Consider: `let (x, mut y) = (1, 2);` which would otherwise have not been possible. --001a11c3fbbae6bd7f04f303e299 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable <div dir=3D"ltr"><div class=3D"gmail_extra"><br><div class=3D"gmail_quote">= On Fri, Feb 21, 2014 at 12:06 PM, Matej Nanut <span dir=3D"ltr">&lt;<a href= =3D"mailto:matejnanut gmail.com" target=3D"_blank">matejnanut gmail.com</a>= &gt;</span> wrote:<br> <blockquote class=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:1p= x #ccc solid;padding-left:1ex"><div dir=3D"ltr"><div><div class=3D"gmail_ex= tra"><div class=3D"gmail_quote">=A0However it might&#39;ve been nicer if yo= u didn&#39;t have to write &quot;let mut&quot; but just &quot;mut&quot;.<br=

</div></div></div><div class=3D"gmail_extra"><br></div></div></blockquote><= div><br></div><div>Something similar had been discussed if I recall correct= ly, and was rejected. Consider: `let (x, mut y) =3D (1, 2);` which would ot= herwise have not been possible.=A0</div> </div></div></div> --001a11c3fbbae6bd7f04f303e299--
Feb 22 2014