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.7 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM,REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no
	version=3.4.4
X-Google-Thread: 103376,ad06d2d7cb045687
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.213.68 with SMTP id nq4mr6871584pbc.2.1328349560363;
        Sat, 04 Feb 2012 01:59:20 -0800 (PST)
Path: 
 lh20ni259067pbb.0!nntp.google.com!news1.google.com!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: Silly and stupid post-condition or not ?
Date: Sat, 4 Feb 2012 01:30:30 -0800 (PST)
Organization: http://groups.google.com
Message-ID: 
 <22467765.2471.1328347830161.JavaMail.geo-discussion-forums@yqgc19>
References: <op.v8w6ptk5ule2fv@douda-yannick>
 <82wr86fzos.fsf@stephe-leake.org>
 <5af407fc-2868-44ca-84d2-c51a2a64104d@o4g2000pbc.googlegroups.com>
 <82k445fu9n.fsf@stephe-leake.org> <jgfjc4$u4b$1@munin.nbi.dk>
Reply-To: comp.lang.ada@googlegroups.com
NNTP-Posting-Host: 88.97.49.112
Mime-Version: 1.0
X-Trace: posting.google.com 1328349560 26415 127.0.0.1 (4 Feb 2012 09:59:20
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Sat, 4 Feb 2012 09:59:20 +0000 (UTC)
In-Reply-To: <jgfjc4$u4b$1@munin.nbi.dk>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=88.97.49.112;
 posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-Google-Web-Client: true
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Date: 2012-02-04T01:30:30-08:00
List-Id: <comp.lang.ada>

[Second attempt to post, my apologies if this is a duplicate but I haven't =
seen the first post appear anywhere after 24 hours.]
On Friday, 3 February 2012 03:13:04 UTC, Randy Brukardt  wrote:
> .... Something like SPARC, that requires an=20
> all-or-nothing approach, very often ends up with nothing.

This misrepresents the options available with the proof features of SPARK, =
which range from full formal proof, through lower formality proofs using us=
er rules (which can have justifications with a range of formalities) to com=
pletely informal, using review proofs.

My experience is that using "as formal as practically possible" has always =
worked well.

> I think that things like SPARC can actually be harmful, as they focus=20
> attention on the wrong things. There is a lot that can be proved about=20
> dynamic constructs in Ada (far more than in other most languages), and it=
 is=20
> unfortunate that instead of taking advantage of this (and making widely=
=20
> usable results), most of effort has been on proving the Fortran 66 subset=
 of=20
> Ada. (I do see signs that this is changing, finally, but I think a lot of=
=20
> the work should have been done years ago.)

It would be interesting to have some examples of what you have in mind here=
.

Cheers,

Phil=20