User Guided Executable Specifications

One of the big drawbacks of classical methods for specifying software requirements is that it is difficult to check the consistency and adequacy of a given specification. The software engineering community has come up with many remedies to this situation (e.g., model based software engineering, agile software development, executable algebraic specification) that usually aim at allowing the user to see the actual behavior of a given specification as early as possible in the development process, but that make compromises in terms of modeling power or precision. In the thesis, the student will design an executable formal specification language that fulfills two seemingly contradicting objectives: The key to achieving both objectives at the same time will be the design of annotations for the specification language that provide information necessary of efficient execution. Increasing user efforts in writing annotations will result in increasing efficiency of execution of the given specification. In a first step, we will develop a tool that will serve for educational purposes, allowing students to execute specifications they write as assignments.