Design Lessons From Binary Fission: A Crowd Sourced Game for Precondition Discovery
Design Lessons From Binary Fission: A Crowd Sourced Game for Precondition Discovery
复制标题
二元裂变的设计经验：用于前提条件发现的众包游戏
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
B. Laurel
中科院分区：
文献类型：
--
作者：
K. Compton;Heather Logas;J. Osborn;Chandranil Chakraborttii;Kelsey A. Coffman;D. Fava;Dylan Lederle;Zhongpeng Lin;J. Mazeika;Afshin Mobramaein;Johnathan Pagnutti;H. Sánchez;E. J. Whitehead;B. Laurel
二进制裂变的优点之一是它很好地抽象出了形式软件验证的混乱细节，并将其作为一个简单的排序问题。这允许Binary Fission表示各种数据类型和谓词，并从各种程序中获取输入数据。这也使Binary Fission能够被广泛的受众访问。然而，这种抽象也让玩家对玩游戏失去了兴趣。一小部分玩家想知道更多关于夸克、过滤器和排序背后的数学基础，并对缺乏关于任何特定问题的信息感到沮丧。在可表达性和灵活性之间找到正确的平衡点是众包形式验证游戏的核心问题。此外，在如此高的抽象层次上利用人类与生俱来的空间直觉技能变得更加困难。
ion of formal verification One of the strengths of Binary Fission is how well it abstracts away the messy details of formal software verification and presents it as a simple sorting problem. This allows for Binary Fission to represent a wide range of data types and predicates, and get input data from a wide variety of programs. This also keeps Binary Fission accessible to a wide audience. However, this abstraction also turned players off to playing the game. A subset of players wanted to know more about the mathematical underpinnings behind the quarks, filters and sorting, and felt frustrated by the lack of information they could get about any particular problem. Finding the correct balance between expressibility and flexibility is a core problem in crowd sourced formal verification games. In addition, it becamemore difficult to leverage the innate human skill of spacial intuition at such a high level of abstraction.