Specifications via Realizability

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.

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Andrej Bauer, Christopher A. Stone
• Keywords: Automatic Generation, Data Structures, ENTCS 2006, Mathematical Theories