描述用于测试学生提交的 Haskell 控制台 I/O 行为
Describing Console I/O Behavior for Testing Student Submissions in Haskell
AI总结：
提出一种形式化语言用于指定控制台I/O程序行为，以测试学生编写的Haskell程序，并支持概率性机械检查及教育中的反馈与任务生成。
摘要：
我们提出了一种小型形式化语言，用于指定简单控制台 I/O 程序的行为。该设计由测试学生编写的交互式 Haskell 程序这一具体应用案例驱动。规范在结构上类似于词法分析正则表达式，但增加了跟踪程序运行状态和历史记录的全局变量等功能，从而能够表达一系列有趣的动态行为。我们基于执行轨迹的接受性为该规范语言提供了语义。基于该语义，我们推导出了对给定规范有效的所有轨迹集合的定义。通过对该集合进行采样，我们能够以概率方式机械地检查程序行为是否符合规范。除了测试之外，该规范语言在教育环境中的其他可能用途包括提供更有帮助的反馈、生成示例解决方案，甚至生成随机练习任务等相关活动。
英文摘要：
We present a small, formal language for specifying the behavior of simple console I/O programs. The design is driven by the concrete application case of testing interactive Haskell programs written by students. Specifications are structurally similar to lexical analysis regular expressions, but are augmented with features like global variables that track state and history of program runs, enabling expression of an interesting range of dynamic behavior. We give a semantics for our specification language based on acceptance of execution traces. From this semantics we derive a definition of the set of all traces valid for a given specification. Sampling that set enables us to mechanically check program behavior against specifications in a probabilistic fashion. Beyond testing, other possible uses of the specification language in an education context include related activities like providing more helpful feedback, generating sample solutions, and even generating random exercise tasks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
