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 -