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/14/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
