通过类型进行验证
为什么应该用工具验证电子表格？
电子表格的正确性是一个严肃的问题，应该借助自动化工具来处理。原因有几个：
- 电子表格容易出错
- 电子表格是重要商业信息、数据和逻辑的载体
- 电子表格可能大且复杂，或者是其他人创建的，难以彻底审查。
通过类型进行验证
类型检查是验证计算机程序的经典、流行和有效的方法。它甚至被系统地应用于某些语言编写的程序，比如OCaml、C#等，这些语言因此被称为"强类型"语言。然而，几乎所有的电子表格语言都是"弱类型"的。例如，允许字符串和数字值的比较（返回 True 或 False），并不会导致任何错误。尽管一些无意义的操作会显示错误，如#VALUE，但这些错误并不会阻塞，用户可以很容易地忽略。因此，我们的方法旨在将类型检查应用于电子表格程序，以提高其质量。
类型
在我们当前的类型系统中，我们按照以下类型对单元格值进行分类：
| 类型 | 描述 |
|---|---|
| 空 | 一个空单元格 |
| 双精度 | 例如，1,2，120%，1,25236E+10 |
| 整数 | 例如，0，-1，100 |
| 布尔值 | TRUE 和 FALSE 的类型 |
| 字符串 | 例如，abc，"abc"，"123"， (一个空格)，"" (两个双引号) |
| 日期 | 例如，11/08/2019，14 mars 2012，14/3/12 1:30 PM |
| 货币 | 例如，$1 234,10，-€1 234,10 |
| 任意 | 一个全局类型，表示 任何 值和类型 |
危险的类型规则
我们在电子表格验证器中实现了一套危险的类型规则。该工具验证电子表格的所有公式，如果发现在电子表格的计算过程中可能匹配到危险的类型规则，就会抛出一个类型错误。在下表中，我们列出了我们的一部分危险类型规则。例如，Boolean + | - Currency | Date 意味着将布尔值加到货币或日期上是危险的。需要注意的是，一些类型规则可能被一些用户视为危险，但被其他用户视为安全。创建一套普遍绝对和详尽的危险类型规则是不可能的。如果你认为该工具中缺少某些类型规则，请联系我们。
| 基本算术规则 |
|---|
| -(布尔值 | 日期) |
| +布尔值 |
| 货币 + | - | * | / 日期 |
| 日期 + | - | * | / 货币 |
| 货币 | 日期 + | - 布尔值 |
| 布尔值 + | - 货币 | 日期 |
| 布尔值 | 字符串 + | - | * | / 任意 |
| 任意 + | - | * | / 布尔值 | 字符串 |
| 日期 * | / 任意 |
| 任意 * | / 日期 |
| 关系操作规则 |
|---|
| 日期 < | > | <= | >= | == | <> 字符串 | 整数 | 双精度 | 布尔值 | 货币 |
| 货币 < | > | <= | >= | == | <> 字符串 | 布尔值 | 日期 |
| 字符串 < | > | <= | >= | == | <> 布尔值 | 整数 | 双精度 | 日期 | 货币 |
| 布尔值 < | > | <= | >= | == | <> 字符串 | 整数 | 双精度 | 日期 | 货币 |
| 整数 | 双精度 < | > | <= | >= | == | <> 字符串 | 布尔值 | 日期 |
| 算术规则 |
|---|
| SIN | COS | ATAN | ASIN (布尔值 | 日期 | 字符串) |
| LN | LOG1 | LOG10 | SQRT | EXP (布尔值 | 日期) |
| POWER | LOG2 (任意, 布尔值 | 日期) |
| POWER | LOG2 (布尔值 | 日期, 任意) |
| MIN, MAX 规则 |
|---|
| MIN | MAX (布尔值 | 字符串) |
| MIN | MAX (..., 布尔值 | 字符串, ...) |
| MIN | MAX (..., 货币 | 双精度 | 整数, ..., 日期, ...) |
| MIN | MAX ({...; 布尔值 | 字符串; ...}) |
| MIN | MAX ({...; 货币 | 双精度 | 整数; ...; 日期; ...}) |
| SUM, AVERAGE, MEDIAN 规则 |
|---|
| SUM | AVERAGE | MEDIAN (布尔值 | 日期 | 字符串) |
| SUM | AVERAGE | MEDIAN ({...; 布尔值 | 日期; ...}) |
| SUM | AVERAGE | MEDIAN (..., 布尔值 | 日期 | 字符串, ...) |
优势
虽然已有其他现有的工具和方法用于校验电子表格，我们的电子表格验证器有几个优点：
- 电子表格验证器是全自动的；启动时不需要用户提供补充信息。
- 它是可靠的。这意味着我们保证电子表格的任何计算中都不会匹配到危险的类型规则。换句话说，如果电子表格通过了工具的验证，那么这个验证适用于所有可能的输入单元格值，只要它们的类型不变。这明显优于手动测试方法，因为手动测试无法覆盖所有可能的输入实例。
错误警告
由于我们推理的单元格属性（即类型）比具体的单元格值更抽象、不够精确，像我们的验证工具可能涉及到精度的概念。如果精度不够，可能会有错误警告，也就是说工具提出的可能不是真正的错误。例如，公式=IF(ABS(A1)>=0, 3, false)+5始终评估为8。然而，仅基于类型的分析将公式翻译为=IF(ABS(A1)>=整数, 整数, 布尔值)+整数。由于它无法评估ABS(A1)>=整数的值，它认为可能存在布尔值+整数的类型错误。因此，改进验证工具的一个方向是提高其精度，减少错误警告。