用于科学探究软件验证的精化类型契约

我们的科学知识日益建立在软件输出之上。定义数据分析流程和计算模型的用户代码对自然科学与社会科学研究至关重要，但如何确保此类代码的正确性却鲜有定论。这类代码的结构及其构建所采用的开发过程，限制了传统测试方法的效用。形式化软件验证方法在确保代码正确性方面已取得巨大成功，但通常所需的专业训练、开发时间与资金投入，超出了自然科学与社会科学领域所能提供的条件。在此，我们提出一个 Python 库，它利用轻量级形式化方法提供正确性保证，而无需专业知识或大量时间投入。我们的包使用精化类型对函数入口与出口条件契约进行运行时验证，允许在契约内检查超性质，并提供自动化测试用例生成以补充在线检查。我们与一个中等规模（约 3000 行代码）的软件包协同开发了该工具，该软件包用于模拟认知 neuroscience 中的决策过程。除帮助我们在开发周期早期定位琐碎缺陷外，该工具还能定位四个可能难以用传统测试方法发现的缺陷，并且能在不含契约或精化类型标注的用户代码中找出缺陷。这展示了形式化方法如何用于验证难以用主流方法测试的科学软件的正确性。