Evaluation criteria for functional specifications
Sergio R. Cárdenas, Marvin V. Zelkowitz · 1990
Functional correctness is a technique for deriving a program and proving that this program meets its specifications. Both a program and its specifications are viewed as &nctions. Using techniques based upon symbolic execution and denotational semantics, a proof methodology has been developed. This current paper extends this theory of functional specifications which then permits us to model various life cycle methods in a consistent manner. Given several possible implementations for a given specification, we then develop techniques for evaluating one implementation over another.