Showing 1–1 of 1 results for author: Frade, M J

A Single-Assignment Translation for Annotated Programs

Authors: Cláudio Belo Lourenço, Maria João Frade, Jorge Sousa Pinto

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]. 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]. △ Less

Submitted 5 May, 2016; v1 submitted 4 January, 2016; originally announced January 2016.