How to reconcile formal specifications and automatic programming: the Descartes system

Much research work in computer science has been carried out in order to facilitate the software development process. Among the numerous research topics, two of them, automatic programming and formal specifications, had rarely been subject to a joint approach. Since 1992, we have developed an automatic programming system called the Descartes system, which, based on formal specifications written in a mathematical language, generates an executable program written in procedural programming language. This system has been used for several industrial applications, among which are a control-command operations scheduler for a fuel-oil based thermal power station, an emergency shut-down system for a nuclear power plant, and a fault-tree processing module. After supplying several items for comparing our work with traditional approaches in the fields of program synthesis and formal specifications, we will describe the Descartes system, the associated specification language, and will then present the results obtained to date