How Do We Read Formal Claims? Eye-Tracking and the Cognition of Proofs about Algorithms
How Do We Read Formal Claims? Eye-Tracking and the Cognition of Proofs about Algorithms
复制标题
DOI：
10.1109/icse48619.2023.00029
复制
发表时间：
2023-05
期刊：
影响因子：
--
通讯作者：
Hammad Ahmad;Z. Karas;Kimberly Diaz;A. Kamil;Jean-Baptiste Jeannin;Westley Weimer
中科院分区：
文献类型：
--
作者：
Hammad Ahmad;Z. Karas;Kimberly Diaz;A. Kamil;Jean-Baptiste Jeannin;Westley Weimer
正式方法成功地用于高保险软件中，但是它们需要严格的数学和逻辑培训，而从业者通常缺乏。因此，将正式方法集成到软件中与许多挑战有关。尽管教育工作者强调本科理论课程中的形式主义，但这些课程通常与学生的成果和满意度差。在本文中，我们提出了一项受控眼神的人类研究（n = 34），研究了具有不同来源准备的学生采用的解决问题的策略（根据理论课程工作和在证明理解任务上进行预先筛查的绩效评估），以及教育工作者如何更好地为低成本的学生做好准备，以使其严格的逻辑推理是软件工程正式方法的核心部分。出人意料的是，我们发现传入的准备并不是对形式主义理解任务的学生成果的良好预测指标，并且学生的自我报告并不准确地识别与此类任务相关的高成果相关的因素。相反，重要的是，我们发现结果的差异可以归因于通过归纳和递归算法证明的绩效，并且表现更好的学生表现出更大的关注转换行为，这一结果对设计对设计具有多种影响。教材。我们的结果表明，需要在核心理论课程中进行大量的教学干预，以使学生成果与精通和保留材料的目标相结合，从而改善学生为高保证软件工程做准备。
Formal methods are used successfully in high-assurance software, but they require rigorous mathematical and logical training that practitioners often lack. As such, integrating formal methods into software has been associated with numerous challenges. While educators have placed emphasis on formalisms in undergraduate theory courses, such courses often struggle with poor student outcomes and satisfaction. In this paper, we present a controlled eye-tracking human study (n = 34) investigating the problem-solving strategies employed by students with different levels of incoming preparation (as assessed by theory coursework taken and pre-screening performance on a proof comprehension task), and how educators can better prepare low-outcome students for the rigorous logical reasoning that is a core part of formal methods in software engineering. Surprisingly, we find that incoming preparation is not a good predictor of student outcomes for formalism comprehension tasks, and that student self-reports are not accurate at identifying factors associated with high outcomes for such tasks. Instead, and importantly, we find that differences in outcomes can be attributed to performance for proofs by induction and recursive algorithms, and that better-performing students exhibit significantly more attention switching behaviors, a result that has several implications for pedagogy in terms of the design of teaching materials. Our results suggest the need for a substantial pedagogical intervention in core theory courses to better align student outcomes with the objectives of mastery and retaining the material, and thus bettering preparing students for high-assurance software engineering.