C. A. Middelburg

C. A. Middelburg

In a previous paper, a process algebra based on ACP (Algebra of Communicating Processes) was proposed in which processes involving data can be handled by means of features originating from imperative programming. In this paper, an extension of that process algebra with probabilistic choice operators is presented that rests on the principle that probabilistic choices are always resolved before choices involved in alternative composition and parallel composition are resolved. This extension can be useful, among other things, for specifying the patterns of behaviour expressed by algorithms that are important in the area of distributed computing and verifying properties about them. Many canonical problems in that area, such as the leader election problem and the consensus problem, call for a probabilistic algorithm.

J. A. Bergstra, C. A. Middelburg

The secure hash function SHA-256 is a function on bit strings. This means that its restriction to the bit strings of any given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. We describe such instruction sequences for the restrictions to bit strings of the different possible lengths by means of uniform terms from an algebraic theory.