preprint · arXiv (Cornell University) · 2016

Programming Language Features for Refinement

Koenig, Jason, Leino, K. Rustan M.

Cited by 0Open access

Abstract

Algorithmic and data refinement are well studied topics that provide a mathematically rigorous approach to gradually introducing details in the implementation of software. Program refinements are performed in the context of some programming language, but mainstream languages lack features for recording the sequence of refinement steps in the program text. To experiment with the combination of refinement, automated verification, and language design, refinement features have been added to the verification-aware programming language Dafny. This paper describes those features and reflects on some initial usage thereof.

Cite this paper

APA 7

Koenig, J., & Leino, K. R. M. (2016). Programming Language Features for Refinement. arXiv (Cornell University). https://doi.org/10.48550/arxiv.1606.02022

MLA 9

Koenig, Jason, and K. Rustan M. Leino. “Programming Language Features for Refinement.” arXiv (Cornell University), 2016, https://doi.org/10.48550/arxiv.1606.02022.

Chicago

Koenig, Jason, and K. Rustan M. Leino. 2016. “Programming Language Features for Refinement.” arXiv (Cornell University). https://doi.org/10.48550/arxiv.1606.02022.

Harvard

Koenig, J. and Leino, K.R.M. (2016) ‘Programming Language Features for Refinement’, arXiv (Cornell University). Available at: https://doi.org/10.48550/arxiv.1606.02022.

BibTeX

@misc{koenig2016programming,
  title = {{Programming Language Features for Refinement}},
  author = {Koenig, Jason and Leino, K. Rustan M.},
  journal = {arXiv (Cornell University)},
  year = {2016},
  doi = {10.48550/arxiv.1606.02022}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.