一句话：通过受控实验与出声思维，研究模型查找器输出中一次展示实例数量及展示负实例的价值。
模型查找器（如 SAT/SMT 求解器和 Alloy）既用于常规验证，也支持无性质探索，但其输出设计缺乏严格的人因研究。传统工具通常一次只展示一个满足实例。本文借鉴认知科学，考察两个输出维度：一次展示多少实例，以及是否必须只展示满足输入约束的实例。作者采用受控实验和开放式出声思维，发现某些场景下展示负实例（不满足约束的实例）有益，而多实例展示的影响尚不明确。该工作为从理论出发理解用户如何认知加工模型查找器输出、以及工具如何更好支持用户迈出第一步。
Model-finders, such as SAT/SMT-solvers and Alloy, are used widely both directly and embedded in domain-specific tools. They support both conventional verification and, unlike other verification tools, property-free exploration. To do this effectively, they must produce output that helps users with these tasks. Unfortunately, the output of model-finders has seen relatively little rigorous human-factors study. Conventionally, these tools tend to show one satisfying instance at a time. Drawing inspiration from the cognitive science literature, we investigate two aspects of model-finder output: how many instances to show at once, and whether all instances must actually satisfy the input constraints. Using both controlled studies and open-ended talk-alouds, we show that there is benefit to showing negative instances in certain settings; the impact of multiple instances is less clear. Our work is a first step in a theoretically grounded approach to understanding how users engage cognitively with model-finder output, and how those tools might better support users in doing so.
@article{paperbot1533,
title = {Applying cognitive principles to model-finding output: the positive value of negative information},
author = {Tristan Dyer and Tim Nelson and Kathi Fisler and Shriram Krishnamurthi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA1},
year = {2022},
doi = {10.1145/3527323}
}