Interactive Formal Specification for Mathematical Problems of Engineers
<|reference_start|>Interactive Formal Specification for Mathematical Problems of Engineers: The paper presents the second part of a precise description of the prototype that has been developed in the course of the ISAC project over the last two decades. This part describes the "specify-phase", while the first part describing the "solve-phase" is already published.   In the specify-phase a student interactively constructs a formal specification. The ISAC prototype implements formal specifications as established in theoretical computer science, however, the input language for the construction avoids requiring users to have knowledge of logic; this makes the system useful for various engineering faculties (and also for high school).   The paper discusses not only ISAC's design of the specify-phase in detail, but also gives a brief introduction to implementation with the aim of advertising the re-use of formal frameworks (inclusive respective front-ends) with their generic tools for language definition and their rich pool of software components for formal mathematics.<|reference_end|>
@article{neuper2024interactive,
    title={Interactive Formal Specification for Mathematical Problems of Engineers},
    author={Walther Neuper (JKU - Johannes Kepler Universit"at Linz)},
    journal={EPTCS 400, 2024, pp. 120-138},
    year={2024},
    doi={10.4204/EPTCS.400.8},
    archivePrefix={arXiv},
    eprint={2404.05462},
    primaryClass={cs.HC cs.LO}
}