[Spark2014-discuss] Foo'Result'First strange behavior

Hugues Jérôme hugues.jerome at gmail.com
Tue Jul 22 16:35:01 CEST 2014


Le 22 juil. 2014 à 14:19, Yannick Moy <moy at adacore.com> a écrit :

>> AFAICT, the postcondition and the assertion refers to the same entity. Is it a known limitation in the toolset?
> 
> Yes, there are limitations in the GPL 2014 version wrt proof of unconstrained arrays. This has been much improved in the current development version, and I can now prove your code completely. 

Thanks, this is good to know, I may now jump to the next exercise (and then write the next question for you !)





More information about the Spark2014-discuss mailing list