[Spark2014-discuss] Foo'Result'First strange behavior
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