3 ms·
Fairly short course on SPARK/Ada - https://learn.adacore.com/courses/intro-to-spark/index.html https://learn.adacore.com/courses/intro-to-spark/index.html SPAR
by Jtsummers 2y ago
Fairly short course on SPARK/Ada - https://learn.adacore.com/courses/intro-to-spark/index.html https://learn.adacore.com/courses/intro-to-spark/index.html
SPARK's pre-/postconditions and assertions can be statically checked, they aren't just for runtime enforcement. This is its key value proposition, if it were just runtime enforcement it'd be nice, but not that great.