 |
| |||
| perform modular formal verification (To prove the post condition of a subprogram according to its own precondition and the precondition and postconditions of its callees (ie, those subprograms that it calls) whether or not these callees are themselves proven. For a complete, 100%, proof, all the subprograms of an application need to be formally proven; корпорации AdaCore; контекстуальный перевод на русс. язык Alex_Odeychuk) | |||