[Spark2014-discuss] [M503-001] SPARK 2014: proof rules for type invariants

Steve Baird baird at adacore.com
Fri May 3 23:17:21 CEST 2013

On 05/03/2013 01:50 PM, Tucker Taft wrote:
> On 5/3/13 4:46 PM, Steve Baird wrote:
>> ... Does that make things clearer?
> Could you provide the Ada code for these examples?
> My brain reads Ada better than English. ;-)

Will do.

I was playing a little fast and loose with Pre vs. Pre'Class
in my text description, so a real example might help with that.

   -- Steve

More information about the Spark2014-discuss mailing list