Re: Generic-Package Elaboration Question / Possible GNAT Bug.

[stefan-lucks@see-the.signature]

On Wed, 23 Nov 2011, Dmitry A. Kazakov wrote:

> That is exactly why contracts cannot be dynamic. Dynamic means statically
> undecidable. 

That point seems to be the main issue that makes this discussion going on 
and on ...

Dynamic means it has not been statically decided by an apprpriate tool 
(such as SPARK). 

Good contracts are statically decidable! I guess, few c.l.a. people will 
disagree and claim that good contracts are statically undecidable.

Now, if we have the tools to statically verify these contracts, then we 
are done. There is SPARK, but that very severely constrains Ada to be able 
to find proofs. Perhaps, within some time, there will be tools to 
statically verify some Ada 2012 contracts (google for HiLite Ada). 

In the meantime, Ada 2012 contracts are just claims made by the programmer 
(perhaps formally verified by hand or so). At this stage, what can you do?

  a) Documentation only -- the existence of the contract has no influence 
     on the compiled code. 
  
  b) Support for testing -- check the conditions during testing time, but 
     turn to (a) after testing has been done. (*)

  c) Organized panic -- write the event into a log file; if neccessary, 
     try to minimize the damage (e.g., write important data that has 
     recently been changed into a temporary file); shut down.

Ada 2012 supports all thee strategies (by using compiler switches), 
depending on the programmers' (or project mangagers') views and 
requirements. What should be wrong with this choice?

And sure, Ada 2012 seems to allow you to write really lousy contracts, 
less than useful, with side-effects and whatever. To some degree, with pre 
=> ..., post => ... is a bit like UNCHECKED_Something: useful when used 
with care, but dangerous.

---------
(*) This is what someone denoted as "debugging" support. I think, testing 
is the better notion here. 

-- 
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany  ----
    <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------