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