AN EXTENSIONAL TREATMENT OF LAZY DATA-FLOW DEADLOCK

In an extensional treatment of dataflow deadlock Wadge (1981) introduced an elegant nonoperational test for proving that many of Kahn's data flow message passing networks (Kahn, 1974) must be free of deadlock; a test that ''should extend to a much wider context'' in the study of program correctness. Such a context has now been provided with the introduction of partial metric spaces (Matthews, 1992). These spaces can be used to describe semantic domains such as those used in lazy data flow languages (Wadge and Ashcroft, 1985). This paper develops Wadge's ideas on establishing an extensional theory of program correctness by using partial metric spaces to give a nonoperational treatment of lazy data flow deadlock