%0 Journal Article
%J CoRR
%D 2016
%T A Single-Assignment Translation for Annotated Programs
%A Cláudio Belo Lourenço
%A Maria João Frade
%A Jorge Sousa Pinto
%U http://arxiv.org/abs/1601.00584
%V abs/1601.00584
%X <p>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.</p>
%Z <p>n/a</p>
%> https://haslab.uminho.pt/sites/default/files/mjf/files/satranslation.pdf