RSRG: Benchmarks

Adding and Multiplying Numbers

2008 August 28

In this version of the benchmark, the numbers are natural numbers; addition is done iteratively by repeated incrementing, and multiplication is done recursively using the separately verified addition operation.

The VC generator is doing a few generic logical simplifications that are not specific to any particular mathematical theory, but rather have been chosen based on knowledge of how the VCs are generated and hence their logical structure. In other words, the VC generator knows that certain specific theory-independent simplifications are most likely to be possible and valuable, and it does these -- leaving everything else to the back-end prover.

• Contract: UnboundedNaturalFacility
• Contract: UnboundedNaturalAdd
• Realization: Iterative for UnboundedNaturalAdd
• Symbolic Tracing Table
• Verification Conditions: Human-Readable Format
• Verification Conditions: Isabelle Format
• Results: Isabelle proves all the VCs automatically within a total of about 1 second. (Hardware: Xeon 2.8 GHz Linux server, 8 GB RAM. Software: Isabelle2008.)
• Verification Conditions: SplitDecision XML Format
• Results: SplitDecision proves all the VCs automatically within a total of about 0.6 seconds. (Hardware: MacBook Pro with Mac OS X 10.5.4, 2.2 GHz Intel Core Duo, 2 GB RAM. Software: SplitDecision is written in Resolve/C++, compiled with gcc.)
• Realization: Iterative for UnboundedNaturalAdd (with a bug)
• The bug is that the loop invariant is too weak. Note that this means the code is not "correct", even though under the usual operational semantics for this program the executable portion produces the same answers as the verified version above.
• Symbolic Tracing Table
• Verification Conditions: Human-Readable Format
• Verification Conditions: Isabelle Format
• Results: Isabelle proves all the VCs automatically except the VC called "lemma 4", which arises from the need to show that the precondition for Decrement is satisfied; and the VC called "lemma 9", which arises from the need to show that m is restored to its incoming value. Isabelle refutes these VCs.
• Verification Conditions: SplitDecision XML Format
• Results: SplitDecision proves all the VCs automatically except the VCs called "lemma 4" and "lemma 9"; it does not refute either one.
• Realization: Iterative for UnboundedNaturalAdd (with a different bug)
• The bug this time is that the call to Decrement is missing at the end of the loop.
• Symbolic Tracing Table
• Verification Conditions: Human-Readable Format
• Verification Conditions: Isabelle Format
• Results: Isabelle proves all the VCs automatically except the VCs called "lemma 5", "lemma 6", and "lemma 9". These VCs arise from the need to show the first two clauses of the loop invariant and loop termination, respectively. Isabelle refutes these VCs.
• Verification Conditions: SplitDecision XML Format
• Results: SplitDecision proves all the VCs automatically except the VCs called "lemma 5", "lemma 6", and "lemma 9"; it does not refute any of these.
• Contract: UnboundedNaturalMultiply
• Realization: Recursive for UnboundedNaturalMultiply
• Symbolic Tracing Table
• Verification Conditions: Human-Readable Format
• Verification Conditions: Isabelle Format
• Results: Isabelle proves all the VCs automatically except the VC called "lemma 8". It proves this with the additional hint to use distributivity.
• Verification Conditions: SplitDecision XML Format
• Results: SplitDecision proves all the VCs automatically except the VCs called "lemma 8" and "lemma 9".
• Realization: Recursive for UnboundedNaturalMultiply (with a bug)
• The bug is that the base case, m = 0, is not accounted for in the code.
• Symbolic Tracing Table
• Verification Conditions: Human-Readable Format
• Verification Conditions: Isabelle Format
• Results: Isabelle proves all the VCs automatically except the VCs called "lemma 7" and "lemma 9". These VCs arise from the need to show that the ensures clause of Multiply holds at the end of the code: the former for the path when m > 1 upon entry (i.e., both "if" conditions hold; this, as above, requires distributivity), the latter for the path when m = 0 upon entry. Isabelle refutes the latter VC.
• Verification Conditions: SplitDecision XML Format
• Results: SplitDecision proves all the VCs automatically except the VCs called "lemma 7", "lemma 8", and "lemma 9". For "lemma 7" and "lemma 8", the issue is the same as for the correct version of the code. The VC called "lemma 9" is false; SplitDecision simplifies it but does not refute it.
• Realization: Recursive for UnboundedNaturalMultiply (with a different bug)
• The bug this time is that the call to Increment is missing just after the recursive call to Multiply.
• Symbolic Tracing Table
• Verification Conditions: Human-Readable Format
• Verification Conditions: Isabelle Format
• Results: Isabelle proves all the VCs automatically except the VCs called "lemma 5" and "lemma 8". These VCs arise from the need to show that m is restored, and that the ensures clause holds, for the path when m > 1 upon entry. Isabelle refutes both these VCs.
• Verification Conditions: SplitDecision XML Format
• Results: SplitDecision proves all the VCs automatically except the VCs called "lemma 5", "lemma 8", and "lemma 9". For "lemma 9", the issue is the same as for the correct version of the code. SplitDecision simplifies all of these VCs, but does not refute "lemma 5" or "lemma 8".