Specifications via Realizability (CLASE 2005)
With Chris Stone.
Abstract:
We present a system, called RZ, for automatic generation of program specifications from mathematical theories. We translate mathematical theories to specifications by computing their realizability interpretations in the ML language augmented with assertions (as comments). While the system is best suited for descriptions of those data structures that can be easily described in mathematical language (e.g., finitely presented groups, real arithmetic, graphs, etc.), it also elucidates the relationship between data structures and constructive mathematics.
Presented at:
Constructive Logic for Automated Software Engineering (CLASE), Satellite event of ETAPS 2005, Edinburgh, 9th April 2005
Download paper:
rz.pdf,
rz.ps.gz
Download slides:
rz-slides.pdf
