[GAP] Ada 2012 in Gnat 2011 ?

[Andy Edmunds]

On 06/06/2011 13:27, Robert Dewar wrote:
> On 6/6/2011 8:10 AM, Cyrille Comar wrote:
>> Le 06/06/2011 13:12, Pierre Habraken a écrit :
>>> Hello,
>>>
>> Hello Pierre,
>>
>>> New features of Ada 2012 such as pre and post-conditions, type
>>> invariants, etc... would be very helpful in teaching algorithmics using
>>> Ada. Can we expect that some of these features will be implemented in
>>> the 2011 release of Gnat ?
>>> Thanks in advance for any info.
>> yes, those Ada 2012 features are implemented and will be in the GPL 2011
>> edition. Note that pre/post are already there in previous versions in
>> the form of pragmas but obviously, the 2012 syntax is nicer to use.
>>
>> Since your question is of general interest, I took the liberty to add
>> the Gap mailinglist to the recipients so that others in the GAP
>> community can see it as well.
> Note that it will be necessary to use the -gnat2012 switch to activate
> these features.
> _______________________________________________
> GAP mailing list
> GAP at gnat.info
> /no-more-mailman.html
> To unsubscribe from this list, please contact the GAP GNAT Tracker administrator
> within your organization.

Hi, this is very interesting. I have a question about the use of 
pre/post conditions in Gnat.

How are the pre/post conditions used? Is there a verification condition 
generator, and proof tool available?
Where can I find out more about these features?

Regards,
Andy