一句话：为 Alloy 公式构建补全建议框架，并利用 Alloy 自动引导用户选择最符合意图的补全。
Alloy 是一种适合验证系统设计的声明式建模语言，但其操作符表达力强，手动编写正确公式十分困难。已有实证研究发现，新手用户有 75% 的时间会写出错误或无法编译的公式。为帮助开发者编写有效公式，本文提出一个在用户构造公式时提供相关补全建议的框架，并利用 Alloy 自身实现新颖的自动引导，帮助用户选择最符合其意图的补全。评估表明，生成这些建议的开销很小，排序策略有效，且自动引导能够在提供上下文与减少呈现信息量之间取得平衡。
Alloy is a declarative modeling language that is well-suited for verifying system designs. Unfortunately, writing correct Alloy models is a difficult task due to Alloy’s expressive operators, which allow for succinct formulations of complex properties, but can be hard to reason over manually. Case in point, a recent empirical study found that 75% of the time, novice Alloy users will write formulas that are incorrect or fail to compile. To aid developers in writing valid formulas, we outline a framework in which the user is presented with relevant completion suggestions as they are constructing their formulas. Moreover, using Alloy itself, we provide novel automated guidance that helps users select the completion that best matches their intention. Our evaluation highlights that there is nominal overhead to create these suggestions, our ranking strategy is effective, and our automated guidance can balance providing context with reducing the amount of information we present.