We are aiming at a classification of semantical models for Communicating Processes that will enable us to recommend certain models which are just detailed enough for particular applications. But before such an aim can...
详细信息
作者：
Raskovsky, Martin R.Essex University
Department Of Computing Science Oxford University Computing Laboratory Programming Research Group United Kingdom
We describe the automatic generation - from the formal denotational semantic specification - of an efficient compiler's code generation phase, producing efficient code for real machines. The method has been succes...
详细信息
A method of describing pictures is introduced. The equations, which describe the appearance of a picture, also form a purely functional program which can be used to compute the set of lines necessary to plot the pictu...
A process communicates with its environment and with other processes by syncronized output and input on named channels. The current state of a process is defined by the sequences of messages which have passed along ea...
A process communicates with its environment and with other processes by syncronized output and input on named channels. The current state of a process is defined by the sequences of messages which have passed along each of the channels, and by the sets of messages that may next be passed on each channel. A process satisfies an assertion if the assertion is at all times true of all possible states of the process. We present a calculus for proving that a process satisfies the assertion describing its intended behaviour. The following constructs are axiomatised: output; input; simple recursion; disjoint parallelism; channel renaming, connection and hiding; process chaining; nondeterminism; conditional; alternation; and mutual recursion. The calculus is illustrated by proof of a number of simple buffering protocols.
This paper argues that our recent progress in the development of a sound programming methodology should not lead us to ignore the more difficult aspects of engineering;and that in future we should pay more attention t...
详细信息
The input-output behaviour of recursive program schemes with parameters called-by-name is expressed as a non-deterministic choice between calls of recursive program schemes with parameters called-by-value, and can the...
详细信息
暂无评论