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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM 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.227.40 with SMTP id rx8mr7033765pbc.5.1328356984239;
        Sat, 04 Feb 2012 04:03:04 -0800 (PST)
Path: 
 lh20ni259377pbb.0!nntp.google.com!news2.google.com!goblin1!goblin.stu.neva.ru!txtfeed2.tudelft.nl!tudelft.nl!txtfeed1.tudelft.nl!dedekind.zen.co.uk!zen.net.uk!hamilton.zen.co.uk!shaftesbury.zen.co.uk.POSTED!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 12:02:51 -0000
Message-ID: <MPG.29972ec7befb6ae9989682@news.zen.co.uk>
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>
MIME-Version: 1.0
User-Agent: MicroPlanet-Gravity/3.0.4
Organization: Zen Internet
NNTP-Posting-Host: 490d8ad8.news.zen.co.uk
X-Trace: 
 DXC=PA79coWiiVoG<aQSeV28Klnok4Z\<mH4ihDU:2=XKPkhlmPCCL>j[if=CLe5aAFkieF?aAPVjj<Yh
X-Complaints-To: abuse@zen.co.uk
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Date: 2012-02-04T12:02:51+00:00
List-Id: <comp.lang.ada>

[Third attempt to reply, so I apologise for any duplicates, but posts 
via Google Groups aren't emerging.]

In article <jgfjc4$u4b$1@munin.nbi.dk>, randy@rrsoftware.com says...
> ... Something like SPARC, that requires an 
> 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 user rules (which can have justifications with a range of 
formalities) to completely informal proof, 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 
> attention on the wrong things. There is a lot that can be proved about 
> dynamic constructs in Ada (far more than in other most languages), and it is 
> unfortunate that instead of taking advantage of this (and making widely 
> usable results), most of effort has been on proving the Fortran 66 subset of 
> Ada. (I do see signs that this is changing, finally, but I think a lot of 
> 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