Proving Reachability in B using Substitution Refinement

This paper proposes an approach to prove reachability properties of the form using substitution refinement in classical B. Such properties denote that there exists an execution path for each state satisfying ψ to a state satisfying ϕ. These properties frequently occur in security policies and information systems. We show how to use Morganʼs specification statement to represent a property and refinement laws to prove it. The idea is to construct by stepwise refinement a program whose elementary statements are operation calls. Thus, the execution of such a program provides an execution satisfying . Proof obligations are represented using assertions (ASSERTIONS clause of B) and can be discharged using Atelier B.