Titlebook: Stepwise Refinement of Distributed Systems; Models, Formalisms, J. W. Bakker,W. -P. Roever,G. Rozenberg Conference proceedings 1990 Spring

丧失

痛苦一生

Specialization in logic programming: From horn clause logic to prolog and concurrent prolog,logic component a Prolog or Concurrent Prolog program contains information about the flow of control. In Prolog we have the cut statement and a leftmost depth first search strategy, in Concurrent Prolog we have read-only variables and commits. In this paper we study the flow of control of these lang

奖牌

Analysis of discrete event coordination,model in such a way that the validity of the latter implies the validity of the former. Reductions, in that they are relative to the property to be proved, are significantly more powerful than equivalence and minimization, and are needed to reason about complex coordinating systems. Furthermore, red

ALB

Refinement and projection of relational specifications, basic constructs: . that respresent sets of states, and . that represent sets of state transitions. We present a theory of . of relational specifications. Several refinement relations between specifications are defined. To illustrate our concepts and methods, three specifications of the alternating

semiskilled

疲惫的老马

DEAF

EXULT

轻弹

Composing specifications,s part of the others‘ environments. We examine the precise distinction between a system and its environment, and provide the requisite proof rule when modules are specified with safety and liveness properties.

Gobble

Refinement calculus, part II: Parallel and reactive programs,shion. Hence the refinement calculus for sequential programs carries over to the parallel programs expressed in this framework. Refinement of reactive programs can be expressed and proved in the refinement calculus by using the methods of data refinement from the sequential refinement calculus.