Rapid prototyping of system enhancements

Consideration is given to AS*, a language-independent specification language to be embedded within an existing programming language for the purpose of providing extensions to existing systems. The initial implementation extends Pascal with AS* specifications (called ASPascal) and the toolset consists of a source code editing system built on top of a syntax editor called AS/SUPPORT, a Prolog verification tool called AS/VERIFY for checking the consistency of the specification, and a translator called AS/PC for converting the extended Pascal program into standard Pascal for compilation and execution. The authors discuss the designs of AS*, the structure of the prototype implementation, and the formal verification of the underlying axioms in a specification