From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.43.78.135 with SMTP id zm7mr15864624icb.27.1400000675112;
        Tue, 13 May 2014 10:04:35 -0700 (PDT)
X-Received: by 10.140.80.5 with SMTP id b5mr40044qgd.20.1400000675074; Tue, 13
 May 2014 10:04:35 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.glorb.com!r10no3916416igi.0!news-out.google.com!gi6ni900igc.0!nntp.google.com!c1no5722056igq.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Tue, 13 May 2014 10:04:34 -0700 (PDT)
In-Reply-To: <5372142e$0$6603$9b4e6d93@newsspool4.arcor-online.net>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=82.43.197.131;
 posting-account=g4n69woAAACHKbpceNrvOhHWViIbdQ9G
NNTP-Posting-Host: 82.43.197.131
References: <e4d8e3db-99b6-49d4-85f3-839f178d4047@googlegroups.com>
 <5372142e$0$6603$9b4e6d93@newsspool4.arcor-online.net>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <e0aa07b0-e464-48de-b35e-ea26767da710@googlegroups.com>
Subject: Re: Weird error with Dynamic_Predicate
From: Martin <martin@thedowies.com>
Injection-Date: Tue, 13 May 2014 17:04:35 +0000
Content-Type: text/plain; charset=ISO-8859-1
Xref: news.eternal-september.org comp.lang.ada:19805
Date: 2014-05-13T10:04:34-07:00
List-Id: <comp.lang.ada>

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