A subrecursive programming language for increased verifiability
Celia Schahczenski · University of Florida Digital Collections (University of Florida) · 1991
Removing gotos from computer languages resulted in more understandable, maintainable and verifiable code. Restricting recursion to primitive recursion in computer languages such as PASCAL has similar results. This dissertation developes a highly structured programming language where recursion is limited to primitive recursion. Programs in the language compute exactly the class of primitive recursive functions. A Hoare verification system is developed for this language. It is proved that this system is sound and complete.