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
Received: by 10.68.238.198 with SMTP id vm6mr4729177pbc.3.1328272271293;
        Fri, 03 Feb 2012 04:31:11 -0800 (PST)
Path: 
 lh20ni255772pbb.0!nntp.google.com!news2.google.com!postnews.google.com!e27g2000vbu.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: Fri, 3 Feb 2012 04:25:17 -0800 (PST)
Organization: http://groups.google.com
Message-ID: 
 <27200179-2b18-4d7c-ae8d-bbfff32070d4@e27g2000vbu.googlegroups.com>
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>
NNTP-Posting-Host: 88.97.49.112
Mime-Version: 1.0
X-Trace: posting.google.com 1328272271 16958 127.0.0.1 (3 Feb 2012 12:31:11
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 3 Feb 2012 12:31:11 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: e27g2000vbu.googlegroups.com; posting-host=88.97.49.112;
 posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-Google-Web-Client: true
X-Google-Header-Order: ARLUEHNKC
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
 Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
 3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe)
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Date: 2012-02-03T04:25:17-08:00
List-Id: <comp.lang.ada>

On Feb 3, 3:13=A0am, "Randy Brukardt" <ra...@rrsoftware.com> wrote:

> .... Something like SPARC, that requires an
> all-or-nothing approach, very often ends up with nothing.

I think this misrepresents the range of options available with SPARK.
Proofs can be anywhere in the range from fully formal from first
principles, through less formal proofs with user supplied rules (which
can themselves be supported by more or less formal justifications) to
the fully informal (proof by review).

I have always adopted "as formal as is reasonably practicable" and it
hasn't failed me yet.

> 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 nice to have some examples of what you have in mind here.

Cheers,

Phil