top | item 43776205 (no title) irundebian | 10 months ago In Ada you can pay for integer overflow checks (runtime) if you want to. With Ada SPARK you can prove that your code does not contain integer overflows so that you don't need runtime checks. discuss order hn newest johnisgood|10 months 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.
johnisgood|10 months 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.
johnisgood|10 months ago
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.