2 ms·
Yes. Latest language standard is Ada 2012. Spark, a subset of Ada 2012 supports formal proofs of program properties ranging from absence of run-time errors to
by joubert 7y ago
Yes.
Latest language standard is Ada 2012.
Spark, a subset of Ada 2012 supports formal proofs of program properties ranging from absence of run-time errors to functional correctness (compliance of the code with formally specified requirements).
If you're curious, you can learn more at https://learn.adacore.com/courses/courses.html https://learn.adacore.com/courses/courses.html
- johnisgood 7y agoMore links: https://www.adacore.com/uploads/books/pdf/AdaCore-Tech-Cyber-Security-web.pdf https://www.adacore.com/uploads/books/pdf/AdaCore-Tech-Cyber... https://www.adacore.com/gems https://www.adacore.com/gems -> https://blog.adacore.com/ https://blog.adacore.com/ https://web.archive.org/web/20190709111613/http://www.drdobbs.com/architecture-and-design/ada-2012-ada-with-contracts/240150569 https://web.archive.org/web/20190709111613/http://www.drdobb... https://github.com/Componolit/libsparkcrypto https://github.com/Componolit/libsparkcrypto https://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/14/140201-fosdem/03-ada-spark.pdf https://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/ev... https://www.adacore.com/uploads/books/pdf/ePDF-ImplementationGuidanceSPARK.pdf https://www.adacore.com/uploads/books/pdf/ePDF-Implementatio... http://www.loper-os.org/?p=1913 http://www.loper-os.org/?p=1913 https://github.com/ohenley/awesome-ada https://github.com/ohenley/awesome-ada