several papers by Jackson and Zave [9], [21], [10], which draw a clear distinction between the environment, which is where the ultimate effects of software are expected, and the machine, the computer-driven system where software operates. Their goal is to show that the intentional relationship between the two can be defined by establishing a logical connection between the intended external behavior of the machine (described by a specification S), the relevant assumptions about environmental properties (described by a body of world knowledge W), and the desired environmental behavior (described by a set of requirements R)