Adding and Multiplying Numbers
Aug. 17, 2010 – 6 years, 8 months ago, by eifler
Verify an operation that adds two numbers by repeated incrementing. Verify an operation that multiplies two numbers by repeated addition, using the first operation to do the addition. Make one algorithm iterative, the other recursive.
Addition is straightforward. It is a single operation and involves a single numeric type: either integers or natural numbers, which may be a built-in type in the programming language or a user-defined abstract data type (ADT). It also involves 5 simple specifications, and presumably results in VCs from a decidable mathematical theory (Presburger arithmetic). Multiplication explicitly adds the requirement for modularity for a program unit that is a single operation, i.e., procedural or functional abstraction, and enough richness that the underlying mathematics is undecidable. Since one operation involves iteration and the other recursion, loop invariants and
termination both become concerns. There are alternative algorithms for multiplication based on addition, e.g., the Egyptian algorithm as well as the more obvious and familiar ones. All the standard procedural programming constructs are likely to arise in these two pieces of code.
Variations: Other operations on integers or natural numbers, e.g., computing powers and roots, involve similar issues and should illustrate similar verification capabilities. The programming type used for numbers may or may not be bounded. Numerical problems of this kind that involve floating point numbers are very interesting as well, raising difficult issues about how to specify their behavior that do not arise with either bounded or unbounded integers or natural numbers.
The paper from which this benchmark is taken was published in may 2008 by various authors from Clemson University, Clemson and the Ohio State University, Columbus. It contains some more benchmarks which are also included on this site.
The solution is recursive and uses a VC generator under development at Clemson; the VCs are proved using the automated proof assistant Isabelle. The solution uses a dialect of the RESOLVE language.
The specification and implementation of the Add_to operation are given with access to a specification of an Integer type and operations. Parameter modes, only updates and evaluates in this code, are specification constructs. The updates mode indicates the parameter may be modified in any way permitted by the ensures clause. The evaluates mode allows an expression to be passed as the corresponding argument, i.e., it indicates a “value” parameter. In an ensures clause, the prefix # for a formal parameter denotes the incoming value. Recursive code is annotated with a progress metric using the keyword decreasing.
Operation Add_to(updates i:Integer; evaluates j:Integer); requires min_int <= i + j and i + j <= max_int and j >= 0; ensures i = #i + j;
Procedure Add_to(updates i:Integer; evaluates j:Integer); decreasing |j|; Var z: Integer; If (not Is_Zero(j)) then Increment (i); Decrement (j); Add_to (i, j); end; end Add_to;
In RESOLVE, all types (including those built-in to most languages) are specified, used, and verified in a uniform way. Integer is specified in Integer_Template shown below, where Z denotes mathematical integers; this is defined in a mathematical module Integer_Theory (not shown) along with mathematical notations such as 0, + , and -. This specification defines two constants min_int and max_int. Every Integer variable is constrained to be within these bounds, and is initially 0.
Concept Integer_Template; uses Integer_Theory, Std_Boolean_Fac; Defines min_int: Z; Defines max_int: Z; Constraint min_int <= 0 and 0 < max_int; Type Family Integer is modeled by Z; exemplar i; constraint min_int <= i and i <= max_int; initialization ensures i = 0; Operation Is_Zero(evaluates i: Integer): Boolean; ensures Is_Zero = ( i = 0 ); Operation Increment(updates i: Integer); requires i + 1 <= max_int; ensures i = #i + 1; Operation Decrement(updates i: Integer); requires min_int <= i - 1; ensures i = #i - 1; … end Integer_Template;
Interactivity, effort needed
How to reproduce
VCs are generated using a tool that implements the proof rules. Briefly, there is a VC for each state in the program where the next statement involves establishing a precondition for the next operation, a loop invariant or progress metric, or the postcondition for the operation being verified.
The VCs as well as references to the tool can be found in the paper from which the benchmark and the solution were taken.
Isabelle-friendly versions of the VCs are generated to provide proofs. Proofs of all VCs are completed automatically by Isabelle with “apply force”.
Timo Eifler email@example.com