This ESPRIT project integrates formal proof techniques and abstraction mechanisms within a common framework to create an environment for scientific software design. It focuses upon recent developments concerning abstraction of data types, data base management, specification and program verification.