[Spark2014-discuss] [M122-037] specifying SPARK sources for analysis

Cyrille Comar comar at adacore.com
Thu Mar 14 14:46:25 CET 2013

I agree with your general message but wanted to react on this specific

Le 14/03/2013 14:41, Arnaud Charlet a écrit :

>  we do not want to start having to do proof on parts of subprograms only, 

well, pragma Assert_And_Cut could allow us to explore this possibility but
     - this is a bit early to consider
     - there is no need to take this case into consideration in this
discussion (it can be assimilated to subprograms completely provable
with a minor twist)

More information about the Spark2014-discuss mailing list