The role for executable specifications in system maintenance

As software becomes increasingly complex, two attributes of the system life cycle are taking on more important roles. We need the ability to formally specify the functionality of the systems we build in order to minimize costly development problems and, with long life times, we need the ability to enhance existing systems with new features in order to prolong their usefulness. This enhancement process also needs a mechanism for formally defining any new functionality on data objects placed upon the system. This paper describes the AS∗ research project which is addressing this issue. AS∗ is a language-independent specification language embedded within an existing programming language for the purpose of providing extensions to existing systems. This paper discusses the designs of AS∗, the structure of the prototype implementation and describes some early experiences using the system.