Overview

Isabelle/jEdit is referenced as the front-end used in an example HOL-TestGen session. In the cited case-study paper, Figure 2 is captioned as “A HOL-TestGen Session Using the Isabelle/jEdit Front-End,” directly identifying Isabelle/jEdit as the user-facing front-end for that session.[C1]

Technical context

The evidence places Isabelle/jEdit in the broader Isabelle/HOL tooling context. Isabelle is described as a proof assistant with a kernel intended to ensure logical correctness, customizable to logics including first-order logic, Zermelo-Fraenkel set theory, and higher-order logic.[C2] Isabelle is also described as an interactive development environment that provides immediate feedback during formal proof attempts and symbolic computations, and includes automatic reasoning tools such as term rewriting and decision procedures.[C3]

Use with HOL-TestGen

HOL-TestGen is described as a formal tool built on top of Isabelle/HOL.[C4] The same source characterizes HOL-TestGen as a document-centric modeling environment for test theories, test specifications, and test generation methods implemented using Isabelle tactic procedures.[C5] The explicit figure caption shows such a HOL-TestGen session being conducted through the Isabelle/jEdit front-end.[C1]

Role in the cited workflow

Within the cited workflow, Isabelle/jEdit is not described as the test generator itself. Rather, the evidence supports describing it as the front-end through which a HOL-TestGen session is presented or operated. The test-generation method attributed to HOL-TestGen includes test case generation, test data selection using constraint-solving techniques including random generation and Z3, and a test execution phase.[C6]