Clarifying Assumptions

The correctness of a program can only be judged with respect to a specification; clarifying and recording the assumptions about the context in which a program is to be used is a crucial part of such a specification. Programs that either employ concurrent threads or execute concurrently in a changing environment experience interference; recording assumptions about interference needs something more expressive than pre/post condition specifications. This chapter evaluates the effectiveness of rely-guarantee conditions for documenting tolerable and induced interference. An important message is that it is sometimes easier and clearer to begin by studying an overall system rather than seeking to describe details of low-level internal devices (which might be viewed as “implementation patterns”).