zbMATH — the first resource for mathematics

Examples
Geometry Search for the term Geometry in any field. Queries are case-independent.
Funct* Wildcard queries are specified by * (e.g. functions, functorial, etc.). Otherwise the search is exact.
"Topological group" Phrases (multi-words) should be set in "straight quotation marks".
au: Bourbaki & ti: Algebra Search for author and title. The and-operator & is default and can be omitted.
Chebyshev | Tschebyscheff The or-operator | allows to search for Chebyshev or Tschebyscheff.
"Quasi* map*" py: 1989 The resulting documents have publication year 1989.
so: Eur* J* Mat* Soc* cc: 14 Search for publications in a particular source with a Mathematics Subject Classification code (cc) in 14.
"Partial diff* eq*" ! elliptic The not-operator ! eliminates all results containing the word elliptic.
dt: b & au: Hilbert The document type is set to books; alternatively: j for journal articles, a for book articles.
py: 2000-2015 cc: (94A | 11T) Number ranges are accepted. Terms can be grouped within (parentheses).
la: chinese Find documents in a given language. ISO 639-1 language codes can also be used.

Operators
a & b logic and
a | b logic or
!ab logic not
abc* right wildcard
"ab c" phrase
(ab c) parentheses
Fields
any anywhere an internal document identifier
au author, editor ai internal author identifier
ti title la language
so source ab review, abstract
py publication year rv reviewer
cc MSC code ut uncontrolled term
dt document type (j: journal article; b: book; a: book article)
An extensional treatment of lazy data flow deadlock. (English) Zbl 0872.68110
Summary: In an extensional treatment of dataflow deadlock, {\it W. W. Wadge} [Theor. Comput. Sci. 13, 3-15 (1981; Zbl 0441.68017)]introduced an elegant nonoperational test for proving that many of Kahn’s data flow message passing networks [{\it G. Kahn}, Inform. Processing 74, Proc. IFIP Congr. 74, Stockholm, 471-475 (1974; Zbl 0299.68007)]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 [{\it S. G. Matthews}, Ann. N. Y. Sci. 728, 183-197 (1994)]. These spaces can be used to describe semantic domains such as those used in lazy data flow languages [{\it W. W. Wadge} and {\it E. A. Ashcroft}, Lucid, the dataflow programming language (A. P. I. C. Studies in Data Processing, Vol 22, (1985; Zbl 0564.68002)]. 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.

MSC:
68Q60Specification and verification of programs
68Q55Semantics
54E35Metric spaces, metrizability
WorldCat.org
Full Text: DOI
References:
[1] Faustini, A. A.: An operational semantics for pure dataflow, ICALP82. Lecture notes in mathematics 140, 212-224 (1982)
[2] Friedman, D. P.; Wise, D. S.: CONS should not evaluate its arguments. Automata languages and programming (1976) · Zbl 0461.68023
[3] Hoare, C. A. R.: An axiomatic basis for computer programming. Comm. ACM 12, 576-583 (1969) · Zbl 0179.23105
[4] Hovsepian, F.: A metalogical analysis of vagueness: an exploratory study into the geometry of logic. Doctoral thesis (1993)
[5] Kahn, G.: The semantics of a simple language for parallel processing. Proc. IFIP cong., 471-475 (1974) · Zbl 0299.68007
[6] Kuratowski, K.: Topologie. 1 (1958) · Zbl 0078.14603
[7] Jones, C. B.: Systematic software development. (1986) · Zbl 0584.68008
[8] Matthews, S. G.: Partial metric topology. Annals of the New York Academy of science 728, 183-197 (1994)
[9] Sutherland, W. A.: Inhtroduction to metric and topological spaces. (1975) · Zbl 0304.54002
[10] Wadge, W. W.: An extensional treatment of dataflow deadlock. Theoret. comput. Sci. 13, No. 1, 3-15 (1981) · Zbl 0441.68017
[11] Wadge, W. W.; Ashcroft, E. A.: Lucid, the dataflow programming language. APIC studies in data processing no. 22 (1985) · Zbl 0564.68002