Statistical methods have been widely misused and misinterpreted in various scientific fields, raising significant concerns about the integrity of scientific research. To develop techniques to mitigate this problem, we propose a new method for formally specifying and automatically verifying the correctness of statistical programs. In this method, programmers are reminded to check the requirements for statistical methods by annotating their source code. Then, a software tool called StatWhy automatically checks whether the programmers have properly specified the requirements for the statistical methods. This tool is implemented using the Why3 platform to verify the correctness of OCaml programs for statistical hypothesis testing. We demonstrate how StatWhy can be used to avoid common errors in a variety of popular hypothesis testing programs.

翻译：统计方法在多个科学领域中被广泛误用和误解，引发了人们对科学研究完整性的严重担忧。为开发缓解此问题的技术，我们提出了一种新方法，用于形式化规约并自动验证统计程序的正确性。该方法通过为源代码添加标注，提醒程序员检查统计方法的前提条件。随后，一个名为StatWhy的软件工具会自动检测程序员是否正确规定了统计方法所需的前提条件。该工具基于Why3平台实现，用于验证OCaml语言编写的统计假设检验程序的正确性。我们通过多个常用假设检验程序的案例，展示了StatWhy如何帮助避免常见错误。