Interactive Formal Specification for Mathematical Problems of Engineers
Abstract
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.
Cite
@article{arxiv.2404.05462,
title = {Interactive Formal Specification for Mathematical Problems of Engineers},
author = {Walther Neuper},
journal= {arXiv preprint arXiv:2404.05462},
year = {2024}
}
Comments
In Proceedings ThEdu'23, arXiv:2404.03709