A temporal logic language for system implementation

摘要

The XYZ system consists of a temporal logic language XYZ/E and several supporting tools. This paper introduces many special features of XYZ/E with its tools which are desirable for a good implemenation language in addition to portability and efficiency. These features include (1) its suitability for stepwise refinement, specification of different abstract levels, verification and rapid prototyping, (2) modules and visual tools to support programming in the large and and (3) a simple, formal method and a corresponding tool for transforming a program from another source language into XYZ/E, a feature which is useful for software reengineering and for embedding standard programs from other languages into an XYZ/E.