Figure: PIN change in Hoare style