Rotation of Sequences: Algorithms and Proofs
Logic in Computer Science
2015-02-06 v3
Abstract
Sequence rotation consists of a circular shift of the sequence's elements by a given number of positions. We present the four classic algorithms to rotate a sequence; the loop invariants underlying their correctness; detailed correctness proofs; and fully annotated versions for the verifiers Boogie, Dafny, and ESC/Java2. The presentation illustrates in detail both how the algorithms work and what it takes to carry out mechanized proofs of their correctness.
Keywords
Cite
@article{arxiv.1406.5453,
title = {Rotation of Sequences: Algorithms and Proofs},
author = {Carlo A. Furia},
journal= {arXiv preprint arXiv:1406.5453},
year = {2015}
}
Comments
Added verified implementations for ESC/Java2