面向形式化方法轻量级绘图的接地语言设计
Grounded Language Design for Lightweight Diagramming for Formal Methods
AI总结：
针对形式化工具默认可视化无效而完整可视化成本高的问题，本文基于认知科学与实例设计正交绘图原语并扩展类 Alloy 工具，实现轻量且有效的模型图形表示。
摘要：
模型求解（以 SAT 求解器及类似工具为代表）应用广泛，既用于嵌入式场景，也作为独立工具使用。例如，Alloy 等工具以 SAT 为目标，使用户能够为大量复杂系统增量式地定义、探索、验证和诊断复杂规约。这些工具至关重要地包含一个可视化器，让用户以图形方式探索这些生成的模型。然而，正如我们所示，对领域一无所知的默认可视化器不仅没有帮助，甚至会主动违背呈现和认知原则。另一个极端是，成熟的可视化需要大量精力以及规约者可能不具备的知识；它们还可能表现出糟糕的失败模式（包括静默失败）。相反，我们需要一种语言来捕获轻量级绘图所需的基本领域信息。我们将语言设计同时建立在关于图形的认知科学文献和大量自定义可视化示例之上，由此识别出轻量级图形的关键元素。我们将这些元素提炼为一小组正交原语，并扩展了一个类似 Alloy 的工具以支持这些原语。我们评估了所生成图形的有效性，发现它们适合推理。随后，我们将其与许多其他绘图语言和工具进行比较，表明这项工作定义了一个轻量、有效且由可靠原则驱动的新细分领域。
英文摘要：
Model finding, as embodied by SAT solvers and similar tools, is used widely, both in embedding settings and as a tool in its own right. For instance, tools like Alloy target SAT to enable users to incrementally define, explore, verify, and diagnose sophisticated specifications for a large number of complex systems. These tools critically include a visualizer that lets users graphically explore these generated models. As we show, however, default visualizers, which know nothing about the domain, are unhelpful and even actively violate presentational and cognitive principles. At the other extreme, full-blown visualizations require significant effort as well as knowledge a specifier might not possess; they can also exhibit bad failure modes (including silent failure). Instead, we need a language to capture essential domain information for lightweight diagramming. We ground our language design in both the cognitive science literature on diagrams and on a large number of example custom visualizations. This identifies the key elements of lightweight diagrams. We distill these into a small set of orthogonal primitives. We extend an Alloy-like tool to support these primitives. We evaluate the effectiveness of the produced diagrams, finding them good for reasoning. We then compare this against many other drawing languages and tools to show that this work defines a new niche that is lightweight, effective, and driven by sound principles.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
