|
|
|
|
|
|
by Jtsummers
375 days ago
|
|
|
Yes. See SPARK for an example of this. It is a subset of Ada plus the SPARK portions to convey details and proofs. You can use it per file, not just on an entire program, which lets you prove properties of critical parts and leave the rest to conventional testing approaches. |
|
|