End-user assertions : propagating their implications
Jay W. Summet · 2001
interpretation is commonly used as a program analysis tool to provide optimization information at compile time, and not to enhance programmer understanding. Many programmers might not find information such as the strictness or mode of parameters to be useful for program comprehension, testing or debugging tasks. The method of propagating assertions outlined here is not intended to improve execution speed, but to improve (end-user) programmer understanding, and program correctness. By involving the user in the specification of the initial assertions, we hope to derive information that is useful to the user, as opposed to the computer.