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=0.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,b78c363353551702
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.241.162 with SMTP id wj2mr5393189pbc.2.1340642603765;
        Mon, 25 Jun 2012 09:43:23 -0700 (PDT)
Path: 
 l9ni18816pbj.0!nntp.google.com!news1.google.com!goblin2!goblin.stu.neva.ru!news.internetdienste.de!noris.net!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Mon, 25 Jun 2012 18:43:02 +0200
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7;
 rv:13.0) Gecko/20120614 Thunderbird/13.0.1
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: about the new Ada 2012 pre/post conditions
References: <jrsjr7$uuo$1@speranza.aioe.org>
 <1hgo6aks03zy.by4pq4xbjsgf$.dlg@40tude.net> <jrsmfh$6fq$1@speranza.aioe.org>
 <npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net> <js00co$clj$1@munin.nbi.dk>
 <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net> <js2hq5$9fj$1@munin.nbi.dk>
 <1oih2rok18dmt.avbwrres5k12.dlg@40tude.net>
 <4fe59ea0$0$9502$9b4e6d93@newsspool1.arcor-online.net>
 <1mkp7fzlk1b0y.1ueinfjn48fcy$.dlg@40tude.net>
 <4fe72b6b$0$9504$9b4e6d93@newsspool1.arcor-online.net>
 <1bbvp3ghpjb5s.1go1s1qvcmagh$.dlg@40tude.net>
 <4fe76fad$0$9507$9b4e6d93@newsspool1.arcor-online.net>
 <1jt8vhzxfrv2i.eohce4d3rwx1$.dlg@40tude.net>
 <4fe83aaa$0$6624$9b4e6d93@newsspool2.arcor-online.net>
 <1pkfv0tiod3rn$.onx6dmaa3if9$.dlg@40tude.net>
 <4fe85beb$0$6638$9b4e6d93@newsspool2.arcor-online.net>
 <21wn0ooltm4q.fvk0lmtoro3f$.dlg@40tude.net>
In-Reply-To: <21wn0ooltm4q.fvk0lmtoro3f$.dlg@40tude.net>
Message-ID: <4fe89517$0$6630$9b4e6d93@newsspool2.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 25 Jun 2012 18:43:03 CEST
NNTP-Posting-Host: 3283ff76.newsspool2.arcor-online.net
X-Trace: 
 DXC=:Q::dT_M8Bij5k5aEF7ISmA9EHlD;3Ycb4Fo<]lROoRa8kF<OcfhCOk0>j8fVEViWnnc\616M64>jLh>_cHTX3jmhhoJ5l4bPFl
X-Complaints-To: usenet-abuse@arcor.de
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Date: 2012-06-25T18:43:03+02:00
List-Id: <comp.lang.ada>

On 25.06.12 15:19, Dmitry A. Kazakov wrote:
> All three used axiomatic approach. None of them would ever seek
> to justify logic by means of logic.

My choice of "justify" was bad. I'll leave it at Stefan Lucks' replies,
only noting that what mathematicians did when working in math mode
is different from what they did when seeking the ultimate foundation
of how what they did might be really true, a certainty.

>>  new Data'(Size => More_than_4k);
> 
> How does this make SPARK null and void?

It's void for Ada. It's really good for some programs.

The point is that with Ada 2012 assertions, now there is something.

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

"Ergo" is an indication of accepting the frames of reference
for #1 and #2, and the connotation of a notional divide.

Assertions are (1) a tool for best effort and (2) need not
even relate to what some body does. They should, of course.
That's in the hands of the programmers, though. Malicious
programmers can write Pre => F (X) and then, in bodies, write
something that corresponds to not F (X). (Note: corresponds to.
That could be "not F(X)".)


>>>> 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.

Again, bad choice of words.
There hardly is a situation qualified by complete formal knowledge
of a program. Stopping all programming that leads to such situations
is not acceptable. Improving the situation via DbC is, if only as
an educational effort in combination with good will.


>> 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 remember having said "transcend", also "insufficient", and "goal".
"Transcend" is different from "not obeying", in particular when
the subject of "transcend" is the human activity called "design",
not some ready made "program". "Transcend" may be a pompous euphemism,
or not.