digitalmars.D - More on Ada2012 and its contracts
- "bearophile" <bearophileHUGS lycos.com> Apr 10 2013
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.
Apr 10 2013