Advertisement

Author Archives

Research and Advances

Social processes and proofs of theorems and programs

It is argued that formal verifications of programs, no matter how obtained, will not play the same key role in the development of computer science and software engineering as proofs do in mathematics. Furthermore the absence of continuity, the inevitability of change, and the complexity of specification of significantly many real programs make the formal verification process difficult to justify and manage. It is felt that ease of formal verification should not dominate program language design.
Research and Advances

Preserving average proximity in arrays

Programmers and data structure designers are often forced to choose between alternative structures. In storing these structures, preserving logical adjacencies or “proximity” is usually an important consideration. The combinatorial problem of storing arrays as various kinds of list structures is examined. Embeddings of graphs are used to model the loss of proximity involved in such storage schemes, and an elementary proof that arrays cannot be stored as linear lists with bounded loss of proximity is presented. Average loss of proximity is then considered, and it is shown that arrays cannot be stored as linear lists with only bounded loss of average proximity, but can be so stored in binary trees. The former result implies, for instance, that row major order is an asymptotically optimal storage strategy for arrays.
Research and Advances

Reduction: a method of proving properties of parallel programs

When proving that a parallel program has a given property it is often convenient to assume that a statement is indivisible, i.e. that the statement cannot be interleaved with the rest of the program. Here sufficient conditions are obtained to show that the assumption that a statement is indivisible can be relaxed and still preserve properties such as halting. Thus correctness proofs of a parallel system can often be greatly simplified.

Shape the Future of Computing

ACM encourages its members to take a direct hand in shaping the future of the association. There are more ways than ever to get involved.

Get Involved