Interactive Formal Specification for Mathematical Problems of Engineers

TL;DR

The paper addresses how to design the specify-phase of the ISAC system, bridging informal problem descriptions to formal specifications for engineering education. It presents an architecture built on Isabelle/Isar, with data models for Given/Find/Relate, interactive feedback, and stepwise construction guiding users toward a formal spec. Key contributions include formalising a running example, template-based problem authoring, simplified Relate postconditions, and a feedback mechanism compatible with PIDE. The work enables reuse of proof-assistant tooling for language definitions and emphasizes transitioning to a proof-based solve-phase with Lucas-Interpretation.

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.

Figures (5)

• Figure 1: The template for starting a Specification.
• Figure 2: The complete Specification.
• Figure 3: The tree of equations (middle panel).
• Figure 4: The Model for the Method_Ref.
• Figure 5: The problem-pattern for the running example.