Predicative specifications for functional programs describing communicating networks (Q579917): Difference between revisions

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.