Predicative specifications for functional programs describing communicating networks
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.
- scientific article; zbMATH DE number 512961
- A functional calculus for specification and verification of nondeterministic interactive systems
- Predicative programming Part II
- On denotational versus predicative semantics
- A functional programming approach to the specification and verification of concurrent systems
- Specification and top-down design of distributed systems
- Specification and design of shared resource arbitration
- Algebraic and functional specification of an interactive serializable database interface
- Algebraic specification of reactive systems
- Functional structures in networks. AMLn -- a language for model driven development of telecom systems.
- scientific article; zbMATH DE number 1497775 (Why is no real title available?)
- A functional calculus for specification and verification of nondeterministic interactive systems
- A functional programming approach to the specification and verification of concurrent systems
- Algebraic specification of concurrent systems
This page was built for publication: Predicative specifications for functional programs describing communicating networks
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q579917)
