Analysis of pointer “rotation”
Two high-level pointer operations, rotation and slide, reduce conceptual difficulties when writing pointer programs and increase the reliability of programs. We analyze theoretically as well as empirically why these operations are more convenient and introduce a mechanically checkable notion of the safety of rotations. Several examples show that safety is a good indication of program correctness. Examples of list marking and list copying programs demonstrate the utility of these operations.