Program verification in functional programming systems

Functional programming systems provide a number of features which facilitate program verification. Such verification may be observed to rest directly upon the theoretical foundations of computing and simultaneously to exhibit a close relation to the programs being verified. In order to demonstrate these aspects of functional systems, two functions, MIN and SORT, are defined on a parameterized type consisting of sequences to elements from some ordered type. Theorems showing that MIN and SORT terminate and return the correct values are stated and proved. Similar results are derived for a function to perform a binary search on an ordered sequence. Finally, conditions similar to Dijkstra’s weakest preconditions are given which allow the simultaneous synthesis and verification of certain programs from program specifications. A function to find the greatest common division of two integers is derived and verified.

Name thesis:degree_name

M.S.

Level thesis:degree_level

masters

Discipline thesis:degree_discipline

Computer Science and Applications

Department dc:contributor.department

Computer Science and Applications

Grantor dc:publisher

Virginia Polytechnic Institute and State University

Year dc:date.issued

1983

Author dc:creator

• Silver, James L.

Statement dc:rights

• In Copyright

Licence dc:rights.uri

• http://rightsstatements.org/vocab/InC/1.0/

Language dc:language.iso

en

Handle dc:identifier.uri

http://hdl.handle.net/10919/106016

OAI identifier oai:identifier

oai:vtechworks.lib.vt.edu:10919/106016