Spreadsheet Verificator

Introduction

Do you want to ensure the correctness of your spreadsheets? Do you need to review spreadsheets made by others? If so, Spreadsheet Verificator is your best friend!

Spreadsheet Verificator verifies all the cell values and formulas of your spreadsheet by types.
It either proves that the spreadsheet is exempt of a class of typing errors, or identifies the cell formulas that contain typing mismatches, which are clues to spreadsheet defects.
As a result, verifying and validating spreadsheets by Spreadsheet Verificator will improve their quality and prevent you from making business decisions with incorrect spreadsheets.

Elements in the Task Pane

1 button
1 result area
1 link to the support page

Must-do Before Running the Tool

unprotect manually the worksheets protected with password, if there is any

Tests

Comparison.xlsx: an artificial simple example to show a comparison of a string and a double does not lead to an obvious error (eg, #VALUE) in Excel, though such a comparison does not make any sense in reality.
Finalgradebook.xlsx: Spreadsheet Verificator will detects a typing error: "AVERAGE(Double, Double, Double, Double, Empty)", from where we could observe that the last argument of the formula does not point to the correct cell.
act3_lab23_posey.xlsx: A "Currency-String" typing error will be raised by the verificator; it reveals that the value of a cell is incorrectly entered.
Progress.xlsx: A "Double/String" typing error raised by the verificator will reveal the incomplete part of the spreadsheet.

Brief Description of our Verification

Why Should Spreadsheets Be Verified by Tools?

Spreadsheets are error-prone, because errors in spreadsheets are not blocking
Spreadsheets are carriers of important business information, data and logic
Spreadsheets can be big and complex, or made by others; they are hard to review thoroughly.

Verification by Types

Type checking is a classic, popular, and effective method to verify computer programs. It is even systematically applied to programs written in certain languages such as OCaml, C#, etc., which are thus called "strongly typed" languages. However, almost all the spreadsheet languages are "weakly typed". For example, a comparison of a string and a numeric value is permitted (returns true of false), and does not lead to any error. Even though some meaningless operations show errors such as #VALUE, they are not blocking and can be easily disregarded by users. Therefore, our approach aims at applying type checking to spreadsheet programs, to improve their quality.

Our Types

Currently, in our type system, we class cell values by the following types:

Empty
Double
Integer
Boolean
String
Date
Currency

Our Safety/Dangerous Typing Rules

We implement a set of "dangerous" typing rules in Spreadsheet Verificator. The tool verifies all the formulas of a spreadsheet, raises a typing error, if it discovers a dangerous typing rule may be matched during the calculation of the spreadsheet. In the following table, we list the dangerous typing rules that are easy to formalize. For instance, "Boolean + | - Currency | Date" means it is dangerous to add or minus a Boolean value to a Currency or a Date.

SIN \| COS \| ATAN \| ASIN (Boolean \| Date \| String)
LN \| LOG1 \| LOG10 \| SQRT \| EXP (Boolean \| Date)
-(Boolean \| Date)
+Boolean
POWER \| LOG2 (ANY, Boolean \| Date)
POWER \| LOG2 (Boolean \| Date, ANY)
Currency + \| - \| * \| / Date
Date + \| - \| * \| / Currency
Currency \| Date + \| - Boolean
Boolean + \| - Currency \| Date
Boolean \| String + \| - \| * \| / ANY
ANY + \| - \| * \| / Boolean \| String
Date * \| / ANY
ANY * \| / Date
Date < \| > \| <= \| >= \| == \| <> String \| Integer \| Double \| Boolean \| Currency
Currency < \| > \| <= \| >= \| == \| <> String \| Boolean \| Date
String < \| > \| <= \| >= \| == \| <> Boolean \| Integer \| Double \| Date \| Currency
Boolean < \| > \| <= \| >= \| == \| <> String \| Integer \| Double \| Date \| Currency
Integer \| Double < \| > \| <= \| >= \| == \| <> String \| Boolean \| Date
MIN \| MAX (Boolean \| String)
MIN \| MAX has one argument, which is array; the array contains Boolean \| String
MIN \| MAX has one argument, which is array; the array does not contain Boolean \| String; it contains Currency \| Double \| Integer and Date
MIN \| MAX has more than one argument, and there exists one Boolean \| String argument
MIN \| MAX has more than one argument; there is no Boolean \| String argument; there exists one Currency \| Double \| Integer argument and one Date argument
SUM (Boolean \| Date \| String)
SUM has one argument, which is array; the array contains Boolean \| Date elements
SUM has more than one argument, and there exists one Boolean \| Date \| String argument
AVERAGE \| MEDIAN (Boolean \| Date \| String)
AVERAGE \| MEDIAN has one argument, which is array; the array contains Boolean \| Date elements
AVERAGE \| MEDIAN has more than one argument, and there exists one Boolean \| Date \| String argument
...

Note that some typing rules may be considered dangerous by some users, but safe by others. It is not possible to make a universally absolute and exhaustive set of dangerous typing rules. If you think certain typing rules are missing in the tool, please write to us.

Advantages

Spreadsheet Verificator is fully automatic; it does not require users to provide supplementary information to be launched.
Another important advantage of our approach is its "soundness". That means we guarantee that none of the dangerous typing rules could ever be matched in any calculation of the spreadsheet. In other words, if the spreadsheet is validated by the tool, the validation applies to all the possible input cell values, as long as their type does not change. This is particularly better and more exhaustive than a manually testing approach, which cannot cover all the possible input instances.

False Alarms

As the cell property (ie, types) we reason on is more abstract and less precise than concrete cell values, verification tools like ours involves a notion of precision. In case of being not precise enough, there may be false alarms, which means what the tool raises is not a real error. For instance, the formula =IF(ABS(A1)>=0, 3, false)+5 always evaluates to 8. Whereas, an analysis solely based on types translates the formula to "=IF(ABS(A1)>=Integer, Integer, Boolean)+Integer". As it cannot evaluate the value of "ABS(A1)>=Integer", it considers the typing error "Boolean+Integer" is possible. Therefore, one target of verification tools is to improve their precision and have less false alarms.

Upcoming Features

be able to verify array formulas
verify formulas containing names
verify VBA macros in a spreadsheet