[GAP] Ada 2012 in Gnat 2011 ?

[Rod Chapman]

> > Is there a verification condition generator, and proof tool available?

You could also go for the SPARK GPL edition, which really
does have a fully working, and industrially fielded,
VC generator and theorem prover. The contracts
in SPARK are specifically designed for static verification,
not dynamic, so the emphasis is a bit different from those
coming in Ada2012...

All the best,
 Rod Chapman, SPARK Team, Altran Praxis

This email is confidential and intended solely for the use of the individual to whom it is addressed. If you are not the intended recipient, be advised that you have received this email in error and that any use, disclosure, copying or distribution or any action taken or omitted to be taken in reliance on it is strictly prohibited. If you have received this email in error please contact the sender. Any views or opinions presented in this email are solely those of the author and do not necessarily represent those of Altran Praxis. 

Although this email and any attachments are believed to be free of any virus or other defect, no responsibility is accepted by Altran Praxis or any of its associated companies for any loss or damage arising in any way from the receipt or use thereof. The IT Department at Altran Praxis can be contacted at it.support at altran-praxis.com.

Altran Praxis Ltd:

Company Number: 3302507, registered in England and Wales

Registered Address: 20 Manvers Street, Bath. BA1 1PX

VAT Registered in Great Britain: 682635707