一句话：提出描述 Haskell 控制台 I/O 交互行为的规约语言与自动测试框架，并用约束求解器生成有意义的输入序列。
在 Haskell 教学中，测试纯函数程序已有 QuickCheck 等成熟工具，但控制台 I/O 程序的交互行为难以用声明式性质描述，自动评分与学生自测都缺乏支持。本文用程序文本输入/输出动作的 trace 刻画控制台交互，并设计一种形式规约语言来描述哪些 trace 符合预期行为。该语言有意限制表达力，以确保所描述的是真正交互行为，而非伪装的纯字符串生成函数，同时保持规约简洁清晰。基于该语言，作者实现自动测试框架，其核心是用约束求解器为被测程序寻找有意义的输入序列，从而支持对 Haskell 控制台 I/O 程序进行自动化测试。
Abstract Good test-suites are an important tool to check the correctness of programs. They are also essential in unsupervised educational settings, like automatic grading or for students to check their solution to some programming task by themselves. For most Haskell programming tasks, one can easily provide high-quality test-suites using standard tools like QuickCheck. Unfortunately, this is no longer the case once we leave the purely functional world and enter the lands of console I/O. Nonetheless, understanding console I/O is an important part of learning Haskell, and we would like to provide students the same support as with other subject matters. The difficulty in testing console I/O programs arises from the standard tools’ lack of support for specifying intended console interactions as simple declarative properties. These interactions are however essential in order to determine whether a program behaves as desired. We describe the console interactions of a program by tracing its text input and output actions. In order to describe which traces match the intended behavior of the program under test, we present a formal specification language. The language is designed to capture interactive behavior found in commonly used textbook exercises and examples, or as much of it as possible, as well as in our own teaching, while at the same time retaining simplicity and clarity of specifications. We intentionally restrict the language, ensuring that expressed behavior is truly interactive and not simply a pure string-builder function in disguise. Based on this specification language, we build a testing framework that allows testing against specifications in an automated way. A central feature of the testing procedure is the use of a constraint solver in order to find meaningful input sequences for the program under test.
@article{WestphalV25,
title = {Automatically testing console I/O behavior of student submissions in Haskell},
author = {OLIVER WESTPHAL and JANIS VOIGTLÄNDER},
journal = {Journal of Functional Programming},
volume = {35},
year = {2025},
doi = {10.1017/s0956796825100075}
}