Predicative specifications for functional programs describing communicating networks
type: Item
instance of: scholarly article
title: Predicative specifications for functional programs describing communicating networks
zbMATH Open document ID: 0625.68007
DOI: 10.1016/0020-0190(87)90227-4
author: Manfred Broy
published in: Information Processing Letters
publication date: 1987-01-01T00:00:00Z
review text: For the design and verification of programs by formal rules two approaches may be distinguished basically: the verification approach where initially the programming is done regardless of formal rules and later proved correct (if possible) against a given specification and the translation approach where the construction of the program is done along a calculus and therefore includes a constructive correctness proof. Following recent ideas of C. A. R. Hoare and E. C. R. Hehner both approaches can be combined into one by considering programs as a particular notation for predicates. This concept of predicative specifications is applied to an applicative language for describing communicating systems. An example of a simple predicative specification language with an integrated functional language is given. It is powerful enough to specify and write programs representing finite and infinite nondeterministic data flow networks. The language is formally defined in terms of predicative specifications and a few simple examples are given. By doing so one of the key-questions is the treatment of nondeterminism. It is resolved in a simple way: a recursive declaration of a nondeterministic function can be rather seen as an equational specification of a predicate on functions. Then the set of functions that fulfil this predicate is taken as the meaning of the recursive declaration. A language framework includes applicative programs with (recursive) declarations and nondeterministic choice, as well as streams and mutually recursive declarations of streams which represent networks of communicating systems. The predicative language for the specification in particular includes predicates on functions. The translation of programs into formulas of predicate calculus provides a basis for program specification, program verification and program development by transformation.
Mathematics Subject Classification ID: 68N01
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 4016166
zbMATH Keywords: functional programming
zbMATH Keywords: predicative specifications
zbMATH Keywords: communicating systems
zbMATH Keywords: nondeterminism
MaRDI profile type: Publication
full work available at URL: 0020-0190(87)90227-4
OpenAlex ID: W1967501773
cites work: Q3677156
cites work: First-order dynamic logic
cites work: Predicative programming Part I
cites work: Q5688938
cites work: Q3906397
description: scientific article; zbMATH DE number 4016166