Programming Language Features for Refinement
This work tackles the problem of integrating refinement steps into programming languages for software developers, but it appears incremental as it builds on existing refinement and verification concepts.
The paper addresses the lack of features in mainstream programming languages for recording refinement steps in program text by adding refinement features to Dafny, a verification-aware language, and describes these features along with initial usage reflections.
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.