that the outputs are amenable to manipulation by machine and analysis tools.
Praxis High Integrity Systems’ Correctness by Construction [208] method, for
example (which has been in use for more than 15 years in the UK) focuses on
the accurate specification of mathematically verifiable requirements.