Work in Progress: ESPECIFICA++, a DSL for Developing the Competency of Formal Specification in Computer Programming Education

Competence in Formal specification is a key skill with which Computing Engineering students often face significant challenges. In this paper, we propose ESPECIFICA++, a domain-specific language (DSL) embedded in the programming language C++ that allows for the description of executable specifications, resulting in a promising tool for fostering the development of formal specification skills among students. Using ESPECIFICA++, students can describe aspects such as preconditions, postconditions, and algorithm invariants. These descriptions then become executable objects that can be validated against sets of test cases, as if they were programs. The paper describes the development process and the current stage in the development of the DSL, outlines the main features of ESPECIFICA++, and conducts a preliminary evaluation of its applicability and usefulness.