Programming Language Features for Refinement

Jason Koenig
(Stanford University)
K. Rustan M. Leino
(Microsoft Research)

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.

In John Derrick, Eerke Boiten and Steve Reeves: Proceedings 17th International Workshop on Refinement (Refine'15), Oslo, Norway, 22nd June 2015, Electronic Proceedings in Theoretical Computer Science 209, pp. 87–106.
Published: 4th June 2016.

ArXived at: https://dx.doi.org/10.4204/EPTCS.209.7 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org