Fisher–Yates shuffle

Manuel Eberl 🌐

September 30, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This work defines and proves the correctness of the Fisher–Yates algorithm for shuffling – i.e. producing a random permutation – of a list. The algorithm proceeds by traversing the list and in each step swapping the current element with a random element from the remaining list.

License

BSD License

Topics

Session Fisher_Yates

Cite

× 
@article{Fisher_Yates-AFP,
  author  = {Manuel Eberl},
  title   = {Fisher–Yates shuffle},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2016},
  note    = {\url{https://isa-afp.org/entries/Fisher_Yates.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: