Precise documentation of critical software

This experience and research based paper discusses the reasons that software cannot be trusted and then explains how the use of greatly improved documentation can make software more trustworthy. It shows how tabular expressions can be used to prepare software documents that are both precise and easily used by developers, inspectors, and testers. The paper reviews a number of "tried and true" ideas and illustrates some new refinements in the methods that resulted from recent research. It is intended both to tell developers of techniques available to them and to suggest new research areas.