A propos of my disagreement with PBL ... If anyone's interested, I think I have an example of a single, small code unit for which compliance with functional requirements would be beyond a SPARK-equivalent verifier and is susceptible to verification *only* by real or simulated unit testing. FWIW, Olwen