This paper presents a Hoare-style calculus for formal reasoning about
reconfiguration programs of distributed systems. Such programs create
and delete components and/or interactions (connectors) while the
system components change state according to their internal behaviour.
Our proof calculus uses a resource logic, in the spirit of Separation
Logic, to give local specifications of reconfiguration
actions. Moreover, distributed systems with an unbounded number of
components are described using inductively defined predicates. The
correctness of reconfiguration programs relies on havoc invariants,
that are assertions about the ongoing interactions in a part of the
system that is not affected by the structural change caused by the
reconfiguration. We present a proof system for such invariants in an
assume/rely-guarantee style. We illustrate the feasibility of our
approach by proving the correctness of real-life distributed systems
with reconfigurable (self-adjustable) tree architectures.