Automatic generation and maintenance of correct spreadsheets

Existing spreadsheet systems allow users to change cells arbitrarily, which is a major source of spreadsheet errors. We propose a system that prevents errors in spreadsheets by restricting spreadsheet updates to only those that are logically and technically correct. The system is based on the concept of templates that describe the principal structure of the initial spreadsheet and all of its future versions. We have developed a program generator that translates a template into an initial spreadsheet together with customized update operations for changing cells and inserting/deleting rows and columns for this particular template. We have designed a type system for templates that ensures the following form of "spreadsheet maintenance safety": Update operations that are generated from a type-correct template are proved to transform the spreadsheet only according to the template and to never produce any omission, reference, or type errors. Finally, we have developed a prototype as an extension to Excel, which has been shown by a preliminary usability study to be well accepted by end users.