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.193.129 with SMTP id ho1mr23269131pbc.8.1340211801566;
        Wed, 20 Jun 2012 10:03:21 -0700 (PDT)
Path: 
 l9ni73028pbj.0!nntp.google.com!news2.google.com!goblin3!goblin2!goblin.stu.neva.ru!news.teledata-fn.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Wed, 20 Jun 2012 19:02:37 +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>
In-Reply-To: <npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net>
Message-ID: <4fe2022d$0$9517$9b4e6d93@newsspool1.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 20 Jun 2012 19:02:38 CEST
NNTP-Posting-Host: 1612c006.newsspool1.arcor-online.net
X-Trace: 
 DXC=V5:@Na?5R7\1`E>oC;JXEZic==]BZ:af^4Fo<]lROoRQnkgeX?EC@@PFMP^6DDEk_Wnc\616M64>ZLh>_cHTX3j]@@jRJ?l:]LZ
X-Complaints-To: usenet-abuse@arcor.de
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Date: 2012-06-20T19:02:38+02:00
List-Id: <comp.lang.ada>

On 20.06.12 16:37, Dmitry A. Kazakov wrote:

> Correctness to be checked statically or dynamically by an *independent*
> program.

Yes, the independent program that checks the assertions is us,
fixing bugs (a.k.a. correcting partial proofs).

The human aspect of pre/post checking is why some assertions
need not be expressible in Ada (and we are free to substitute
True).
Nevertheless, if conditions/assumptions/assertions are
formally expressible, Ada 2012 lets us ask the compiler for
practical help. The programs can perform a few tests automatically,
so that we can fix faulty programs, or faulty assertions, or
faulty brains.