  We propose a new approach to formally describing the requirement for
statistical inference and checking whether a program uses the statistical
method appropriately. Specifically, we define belief Hoare logic (BHL) for
formalizing and reasoning about the statistical beliefs acquired via hypothesis
testing. This program logic is sound and relatively complete with respect to a
Kripke model for hypothesis tests. We demonstrate by examples that BHL is
useful for reasoning about practical issues in hypothesis testing. In our
framework, we clarify the importance of prior beliefs in acquiring statistical
beliefs through hypothesis testing, and discuss the whole picture of the
justification of statistical inference inside and outside the program logic.

Artificial Intelligence