Applying Cognitive Principles to Model-Finding Output: The Positive Value of Negative Information
Applying Cognitive Principles to Model-Finding Output: The Positive Value of Negative Information
复制标题
DOI：
10.1145/3527323
复制
发表时间：
2022-04-01
影响因子：
1.8
通讯作者：
Krishnamurthi，Shriram
中科院分区：
文献类型：
--
作者：
Dyer，Tristan;Nelson，Tim;Krishnamurthi，Shriram
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.
