  Computer programs are increasingly being deployed in partially-observable
environments. A partially observable environment is an environment whose state
is not completely visible to the program, but from which the program receives
partial observations. Developers typically deal with partial observability by
writing a state estimator that, given observations, attempts to deduce the
hidden state of the environment. In safety-critical domains, to formally verify
safety properties developers may write an environment model. The model captures
the relationship between observations and hidden states and is used to prove
the software correct.
  In this paper, we present a new methodology for writing and verifying
programs in partially observable environments. We present belief programming, a
programming methodology where developers write an environment model that the
program runtime automatically uses to perform state estimation. A belief
program dynamically updates and queries a belief state that captures the
possible states the environment could be in. To enable verification, we present
Epistemic Hoare Logic that reasons about the possible belief states of a belief
program the same way that classical Hoare logic reasons about the possible
states of a program. We develop these concepts by defining a semantics and a
program logic for a simple core language called BLIMP. In a case study, we show
how belief programming could be used to write and verify a controller for the
Mars Polar Lander in BLIMP. We present an implementation of BLIMP called CBLIMP
and evaluate it to determine the feasibility of belief programming.
