Verification of a Rust Implementation of Knuth’s Dancing Links using ACL2: Dancing Links

Author: (1) David S. Hardin, Cedar Rapids, IA USA david.s.hardin@gmail.com. Table of Links Abstract and Introduction Dancing Links The Rust Programming Language RAC: Hardware/Software Co-Assurance at Scale Rust and RAR Dancing Links in Rust Related Work Conclusion, Acknowledgments, and References 2 Dancing Links The concept behind Dancing Links is quite simple: when a given element Y of a list is removed in an exact cover algorithm, it is very likely that this same element will later be restored. Thus, rather than “zero out” the ‘previous’ and ‘next’ links associated with element Y, as good programming hygiene would normally dictate, in Dancing Links, the programmer leaves the link values in place for the removed element. The Dancing Links remove operator thus deletes element Y from the list, setting the ’next’ element of the preceding element X to the following element Z, and setting the ’previous’ element of Z to a link to X, but not touching the ’next’ and ’previous’ links of the removed element Y. Later on, if Y needs to be restored, it is simply hooked back in to the list using a simple restore operator. In Knuth’s words, if one monitors the list links as the DLX algorithm proceeds, the links appear to ‘dance’, hence the name. Knuth’s Dancing Links functionality is summarized in Fig. 1. This paper is available on arxiv under CC 4.0 license. Author: (1) David S. Hardin, Cedar Rapids, IA USA david.s.hardin@gmail.com. Author: Author: (1) David S. Hardin, Cedar Rapids, IA USA david.s.hardin@gmail.com. Table of Links Abstract and Introduction Dancing Links The Rust Programming Language RAC: Hardware/Software Co-Assurance at Scale Rust and RAR Dancing Links in Rust Related Work Conclusion, Acknowledgments, and References Abstract and Introduction Abstract and Introduction Dancing Links Dancing Links The Rust Programming Language The Rust Programming Language RAC: Hardware/Software Co-Assurance at Scale RAC: Hardware/Software Co-Assurance at Scale Rust and RAR Rust and RAR Dancing Links in Rust Dancing Links in Rust Related Work Related Work Conclusion, Acknowledgments, and References Conclusion, Acknowledgments, and References 2 Dancing Links The concept behind Dancing Links is quite simple: when a given element Y of a list is removed in an exact cover algorithm, it is very likely that this same element will later be restored. Thus, rather than “zero out” the ‘previous’ and ‘next’ links associated with element Y, as good programming hygiene would normally dictate, in Dancing Links, the programmer leaves the link values in place for the removed element. The Dancing Links remove operator thus deletes element Y from the list, setting the ’next’ element of the preceding element X to the following element Z, and setting the ’previous’ element of Z to a link to X, but not touching the ’next’ and ’previous’ links of the removed element Y. Later on, if Y needs to be restored, it is simply hooked back in to the list using a simple restore operator. In Knuth’s words, if one monitors the list links as the DLX algorithm proceeds, the links appear to ‘dance’, hence the name. Knuth’s Dancing Links functionality is summarized in Fig. 1. This paper is available on arxiv under CC 4.0 license. This paper is available on arxiv under CC 4.0 license. available on arxiv

Verification of a Rust Implementation of Knuth’s Dancing Links using ACL2: Dancing Links

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

Untitled Story

Assessing the Security of GitHub Copilot Generated Code: A Targeted Replication Study

Verification of a Rust Implementation of Knuth’s Dancing Links Using ACL2: Related Work

Rust Implementation of Knuth's Dancing Links: The Rust Programming Language

Rust Implementation of Knuth's Dancing Links: Conclusion, Acknowledgments, and References

Rust Implementation of Knuth's Dancing Links: RAC: Hardware/Software Co-Assurance at Scale

Assessing the Security of GitHub Copilot Generated Code: A Targeted Replication Study

Verification of a Rust Implementation of Knuth’s Dancing Links Using ACL2: Related Work

Rust Implementation of Knuth's Dancing Links: The Rust Programming Language

Rust Implementation of Knuth's Dancing Links: Conclusion, Acknowledgments, and References

Rust Implementation of Knuth's Dancing Links: RAC: Hardware/Software Co-Assurance at Scale

Light-Mode

Classic

Newspaper

Dark-Mode

Neon Noir

Minty

HN StartUps