Structural synthesis of programs from refined user requirements (Programming boiler control in NUT)

Abstract

The aim of this work is to demonstrate the feasibility of using a declarative language as a tool for automated implementation of requirements written in a semiformal manner. The technique of structural synthesis of programs based on automatic proof search in intuitionistic propositional calculus implemented in the NUT system is used for solving the steam-boiler problem. The goal of the experiment is to bridge the gap between the language of requirements and an implementation. An appropriate set of concepts is developed to represent the problem, i.e. the requirements are written in a form understandable by the program synthesis tools. An implementation, including simulator of the actual steam-boiler and control panel, is written in NUT. The program synthesizer is a part of the specification language compiler and it is completely hidden from the user.