A weakest precondition calculus for BUnity

We present a weakest precondition calculus for belief updates in a high-level agent specification language. The weakest precondition calculus supports a deductive method which allows us to reason about important safety and leads-to properties of the semantics of agent specifications.