Programming Language Features for Refinement

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 record...

Full description

Saved in:
Bibliographic Details
Published in:Electronic proceedings in theoretical computer science 2016-06, Vol.209 (Proc. Refine 2015), p.87-106
Main Authors: Koenig, Jason, Leino, K. Rustan M.
Format: Article
Language:English
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2075-2180
2075-2180
DOI:10.4204/EPTCS.209.7