Formal program developments directed by operational properties evaluation

Transformation systems allow to support developments leading from an initial specification to a final program in a totally formal way. Transformations use valid properties of input objects to produce new equivalent ones. Most transformations use functional properties to increase the efficiency of programs. Doing so, they affect non nonfunctional properties which, more often, are not formally expressed. The problem the author addresses is to recognize situations in which transformations can be achieved on the basis of the evaluation of a defined nonfunctional property and his aim is to relate program transformations to nonfunctional properties evaluations. Indeed, a particular transformation tactic can be applied when a given property does not hold. The DEVA language has been used as a support of experiments in the development of programs