SPARK
in [ADA]
|
From: Phil Thornley on 14 May 2010 04:11 On 14 May, 04:07, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > The Quick Reference Card #1 talks about type assertion: > > > A type assertion allows the user to specify the base type which the > > compiler will associate with a signed integer type. The base type > > must be supplied to the Examiner in the configuration file. This > > assertion allows the Examiner to generate VCs which are much more > > readily discharged [RTC 5.2]. > > > Example: > > type T is range 1 .. 10 > > --# assert TBase is Short_Short_Integer; > > As the Examiner ignore any representation clauses [SPARK 95 (13.1)], it > cannot care to any implicit representation clause either. So what's the > purpose of this kind of assertions ? Does the examiner check something > else which is not only the range ? Does it have something to deal with > type conversions ? > > -- > pragma Asset ? Is that true ? Waaww... great Yannick, These base type assertions are used to get the ranges for overflow checks - see Section 5 of Generation of RTCs for SPARK Programs (GenRTCs). The Examiner can't validate this assertion, so it's up to the user to get it right (but you might be able to use compiler assertions to check it). It is safe to assert a smaller base type than the compiler actually chooses, so the portability problem can be reduced by specifying the smallest possible base type. Cheers, Phil
From: Phil Thornley on 14 May 2010 04:17 On 14 May, 05:15, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > > Is this file part of the language definition or did I missed some > > relevant documentation elsewhere ? > > Found : it is detailed in the file Examiner_GenVCs.pdf (Generation of VCs > for SPARK Programs) Yannick, As you are discovering, the documentation for the optional proof assertions in SPARK is not easy to find (it is spread across several documents, and rather scattered within those documents). You might find it helps to look at the tutorials on www.sparksure.com (one set for the proof annotations and one set for the Proof Checker). Cheers, Phil
From: Rod Chapman on 14 May 2010 05:32 > As you are discovering, the documentation for the optional proof > assertions in SPARK is not easy to find (it is spread across several > documents, and rather scattered within those documents). Noted. For SPARK Pro 9.0, we merged all the Proof material into one manual and gave it the rather more obvious title "Proof Manual". We also produced a one-page clickable index to _all_ the manuals, which has also proven useful. - Rod Chapman, SPARK Team
From: Yannick Duchêne (Hibou57) on 14 May 2010 10:20 Le Fri, 14 May 2010 10:17:50 +0200, Phil Thornley <phil.jpthornley(a)googlemail.com> a écrit: > As you are discovering, the documentation for the optional proof > assertions in SPARK is not easy to find (it is spread across several > documents, and rather scattered within those documents). I wouldn't say so much. There was actually in the QR #1, a little â[VCG 3]: ...â and at the bottom of the card, something like â[VCG] Generation of VCs for SPARK Programsâ, so cross references are there ; this was just that I missed one file (I finally moved all release notes documents elsewhere to make the docs directory more handy). > You might find it helps to look at the tutorials on www.sparksure.com > (one set for the proof annotations and one set for the Proof Checker). Seems good material :) The link goes to my bookmarks (will tell about it at fr.comp.lang.ada also). -- There is even better than a pragma Assert: an --# assert
From: Yannick Duchêne (Hibou57) on 14 May 2010 10:28
Le Fri, 14 May 2010 10:11:29 +0200, Phil Thornley <phil.jpthornley(a)googlemail.com> a écrit: > It is safe to assert a smaller base type than the compiler > actually chooses, so the portability problem can be reduced by > specifying the smallest possible base type. Oh, yes, I see. Thanks Phil -- There is even better than a pragma Assert: an --# assert |