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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,6d79efdb8dde2c5a
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news1.google.com!news3.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!193.201.147.68.MISMATCH!feeder.news-service.com!newsfeed.straub-nv.de!eternal-september.org!feeder.eternal-september.org!.POSTED!not-for-mail
From: "J-P. Rosen" <rosen@adalog.fr>
Newsgroups: comp.lang.ada
Subject: Re: Categories for SPARK on Rosetta Code (Was: SPARK : third example
 for Roesetta - reviewers welcome)
Date: Fri, 20 Aug 2010 18:23:32 +0200
Organization: Adalog
Message-ID: <i4ma6e$gm7$1@news.eternal-september.org>
References: <op.vhguffh3ule2fv@garhos> <op.vhjindufxmjfy8@garhos>
 <4c69a251$0$2371$4d3efbfe@news.sover.net> <op.vhjyi5kkxmjfy8@garhos>
 <4c69cd5f$0$2375$4d3efbfe@news.sover.net>
 <e614687a-58ce-499f-a6af-a5893cbdc812@q22g2000yqm.googlegroups.com>
 <1ddee5a6-fc25-4d23-bebd-3364923d0aa5@z10g2000yqb.googlegroups.com>
 <aihbzmy85j4v.163hyfnglvwus.dlg@40tude.net>
 <7cf71c68-4faf-4a7b-a350-405ff7f12ff9@z10g2000yqb.googlegroups.com>
 <4xb6sjkpzo1r$.138841gile5s0$.dlg@40tude.net>
 <87wrrnjf9f.fsf_-_@hugsarin.sparre-andersen.dk>
 <3ed38f7f-372d-422e-9bda-eca8a73d3f0d@x21g2000yqa.googlegroups.com>
 <i4lh4b$gqc$1@news.eternal-september.org>
 <1ncf62lqqj7ab$.1czxyaw96dl17.dlg@40tude.net>
 <i4ljfe$odg$1@news.eternal-september.org>
 <1y0wcz3etd5au.1kgyc5ls0w5kk$.dlg@40tude.net>
 <i4lpco$d44$1@news.eternal-september.org>
 <gcggor638e9z$.avh74wi399su.dlg@40tude.net>
 <i4lvul$5sg$1@news.eternal-september.org>
 <vge6jatqhyxk.1h20juk1ye41$.dlg@40tude.net>
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 20 Aug 2010 16:23:42 +0000 (UTC)
Injection-Info: mx03.eternal-september.org;
 posting-host="Dn22F68J9CHYFQQlT81DGA";
	logging-data="17095"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18MvBiCeKPk2Cm7ua1VgoII"
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; fr;
 rv:1.9.2.8) Gecko/20100802 Thunderbird/3.1.2
In-Reply-To: <vge6jatqhyxk.1h20juk1ye41$.dlg@40tude.net>
Cancel-Lock: sha1:2riLQsVxeO8kiya1OizKHWJ0vtc=
Xref: g2news1.google.com comp.lang.ada:13541
Date: 2010-08-20T18:23:32+02:00
List-Id: <comp.lang.ada>

Le 20/08/2010 16:05, Dmitry A. Kazakov a �crit :
> I thought about a specific approach to programming, as it was proposed by
> Dijkstra, with designing both the program and a proof that certain
> properties of the program hold. SPARK's annotations support this approach.
> This is not specific to SPARK.
> 
Good - and I still think that Eiffel could claim that to a certain
extent, and also Ada with Pre/Post condition.

Now, do you have a name for it?

-- 
---------------------------------------------------------
           J-P. Rosen (rosen@adalog.fr)
Visit Adalog's web site at http://www.adalog.fr