RSRG: Benchmarks: Adding and Multiplying Numbers

2008 May 9

In this version, the numbers are bounded computational integers, and addition is done (recursively) by repeated incrementing. Please note that all files can be opened with a simple word processor, regardless of the extensions.  Results for the rest of the benchmark (multiplication) are available and will be added as time permits.

• Concept (specification): Integer_Template
• Enhancement (specification): Adding_Capability
• Realization (implementation): Recursive_Realiz for Adding_Capability of Integer_Template
• Verification Conditions: Easy-to-read Format
• Verification Conditions: Isabelle Format
• Results: Isabelle proves all the VCs.
• Link forthcoming: Realization: Iterative_Realiz for Adding_Capability (with a bug)
• The bug is that the loop invariant is too weak. Note that this means the code is not "correct" (because it can't be verified), even though the executable portion produces correct answers.
• Link forthcoming: Verification Conditions: Easy-to-read Format
• Link forthcoming: Verification Conditions: Isabelle Format
• Results: Isabelle proves all the VCs except ... .

Murali Sitaraman and Heather Keown Harton

Last modified: Wed May 14 10:07:49 EDT 2008