ISO proof of permutation enumeration algorithm

[kj]

I'm looking for a proof that the following algorithm indeed enumerates
all the permutations of a sequence s.  I'll attempt to render the
algorithm in my own home-grown pseudocode (additional explanations
follow).  The important thing to note is that at every iteration
of the outer loop the algorithm obtains the next permutation by
transforming the sequence s *in place*.  Hence, as the algorithm
progresses, s "visits" each permutation of its original value.
(The first iteration just produces the original s.)

  m <-- length(s)
  n <-- 0

  while (true)

     if ( n == 0 )
        print( s )
        n <-- n+1
        continue 
     endif

     i <-- 1 
     p <-- n
     while ( i <= m and p % i == 0 )
       p <-- p / i
       i <-- i + 1
     endwhile

     if ( m < i )
       break
     endif

     j <-- m - i
     d <-- p % i 

     s[ j+1 .. m-1 ] <-- reverse( s[ j+1 .. m-1 ] )
     s[ j, d ] <-- s[ d, j ]

     print( s )
     n <-- n+1

  endwhile

Notes:

  0. <-- denotes assignment; == denotes test of equality; % denotes
     the modulus operation (e.g. 7 % 5 is equal to 2);
  1. the indexing of s is zero-based
  2. hence, since m is the length of s, its last element is s[m-1]
  3. s[ j+1 .. m-1 ] represents the sub-sequence s[j+1],...,s[m-1]
  4. the expression s[ j+1 .. m-1 ] <-- reverse s[ j+1 .. m-1 ]
     says reverse *in place* the last m-(j+1) elements of s
  5. the expression s[ j, d ] <-- s[ d, j ] just says "swap s[j]
     and s[d]"
  6. the continue and break statements in the algorithm instruct
     it to repeat and exit (respectively) the outer while-loop;

If anyone knows how a proof would go, or where I can read a proof,
please let me know.  Also, if anyone knows the name of this algorithm,
I'd also like to know it.  Many thanks in advance.

kj
-- 
NOTE: In my address everything before the first period is backwards;
and the last period, and everything after it, should be discarded.