About the contract-based programming of Ada 2012 and related
matters, by Robert Dewar, president of AdaCore:
http://www.drdobbs.com/article/print?articleId=240150569&siteSectionName=architecture-and-design
There are trumpets about contract programming:
But Ada 2012 does bring an "earth-shaking" advance
the--introduction of
contract-based programming, or what Eiffel programmers call
"design by
contract."
Compared to the usually long syntax of Ada, they are short and
nice enough:
Suppose that Dedupe needs to meet the following requirements:
On entry, the parameter Arr contains at least one
duplicated element.
On exit, all duplicates (and only the duplicates) have been
removed, nothing new
has been added, and the parameter Last shows the new upper
bound.
procedure Dedupe (Arr: in out Int_Array; Last : out
Natural) with
Pre => Has_Duplicates(Arr),
Post => not Has_Duplicates( Arr(Arr'First .. Last) )
and then (for all Item of Arr'Old =>
(for some J in Arr'First .. Last =>
Item = Arr(J)))
-- Only duplicates removed
and then (for all J in Arr'First .. Last =>
(for some Item of Arr'Old =>
Item = Arr(J)));
-- Nothing new added
where the helper function Has_Duplicates can be defined as
follows:
function Has_Duplicates(Arr : Int_Array) return Boolean is
begin
return (for some I in Arr'First .. Arr'Last-1 =>
(for some J in I+1 .. Arr'Last =>
Arr(I)=Arr(J)));
end Has_Duplicates;
The ranges on scalar types are very useful:
Besides preconditions and postconditions for subprograms, Ada
2012
supports several other kinds of contracts. One category
involves predicates
on types: conditions that must always be met by values of the
type. One of
the most important such predicates, ranges on scalar types, has
been part
of the language since Ada 83:
Test_Score : Integer range 0 through 100;
Distance : Float range -100.0 .. 100.0;
This time I have understood a bit better the difference between
Static_Predicate and Dynamic_Predicate:
Ada 2012's subtype predicates come in two forms,
Static_Predicate and
Dynamic_Predicate, employed depending on the nature of the
expression
that defines the predicate. For example:
type Month is
(Jan, Feb, Mar, Apr, May, Jun, Jul, Aug, Sep, Oct, Nov,
Dec);
subtype Long_Month is Month with
Static_Predicate => Long_Month in (Jan, Mar, May, Jul, Aug,
Oct, Dec);
subtype Short_Month is Month with
Static_Predicate => Short_Month in (Apr, Jun, Sep, Nov);
subtype Even is Integer with
Dynamic_Predicate => Even rem 2 = 0;
The predicate is checked on assignment, analogous to range
constraints:
L : Long_Month := Apr; -- Raises Constraint_Error
E : Even := Some_Func(X, Y); -- Check that result is even
The static forms allow more compile-time checking. For example,
in this
case statement:
case Month_Val is
when Long_Month => …
when Short_Month => …
end case;
the compiler will detect that Feb is absent. Dynamic predicates
cannot
be checked at compile time, but violations can still be
detected at
runtime. In general, predicates require runtime checks; when
you assign
a Month value to a Short_Month variable, a runtime check
verifies that
it has an appropriate value.
Bye,
bearophile
