Re: about the new Ada 2012 pre/post conditions

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Mon, 25 Jun 2012 14:39:06 +0200, Georg Bauhaus wrote:

> On 25.06.12 13:54, Dmitry A. Kazakov wrote:
> 
>>> Indeed, it helps to remember that logicians and mathematicians
>>> have learned that logic and mathematics cannot justify themselves.
>> 
>> No, they never ever did that.
> 
> They tried, though. I didn't even say that they did.
> 
> Frege thought, for some time, that he had done.
> Russel sent a correction. Hilbert did not give up, though:

Not at all. All three used axiomatic approach. None of them would ever seek
to justify logic by means of logic.

>>> We have to do something. DbC is something. Better than nothing.
>> 
>> Is SPARK nothing?
> 
> Try
> 
>  new Data'(Size => More_than_4k);

How does this make SPARK null and void?

>> Is strong typing nothing?
> 
> Until Ada 2012, there was nothing in addition to the strong type
> system of Ada 2005.

And the point is? Some hidden Ada version between 2005 and 2012?

>> But you seemingly did not read what I wrote earlier. There is either #1 or
>> #2.
> 
> I have tried to explain that neither #1 nor #2 are applicable
> because they assume applicability of exhaustive formal analysis
> to general program design (not programs).

So #2 does not apply, I missed where you agreed with me on that.

Ergo, Ada 2012 preconditions are not contract (not #2). 

Please confirm this, and we will proceed to #1 and whether (not #2 is
equivalent to #1). 

>>> DbC is a best effort thing like every system building effort.
>> 
>> How are you going to prove this, if "DbC" contradicts logic itself?
> 
> A program that is known to be covered entirely by logic
> is really an exception.

Please, show this without logic.
 
> Proving things in a DbC framework is similar to proving things
> with the help of more than Ada, as is done when using SPARK.

No. You claimed that what you call DbC does not obey laws of logic. I am
eager to learn how are you going to "prove things" without these laws.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de