2016/01/04 by Lourenço, Cláudio Belo, Frade, Maria João, Pinto, Jorge Sousa
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1601.00584
We present a translation of While programs annotated with loop invariants into a dynamic single-assignment language with a dedicated iterating construct. We prove that the translation is sound and complete. This is a companion report to our paper Formalizing Single-assignment Program Verification: an Adaptation-complete Approach [6].