An algorithm is developed for the in-situ inversion of a cyclic permutation represented in an array. The emphasis is on the quo modo rather than the quod; we are interested in finding concepts and notations for dealing more effectively with formal developments and proofs of such algorithms, rather than in this particular algorithm itself.