|
|
|
|
|
|
by nickpsecurity
3091 days ago
|
|
|
That's Design-by-Contract. On checking side, one can generate tests from specs, static analysis, turn them plus code into verification conditions to feed to solvers, or inputs to theorem prover for handling complex stuff. Eiffel implements DbC with test generation. SPARK Ada does automated and manual proofs. Ada 2012 added contracts but idk tool support. Many languages have ways of emulating this functionality, too. What you're describing is essentially a proven, lightweight, formal method for improving software quality. Many commercial apps use it. |
|
|