Denotational engineering (Q1825025)

A systematic methodology of using denotational techniques in software design is presented. It is suggested to develop denotations at first and to derive syntax from them consequently, as denotations specify the essential components of designed system whilst syntax serves as a tool how to access them. This process is systematically divided into four steps (each of them could consists of several substeps); in each step a corresponding many-sorted algebra is defined/derived: (1) Develop a model of a designed system, i.e. define an algebra Dat specifying objects which are to be manipulated and operations over them. Dat is enriched by utilities supplied by a computer system environment and an algebra Sys is obtained. Bottom-up: Dat\(\to Sys\) and top-down: Sys\(\to Dat\) approaches are discussed. (2) Define user interface (an algebra Den) by the selection of the objects and the operations of Sys which are to be visible by the user (restriction: Sys\(\to Den).\) (3) Derive prototype syntax Term for denotations selected in (2). (Term algebra Term is uniquely determined by the signature of Den.) (4) Transform (stepwise) the prototype syntax Term (via homomorphic refinements) to obtain desired syntax Syn which is sufficiently convenient and which is correct with respect to Den. The proposed method is illustrated by two examples and some open problems related to the derivation of syntax are discussed.