带注解程序的单赋值翻译
计算机科学中的逻辑
2016-05-06 v3
摘要
我们提出一种将带有循环不变式注解的While程序翻译为具有专用迭代构造的动态单赋值语言的方法。我们证明该翻译是可靠且完备的。这是我们的论文《形式化单赋值程序验证：一种适应完备的方法》[6]的配套报告。
引用
@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}
}