论文标题
使用ACL2教学生软件测试
Using ACL2 To Teach Students About Software Testing
论文作者
论文摘要
我们报告了在课堂上使用ACL2使用ACL2的经验，以向学生传授软件测试。怀俄明大学的COSC2300课程是传统的离散数学课程，但明确关注计算机科学应用程序。例如，关于逻辑和证据的部分是由渴望写有关计算机软件的证据的愿望的动机。我们强调，软件正确性的重要性沿着一端的随意程序而属于一个频谱，另一端是关键任务。与此频谱相对应的是多种工具，包括单位测试，属性的随机测试，甚至是正式的证明。在本文中，我们描述了一项主要活动之一，其中学生使用ACL2轿车的反示例生成设施来研究错误检测中使用的各种现有校验和算法的属性。学生面临正确陈述相关属性的挑战，以便在所有情况下有效地使用反示例生成工具，并且ACL2可以在其中一些中自动找到正式的证据。
We report on our experience using ACL2 in the classroom to teach students about software testing. The course COSC2300 at the University of Wyoming is a mostly traditional Discrete Mathematics course, but with a clear focus on computer science applications. For instance, the section on logic and proofs is motivated by the desire to write proofs about computer software. We emphasize that the importance of software correctness falls along a spectrum with casual programs on one end and mission-critical ones on the other. Corresponding to this spectrum is a variety of tools, ranging from unit tests, randomized testing of properties, and even formal proofs. In this paper, we describe one of the major activities, in which students use the ACL2 Sedan's counter-example generation facility to investigate properties of various existing checksum algorithms used in error detection. Students are challenged to state the relevant properties correctly, so that the counter-example generation tool is used effectively in all cases, and ACL2 can find formal proofs automatically in some of those.
