An integrated system to support program design development and analysis

The paper describes an interactive programming system which provides an integrated collection of tools for dealing with the whole process of program development (from program design to program maintenance). The pivot tool, the symbolic interpreter, may cover a broad range of applications (debugging, testing, formal verification). The main features of the symbolic interpreter, i.e. the possibility of handling non deterministic branching at choice points and the presence of a system for symbolic expression manipulation, are described. The programming system is built around a high-level language, which provides few simple independent semantic constructs and powerful extension mechanisms. Furthermore, the relation between top-down design and formal specification of abstractions is discussed in the framework of the programming system.