Establishing High Confidence in Code Implementations of Algorithms using Formal Verification of Pseudocode
Abstract
Using a theorem prover to establish that a body of code correctly implements an algorithm is a task seldom undertaken because the effort required tends to be prohibitive. Direct reasoning about code in a particular programming language requires that some version of the language's semantics-e.g., axiomatic, operational, denotational-be used to determine the program correctness assertions to establish with the theorem prover. Any scheme for generating correctness assertions will be language-specific, and for languages with complex constructs, can be complex to implement and use. Direct reasoning about algorithms using a theorem prover can be not just difficult, but impossible, if the algorithms are (as is typical) specified using informal pseudocode. This paper provides high confidence in the correctness of an algorithm's implementation. The scheme uses formal pseudocode specifications, in a restricted language of while programs with (probably recursive) procedure calls, to bridge from algorithm specifications to implementations in code. Each block of formal pseudocode is verified in the theorem prover PVS by translating it into a state machine model and proving a set of state invariants. High confidence in implementation correctness is achieved by combining verification of the pseudocode with traceability arguments relating the algorithm specification to the pseudocode representation and the pseudocode representation to the actual code.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 16, 2006
- Accession Number
- ADA462080
Entities
People
- Elizabeth I. Leonard
- Myla M. Archer
Organizations
- United States Naval Research Laboratory