gcd package:sbv

Symbolic GCD as our specification. Note that we cannot really implement the GCD function since it is not symbolically terminating. So, we instead uninterpret and axiomatize it below. NB. The concrete part of the definition is only used in calls to traceExecution and is not needed for the proof. If you don't need to call traceExecution, you can simply ignore that part and directly uninterpret. In that case, we simply use Prelude's version.

Computing GCD symbolically, and generating C code for it. This example illustrates symbolic termination related issues when programming with SBV, when the termination of a recursive algorithm crucially depends on the value of a symbolic variable. The technique we use is to statically enforce termination by using a recursion depth counter.

Proof of correctness of an imperative GCD (greatest-common divisor) algorithm, using weakest preconditions. The termination measure here illustrates the use of lexicographic ordering. Also, since symbolic version of GCD is not symbolically terminating, this is another example of using uninterpreted functions and axioms as one writes specifications for WP proofs.

The state for the sum program, parameterized over a base type a.

This call will generate the required C files. The following is the function body generated for sgcd. (We are not showing the generated header, Makefile, and the driver programs for brevity.) Note that the generated function is a constant time algorithm for GCD. It is not necessarily fastest, but it will take precisely the same amount of time for all values of x and y.

#include <stdio.h>
#include <stdlib.h>
#include <inttypes.h>
#include <stdint.h>
#include <stdbool.h>
#include "sgcd.h"

SWord8 sgcd(const SWord8 x, const SWord8 y)
{
const SWord8 s0 = x;
const SWord8 s1 = y;
const SBool  s3 = s1 == 0;
const SWord8 s4 = (s1 == 0) ? s0 : (s0 % s1);
const SWord8 s5 = s3 ? s0 : s4;
const SBool  s6 = 0 == s5;
const SWord8 s7 = (s5 == 0) ? s1 : (s1 % s5);
const SWord8 s8 = s6 ? s1 : s7;
const SBool  s9 = 0 == s8;
const SWord8 s10 = (s8 == 0) ? s5 : (s5 % s8);
const SWord8 s11 = s9 ? s5 : s10;
const SBool  s12 = 0 == s11;
const SWord8 s13 = (s11 == 0) ? s8 : (s8 % s11);
const SWord8 s14 = s12 ? s8 : s13;
const SBool  s15 = 0 == s14;
const SWord8 s16 = (s14 == 0) ? s11 : (s11 % s14);
const SWord8 s17 = s15 ? s11 : s16;
const SBool  s18 = 0 == s17;
const SWord8 s19 = (s17 == 0) ? s14 : (s14 % s17);
const SWord8 s20 = s18 ? s14 : s19;
const SBool  s21 = 0 == s20;
const SWord8 s22 = (s20 == 0) ? s17 : (s17 % s20);
const SWord8 s23 = s21 ? s17 : s22;
const SBool  s24 = 0 == s23;
const SWord8 s25 = (s23 == 0) ? s20 : (s20 % s23);
const SWord8 s26 = s24 ? s20 : s25;
const SBool  s27 = 0 == s26;
const SWord8 s28 = (s26 == 0) ? s23 : (s23 % s26);
const SWord8 s29 = s27 ? s23 : s28;
const SBool  s30 = 0 == s29;
const SWord8 s31 = (s29 == 0) ? s26 : (s26 % s29);
const SWord8 s32 = s30 ? s26 : s31;
const SBool  s33 = 0 == s32;
const SWord8 s34 = (s32 == 0) ? s29 : (s29 % s32);
const SWord8 s35 = s33 ? s29 : s34;
const SBool  s36 = 0 == s35;
const SWord8 s37 = s36 ? s32 : s35;
const SWord8 s38 = s33 ? s29 : s37;
const SWord8 s39 = s30 ? s26 : s38;
const SWord8 s40 = s27 ? s23 : s39;
const SWord8 s41 = s24 ? s20 : s40;
const SWord8 s42 = s21 ? s17 : s41;
const SWord8 s43 = s18 ? s14 : s42;
const SWord8 s44 = s15 ? s11 : s43;
const SWord8 s45 = s12 ? s8 : s44;
const SWord8 s46 = s9 ? s5 : s45;
const SWord8 s47 = s6 ? s1 : s46;
const SWord8 s48 = s3 ? s0 : s47;

return s48;
}

The symbolic GCD algorithm, over two 8-bit numbers. We define sgcd a 0 to be a for all a, which implies sgcd 0 0 = 0. Note that this is essentially Euclid's algorithm, except with a recursion depth counter. We need the depth counter since the algorithm is not symbolically terminating, as we don't have a means of determining that the second argument (b) will eventually reach 0 in a symbolic context. Hence we stop after 12 iterations. Why 12? We've empirically determined that this algorithm will recurse at most 12 times for arbitrary 8-bit numbers. Of course, this is a claim that we shall prove below.

We have:

>>> prove sgcdIsCorrect
Q.E.D.

Constraints and axioms we need to state explicitly to tell the SMT solver about our specification for GCD.

A program is the algorithm, together with its pre- and post-conditions.