  The rely/guarantee approach of Jones extends Hoare logic with rely and
guarantee conditions in order to allow compositional reasoning about
shared-variable concurrent programs. This paper focuses on localisation in the
context of rely/guarantee concurrency in order to support local variables.
Because we allow the body of a local variable block to contain component
processes that run in parallel, the approach needs to allow variables local to
a block to become shared variables of its component parallel processes. To
support the mechanisation of the rely/guarantee approach, we have developed a
synchronous concurrent refinement algebra. Its foundation consists of a small
set of primitive commands plus a small set of primitive operators from which
all remaining constructs are defined. To support local variables we add a
primitive localisation operator to our algebra that is used to define local
variable blocks. From this we can prove properties of localisation, including
its interaction with rely and guarantee conditions.
