Scholarlink

Writing declarative models has numerous benefits, ranging from automated reasoning and correction of design-level properties before systems are built, to automated testing and debugging of their implementations after they are built. Alloy is a declarative modeling language that is well-suited for verifying system designs. 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. However, even with visualized scenarios, it is difficult to write correct Alloy models. This paper presents an empirical study of over 93,000 models written mainly by users trying to learn Alloy to form a comprehensive series of observations to guide the growing body of debugging and educational efforts for Alloy model development.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Right or Wrong – Understanding How Users Write Software Models in Alloy

  • 会议论文

  • 发表日期：

    2025年

查看全文
  • Ana Jovanovic,
  • Allison Sullivan

摘要

Writing declarative models has numerous benefits, ranging from automated reasoning and correction of design-level properties before systems are built, to automated testing and debugging of their implementations after they are built. Alloy is a declarative modeling language that is well-suited for verifying system designs. 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. However, even with visualized scenarios, it is difficult to write correct Alloy models. This paper presents an empirical study of over 93,000 models written mainly by users trying to learn Alloy to form a comprehensive series of observations to guide the growing body of debugging and educational efforts for Alloy model development.