i-nth logo

Authors

Tie Cheng & Xavier Rival

Abstract

Spreadsheet languages are very commonly used, by large user bases, yet they are error prone.

However, many semantic issues and errors could be avoided by enforcing a stricter type discipline. As declaring and specifying type information would represent a prohibitive amount of work for users, we propose an abstract interpretation based static analysis for spreadsheet programs that infers type constraints over zones of spreadsheets, viewed as two-dimensional arrays.

Our abstract domain consists in a cardinal power from a numerical abstraction describing zones in a spreadsheet to an abstraction of cell values, including type properties. We formalize this abstract domain and its operators (transfer functions, join, widening and reduction) as well as a static analysis for a simplified spreadsheet language. Last, we propose a representation for abstract values and present an implementation of our analysis.

Sample

Example of inferring types over spreadsheet zones
Example of inferring types over spreadsheet zones

Our analyzer infers invariants about types of different parts of the sheet, and it also detects different sorts of type conflicts hidden in the code, which may result in strange behaviors. This example contains several errors.

Publication

2012, 19th International Conference on Static Analysis, September, pages 94-110

Full article

An abstract domain to infer types over zones in spreadsheets