Ada conference, Ada and Spark

[bearophile]

Meta:

> What are the limitations on what Static_Predicate can verify? 
> It seems like this could be quite powerful, but not as powerful 
> as runtime checks, since not everything can be checked at 
> compile time.

In Ada there is Dynamic_Predicate for the other cases :-)


> Does the loop break if the invariant fails, or does it stop the 
> program?

Ada has an elaborate infrastructure to allow you to choose how to 
react to failures, how to handle them, what failures to ignore, 
etc. At least, it stops the program.


> I don't think this is quite as important, seeing as D has the 
> pure keyword.

Purity means you can't use mutable values from outer scopes. The 
point of those Spark annotations (and @outer()) is to do the 
opposite: to specify the flow of information in system 
programming when you are not using purity.

Bye,
bearophile