Abstract
We present the core-\(\mathcal{L}_\pi\)fragment of \(\mathcal{L}_\pi\)and its program logic. We illustrate the adequacy of \(\mathcal{L}_\pi\)as a meta-language for jointly defining operational semantics and program logics of languages with concurrent and logic features, considering the case of a specification logic for concurrent objects addressing mobile features like creation of objects and channels in a simple way. Specifications are executable by a translation that assigns to every specification a model in the form of a core-\(\mathcal{L}_\pi\)program. We also illustrate the usefulness of this framework in reasoning about systems and their components.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
L. Caires. A language for the logical specification of processes and relations. In Michael Hanus, editor, Proceedings of the Algebraic and Logic Programming International Conference, number 1139 in LNCS, pages 150–164, 1996.
L. Caires. A language for the logical specification of processes and relations. Technical Report 6.96, Universidade Nova de Lisboa, DI/FCT, 1996. http://www-ctp.di.fct.unl.pt/~lcaires/writings/lpi6.96.ps.gz.
L. Caires and L. Monteiro. Proof net semantics of proof search computation. In K. Meinke and M. Hanus, editors, Proceedings of the Algebraic and Logic Programming International Conference, number 1298 in LNCS, pages 194–208, 1997.
J. Fiadeiro and T. Maibaum. Temporal theories as modularisation units for concurrent system specification. Formal Aspects of Computing, 4(3):239–272, 1992.
D. Kozen. Results on the propositional Μ-calculus. TCS, 27(3):333–354, 1983.
D. Miller. A survey of linear logic programming. Computational Logic, 2(2), 1995.
D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform proof as a foundation for logic programming. Ann. of Pure and App. Logic, (51):125–157, 1991.
R. Milner. Functions as processes. Math. Struc. in Computer Sciences, 2(2):119–141, 1992.
R. Milner. Calculi for interaction. Acta Informatica, 33(8):707–737, 1996.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, Part I 4-II. Information and Computation, 100(1):1–77, 1992.
O. Nierstrasz, J-G. Schneider, and M. Lumpe. Formalizing composable software systems-A research agenda. In Proceedings 1st IFIP Workshop on Formal Methods for Open Object-based Distributed Systems FMOODS'96, pages 271–282. Chapmann and Hall, 1996.
B. Pierce and D. Turner. Concurrent objects in a process calculus. In Takayasu Ito and Akinori Yonezawa, editors, Theory and Practice of Parallel Programming (TPPP), Sendai, Japan (Nov. 1994), number 907 in Lecture Notes in Computer Science, pages 187–215. Springer-Verlag, April 1995.
A. Pnueli. The temporal semantics of concurrent programs. In G. Kahn, editor, Semantics of Concurrent Computations, volume 70 of LNCS, pages 1–20, Evian, France, July 1979. Springer-Verlag, Berlin, Germany.
D. Sangiorgi. An interpretation of typed objects into the typed 7r-calculus. Technical report, INRIA Technical Report RR-3000, 1996.
A. Sernadas, C. Sernadas, and J. Costa. Object specification logic. Journal of Logic and Computation, 5(5):603–630, October 1995.
D. Walker. Objects in the π-calculus. Journal of Information and Computation, 116(2):253–271, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Caires, L., Monteiro, L. (1998). Verifiable and executable logic specifications of concurrent objects in \(\mathcal{L}_\pi\) . In: Hankin, C. (eds) Programming Languages and Systems. ESOP 1998. Lecture Notes in Computer Science, vol 1381. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0053562
Download citation
DOI: https://doi.org/10.1007/BFb0053562
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64302-9
Online ISBN: 978-3-540-69722-0
eBook Packages: Springer Book Archive