POSIX shell的可执行形式语义

POSIX shell是一种广泛部署的、用于管理计算机系统的强大工具。shell是专家的控制面板，是配置、编译、安装、维护和部署系统所必需的工具。尽管它是强大且关键的基础设施，POSIX shell却饱受诟病且常被误解。它的强大与微妙之处是一种危险的组合。我们为POSIX shell定义了一种形式化、机械化、可执行的small-step语义，称之为Smoosh。我们将Smoosh与另外七个旨在一定程度上符合POSIX标准的shell（bash、dash、zsh、OSH、mksh、ksh93和yash）进行了比较。使用三个测试套件——POSIX测试套件、Modernish测试套件与shell诊断，以及我们自行设计的测试套件——我们发现Smoosh的语义最符合POSIX标准。Modernish判定Smoosh的bug最少（仅一个，源于使用dash的解析器）且没有怪异行为。为了表明我们的语义除了产生一个合规的、可执行的shell之外还有用，我们还实现了一个符号步进器以阐明shell的微妙行为。Smoosh将作为POSIX shell形式化研究的基础，支持新shell、新shell工具以及新shell设计的研究与开发。