• bearophile (11/104) Apr 10 2013 About the contract-based programming of Ada 2012 and related

"bearophile" <bearophileHUGS lycos.com> writes:

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