← Back to context

Comment by johnisgood

1 day ago

And you can disable these checks with a flag when it comes to Ada, and yeah, with SPARK, none of it happens at runtime.

Check the table at https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce..., look for "SPARK builds on the strengths of Ada to provide even more guarantees statically rather than dynamically.".

More reading:

https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial....

https://learn.adacore.com (many books for learning Ada and SPARK) available in PDF, EPUB, and HTML format.

0 comments

johnisgood

Reply