TY - GEN

T1 - Towards a mechanically supported and compositional calculus to design distributed algorithms

AU - Prasetya, I. S.W.B.

N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1994.

PY - 1994

Y1 - 1994

N2 - This paper presents a compositional extension of the programming calculus UNITY, which is used to design distributed programs. As the extension is compositional, we can use it to derive a program ’on the fly’. That is, we can shape a program at the same time as we manipulate and decompose its given specification, and each time we apply a compositionality theorem we basically add a detail to the shape. Safety properties are known to be compositional in UNITY, but progress in general are not. So, we define a class of progress properties which are compositional. In addition, for programs that are constructed from components that do not write each other's write variables, the compositionality of this new class of progress can be expressed elegantly. We also have formalized and verified the resulting calculus using the theorem prover HOL. Together with the available tools in HOL this provides a mechanical support in designing distributed programs.

AB - This paper presents a compositional extension of the programming calculus UNITY, which is used to design distributed programs. As the extension is compositional, we can use it to derive a program ’on the fly’. That is, we can shape a program at the same time as we manipulate and decompose its given specification, and each time we apply a compositionality theorem we basically add a detail to the shape. Safety properties are known to be compositional in UNITY, but progress in general are not. So, we define a class of progress properties which are compositional. In addition, for programs that are constructed from components that do not write each other's write variables, the compositionality of this new class of progress can be expressed elegantly. We also have formalized and verified the resulting calculus using the theorem prover HOL. Together with the available tools in HOL this provides a mechanical support in designing distributed programs.

UR - http://www.scopus.com/inward/record.url?scp=84958786444&partnerID=8YFLogxK

U2 - 10.1007/3-540-58450-1_54

DO - 10.1007/3-540-58450-1_54

M3 - Conference contribution

AN - SCOPUS:84958786444

SN - 9783540584506

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 362

EP - 377

BT - Higher Order Logic Theorem Proving and Its Applications - 7th International Workshop, Proceedings

A2 - Melham, Thomas F.

A2 - Camilleri, Juanito

PB - Springer

T2 - 7th International workshop on Higher Order Logic Theorem Proving and its Applications, 1994

Y2 - 19 September 1994 through 22 September 1994

ER -