Structure Editor for Building Software Models
Mohammad Nurullah Patwary, Ana Jovanovic, Allison Sullivan
TL;DR
The paper tackles the problem that novices struggle to learn Alloy and encounter frequent compilation errors, even with Analyzer feedback. It proposes a proof-of-concept structure editor that uses block-based inputs to actively reveal grammar and type implications during model construction, aiming to prevent syntax and type errors. Central contributions include a Scratch-inspired three-panel UI, a categorized block taxonomy, and mechanisms (holes, extension points, and constraint checks) to enforce syntactic validity and type-correctness during construction. If realized, this approach could significantly reduce initial learning barriers and broaden adoption of formal methods by front-loading error prevention and education into the modeling process.
Abstract
Alloy is well known a declarative modeling language. A key strength of Alloy is its scenario finding toolset, the Analyzer, which allows users to explore all valid scenarios that adhere to the model's constraints up to a user-provided scope. Despite the Analyzer, Alloy is still difficult for novice users to learn and use. A recent empirical study of over 93,000 new user models reveals that users have trouble from the very start: nearly a third of the models novices write fail to compile. We believe that the issue is that Alloy's grammar and type information is passively relayed to the user despite this information outlining a narrow path for how to compose valid formulas. In this paper, we outline a proof-of-concept for a structure editor for Alloy in which user's build their models using block based inputs, rather than free typing, which by design prevents compilation errors.