StatWhy：用于统计假设检验程序的形式化验证工具

统计方法在各个科学领域中被广泛误用和误解，引发了对科学研究完整性的严重担忧。为缓解这一问题，我们提出了一种工具辅助方法，用于形式化规约并自动验证统计程序的正确性。在该方法中，程序员需要在这些统计程序的源代码中为其标注相关要求。通过这种标注，提醒他们检查统计方法的要求，包括那些无法进行形式化验证的要求，例如未知真实总体的分布。我们的软件工具 StatWhy 会自动检查程序员是否正确规约了统计方法的要求，从而识别出需要处理的任何缺失要求。该工具使用 Why3 平台实现，以验证执行统计假设检验的 OCaml 程序的正确性。我们演示了如何使用 StatWhy 来避免各种统计假设检验程序中的常见错误。