Executable specification languages
The system is specified in a formal language
This specification is processed and an executable system is automatically generated
At the end of the process, the specification may serve as a basis for a re-implementation of the system