A Single-Assignment Translation for Annotated Programs
Logic in Computer Science
2016-05-06 v3
Abstract
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].
Keywords
Cite
@article{arxiv.1601.00584,
title = {A Single-Assignment Translation for Annotated Programs},
author = {Cláudio Belo Lourenço and Maria João Frade and Jorge Sousa Pinto},
journal= {arXiv preprint arXiv:1601.00584},
year = {2016}
}