Formal specification of software systems using two-level grammar

Two-level grammar (TLG) is proposed for the formal specification and automatic generation of software systems. TLG specifications are unique in that they are a structured form of natural language which is executable. This has the potential for greatly increasing the reliability of the developed software system for the following reasons. Because it is a form of natural language, TLG may be used as an effective communication medium between the system users, designers, and implementors, thereby reducing the likelihood of errors caused by miscommunication. Furthermore, an efficient software system, expressed in C, can be automatically generated from the specification in a provably correct way. Successful applications have included database/knowledge-base systems and programming language compilers