Complete Calculi for Structured Specifications in Fork Algebra

LOPEZ POMBO, CARLOS GUSTAVO; FRIAS, MARCELO FABIAN

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Lugar: Berlín; Año: 2010 vol. 6255 p. 290 - 305

0302-9743

In previous articles we presented Argentum, a tool for rea- soning across heterogeneous specifications based on the language of fork algebras. Argentum’s foundations were formalized in the framework of institutions. The formalization made simple to describe a methodology capable of producing a complete system desription from partial views, eventually written in different logical languages. Structured specifications were introduced by Sannella and Tarlecki and extensively studied by Borzyszkowski. The latter also presented condi- tions under which the calculus for structured specifications is complete. Using fork algebras as a “universal” institution capable of representing expressive logics (such as dynamic and temporal logics), requires us- ing a fork language that includes a reflexive-transitive closure operator. The calculus thus obtained does not meet the conditions required by Borzyszkowski. In this article we present structure building operators (SBOs) over fork algebras, and provide a complete calculus for these operators.