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=unavailable autolearn_force=no version=3.4.4
Path: 
 buffer2.nntp.dca1.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Mon, 27 Jul 2015 16:59:13 -0500
Newsgroups: comp.lang.ada
Date: Mon, 27 Jul 2015 17:59:12 -0400
From: Peter Chapin <PChapin@vtc.vsc.edu>
X-X-Sender: pcc09070@WIL414CHAPIN.vtc.vsc.edu
Subject: Re: Assertions in SPARK (Was: If not Ada, what else...)
In-Reply-To: <mp52ld$ves$1@dont-email.me>
Message-ID: <alpine.CYG.2.11.1507271757530.5816@WIL414CHAPIN.vtc.vsc.edu>
References: <iomd56$c1s$1@dont-email.me>
 <14592326-5070-4663-a864-5684298f3748@googlegroups.com>
 <004361da-53c4-4ea9-8cc6-38944aa6c7ad@googlegroups.com>
 <29dd5458-f9ce-4db8-9128-8ab35a9ce5f8@googlegroups.com>
 <64bc671c-72e5-4924-b703-3b907c69949c@googlegroups.com>
 <877fq9uj6g.fsf@theworld.com>
 <65061686-5c8f-433b-9b11-9e228298158e@googlegroups.com>
 <87k2u96jms.fsf@jester.gateway.sonic.net>
 <06f8a6f9-d219-4d40-b9ac-8518e93839bd@googlegroups.com>
 <87y4io63jy.fsf@jester.gateway.sonic.net>
 <7a29d3e9-d1bd-4f4a-b1a6-14d3e1a83a4d@googlegroups.com>
 <87mvz36fen.fsf@jester.gateway.sonic.net>
 <87vbd67yr1.fsf_-_@adaheads.sparre-andersen.dk> <mp52ld$ves$1@dont-email.me>
User-Agent: Alpine 2.11 (CYG 23 2013-08-11)
Organization: Vermont Technical College
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-HV2T1Fqlz1S2Zll/ldSKbSbwzmdVg11kOi7PW/K1Dely8MEx1z6ko8+vTyk0ickDKcMD2b6W7A1Ls8q!c1OqQSvFDlN8kYaRai831lUs7okU+mi6Kxg4HNRWPlIwhc7pMnGUff2lXSBTvHOD0fY51RIhwtOT!ZtGV+YViP/iG3EFCjQ==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint
 properly
X-Postfilter: 1.3.40
Xref: number.nntp.giganews.com comp.lang.ada:194358
Date: 2015-07-27T17:59:12-04:00
List-Id: <comp.lang.ada>

On Mon, 27 Jul 2015, G.B. wrote:

>>> I remember being disappointed that (unless I missed something) there 
>>> doesn't seem to be a way to put assertions in the middle of a function 
>>> body and have Spark check them statically.  Am I mistaken about that?
>> 
>> You are.  I don't have a SPARK book right here, but IIRC it is simply:
>>
>>     --# assert <expression>
>
> Also worth considering is
>
> --# check <expression>
>
> which is different from assert in that is doesn't change SPARK's mind 
> about where the interesting points in the paths are.

The SPARK2014 version of these constructions are pragma Assert (similar to 
the check annotation) and pragma Assert_And_Cut (similar to the assert 
annotation). They are checked statically by the SPARK proof tools.

Peter