A unifying framework for correct program construction

Abstract

We present a description technique for the correct construction of programs that allows us to define terms like refinement, modelchecking, and synthesis as special operations within this framework. From that meta-view on program constructions both advantages and disadvantages of all methods mentioned become clear. Furthermore, it becomes clear that an incremental program construction seems to be the most suitable method to construct programs. To demonstrate this incremental construction method we present a real-time case study.