Programming Language Features for Refinement

TL;DR

This paper introduces refinement features into the Dafny programming language to better support the recording and management of refinement steps, integrating automated verification with language design.

Contribution

It presents novel language features for refinement in Dafny, enabling more rigorous and automated software development processes.

Findings

Refinement features were successfully integrated into Dafny.

Initial usage shows potential for improved verification workflows.

The approach bridges refinement techniques with programming language design.

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.