Get back to me when the formal methods actually generate high quality code that cannot deviate from the spec.
Get back to me when the formal methods actually generate high quality code that cannot deviate from the spec.
This summary page links to the full PDF: https://www.adacore.com/tokeneer
That would be useful but there is a fundamental issue: code is too specific. İn formal specification you usually don't specify that detailed but you specify the general behaviour of the system. So usually the specification corresponds to a lot of programs with subtle differences. That's why code a documentation falls short: you don't know what is intentional and what is just a random choice. It's simply too specific to describe high level requirements.
The other way around (verification of program with respect to the specification) can be more feasible to implement.