A Single-Assignment Translation for Annotated Programs
classification
💻 cs.LO
keywords
single-assignmenttranslationannotatedprogramsadaptation-completeapproachcompanioncomplete
read the original 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].
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.