Interactive Formal Specification for Mathematical Problems of Engineers
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866910407711522816 |
|---|---|
| author | Neuper, Walther |
| author_facet | Neuper, Walther |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_05462 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Interactive Formal Specification for Mathematical Problems of Engineers Neuper, Walther Human-Computer Interaction Logic in Computer Science H.5.2; I.5.5; F.4.m 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. |
| title | Interactive Formal Specification for Mathematical Problems of Engineers |
| topic | Human-Computer Interaction Logic in Computer Science H.5.2; I.5.5; F.4.m |
| url | https://arxiv.org/abs/2404.05462 |