Preprints of IIS SB RAS, 2007

The present paper describes a distributed systems specification language Dynamic-REAL (dREAL) which extends the language Basic-REAL developed previously by dynamic constructs for generating and removing process instances. The dREAL language includes sublanguages of executable and logic specifications. Syntax and formal semantics of the dREAL language are represented in this paper. As an example, a protocol for control of a booking terminals net is considered.

The work presents the technology of communication protocol specification. Several communication protocols are considered for the following aspects of communication: blocked or non-blocked receiving/sending, reliable or unreliable communication. This paper can be considered as an introduction to problems of communication protocols.

Some communication and data transfer patterns are described. The following communication protocol components are defined: nodes, channels, messages, input and output streams, events, timers, etc. Techniques of reliable transfer over unreliable channels such as retransmission, check summing, reception of acknowledgment, etc. are described. Additional properties of protocol specifications set are given. They are correctness, safety and liveness properties. They are usually expressed in some language of temporal logic.

The calculus of computable predicates is a mathematical model of programs whose specification is a predicate. A program on the calculus language is the closed set of recursive definitions of predicates. The specification of each defined predicate consists of the precondition and postcondition. Program correctness definition is considered as the concretization of the general law of the correspondence between a program and its specification. Two rule systems of program correctness proof are introduced. In first rule system, the postcondition is proved from the right part of the predicate definition. In the second rule system, for single-valued predicates, the right part is derived from the precondition and postcondition.

The calculus of computable predicates is defined by a collection of basic predicates and the following six computable formulas: superposition, alteration, parallel composition, predicate generation, predicate application, and array constructor. The collection of basic predicates defines a data type system. The calculus is a mathematical model of the class of programs whose specification may be written as a formula of the higher-order predicate calculus. The calculus of computable predicates may be used to construct pure functional programming languages.