Titlebook: Mathematical Methods in Program Development; Manfred Broy,Birgit Schieder Conference proceedings 1997 Springer-Verlag Berlin Heidelberg 19

食料

Cursory

不确定

骇人

The transitive closure of a wellfounded relation (EWD1241)Transitive closures can be defined in many ways, but today we define the nonreflexive transitive closure . of a relation r as the strongest 5 satisfying

OREX

A kind of converse of Leibniz’s Principle (EWD1245)We owe to Gottfried W. Leibniz the principle that is informally known as “substituting equals for equals” and is formally expressed by ., which we can also read as “function application is equality-preserving”. This note proves the . Besides the two constant relations, equality is the . relation preserved by function application.

善辩

你敢命令

Complete DAGs (EWD1204) which the edges may be directed. (As by-product of his considerations he finds, for instance, that “any non-cyclic ascription of directions to any five of the edges can be non-cyclically extended to the sixth edge.”) Here is a little bit of related theory.

osteoclasts

命令变成大炮

On a Method for the Formal Design of Multiprograms (AvG140/WF231)ency. In our first and simple example we derive a protocol for the problem of Concurrent Vector Writing, and in our second and more tricky example we design a distributed algorithm for the problem of Liberal Phase Synchronization.

辞职

Specification and Design of a Transmission Protocol by Successive Refinements Using B1less fashion by . its intended behavior on ., all other steps being just void: in other words, time does not exist yet and, of course, no distribution can take place between the various phases of the protocol. This is the reason why the desired properties of the protocol are expressed so easily