Re: Weird error with Dynamic_Predicate

[Martin <martin@thedowies.com>]

On Tuesday, May 13, 2014 1:46:39 PM UTC+1, G.B. wrote:
> On 12.05.14 21:47, mockturtle wrote:
> 
> > Any ideas?
> 
> 
> 
>  From a different angle, a rule of contract-based design---
> 
> assuming the lessons learned from DbC---is not a substitute
> 
> for input checking. While I guess you have your reasons for
> 
> attaching the Dynamic_Predicate to a string type, if you
> 
> are preforming proofs, which DbC would oblige you to do,
> 
> there is a different strategy:
> 
> 
> 
> By the above rule (about DbC not being input checking),
> 
> some I/O routine would check the syntax;
> 
> then, if the characters form a well formed string, the object
> 
> can be converted to a different string type; this string
> 
> type does not have the dynamic check attached, since after
> 
> the checking routine is done, the type's objects are known
> 
> to have only good values.



Right, it should be the 'constructor' that ensures the class invariant - the validity of the 'raw string' or raises an exception otherwise.

So you always want to force the user to use a proved 'constructor' function and no other, e.g.

package Valid_Strings is
   type Valid_String (<>) is tagged private;
   Invalid_String : exception;
   function Create (S : String) return Valid_String; -- or Invalid_String
private
   type Valid_String is tagged record
      ...
   end record;
   ...
end Valid_Strings;


-- Martin