[GAP] Ada 2012 in Gnat 2011 ?

[Cyrille Comar]

Le 06/06/2011 14:48, Andy Edmunds a écrit :

> 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?

In the language itself (Ada 2012) they have a dynamic semantics close to 
Eiffel's and thus can be seen as a generalization of dynamic checks as 
provided by older Ada versions for index, range and overflow checks. 
This is particularly true for subtype predicates.

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

That's interesting you ask the question because we do participate to a 
research project whose goal is precisely to use those new Ada2012 
features for program proving and better integration of testing and 
proving. Take a look at http://www.open-do.org/projects/hi-lite/ and if 
you are interested, you can register to the mailinglist which is pretty 
active (and sometimes very technical).

> Where can I find out more about these features?

Good starting points for Ada2012 are:

  http://www.adacore.com/home/ada_answers/ada-2012/
  http://www.ada-auth.org/standards/ada12.html

Ed (Schonberg) made a presentation last year that can be found at 
http://www.disca.upv.es/jorge/ae2010/slides/05-3_Language_Tech_Schonberg_Towards_Ada_2012.pdf

John Barnes is working on a rationale that should be available later 
this year.