A Brief Introduction to the PVS2C Code Generator
Natarajan Shankar · Kalpa publications in computing · 2018
We present a brief tutorial on the PVS2C code generator for producing C code from an applicative fragment of the PVS specification language. This fragment roughly corresponds to a self-contained functional language. The tutorial covers the generation of C code for numeric data types and associated operations, arrays, recursive data types, and higher- order operations.