2018/08/27 by James Hoey, Irek Ulidowski, Shoji Yuen
Computer Science · #cs.PL
paper · pdf · doi:10.4204/eptcs.276.7
published as EPTCS 276, 2018, pp. 69-86 · In Proceedings EXPRESS/SOS 2018, arXiv:1808.08071
arxiv created 2018/08/27 · arxiv updated 2018/08/28
We show how to reverse a while language extended with blocks, local variables, procedures and the interleaving parallel composition. Annotation is defined along with a set of operational semantics capable of storing necessary reversal information, and identifiers are introduced to capture the interleaving order of an execution. Inversion is defined with a set of operational semantics that use saved information to undo an execution. We prove that annotation does not alter the behaviour of the original program, and that inversion correctly restores the initial program state.