Using Hoare Logic in a Process Algebra Setting

• Autorzy: Bergstra J. A. , Middelburg C. A.

Identyfikatory

DOI

10.3233/FI-2021-2026

• Języki publikacji: EN

Abstrakty

EN

This paper concerns the relation between process algebra and Hoare logic. We investigate the question whether and how a Hoare logic can be used for reasoning about how data change in the course of a process when reasoning equationally about that process. We introduce an extension of ACP (Algebra of Communicating Processes) with features that are relevant to processes in which data are involved, present a Hoare logic for the processes considered in this process algebra, and discuss the use of this Hoare logic as a complement to pure equational reasoning with the equational axioms of the process algebra.

Słowa kluczowe

EN

process algebra; data parameterized action; assignment action; guarded command; asserted process; Hoare logic

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 179, nr 4
• Strony: 321--344
• Opis fizyczny: Bibliogr. 29 poz., tab.

Twórcy

autor

Bergstra J. A.

• Informatics Institute, University of Amsterdam, Amsterdam, the Netherlands

autor

Middelburg C. A.

• Informatics Institute, University of Amsterdam, Amsterdam, the Netherlands

Bibliografia

• [1] Bergstra JA, Klop JW. Process Algebra for Synchronous Communication. Information and Control, 1984. 60(1-3):109-137. doi:10.1016/S0019-9958(84)80025-X.
• [2] Baeten JCM, Weijland WP. Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 1990. doi:10.1017/CBO9780511624193.
• [3] Bergstra JA, Bethke I, Ponse A. Process Algebra with Iteration and Nesting. Computer Journal, 1994. 37:243-258. doi:10.1093/comjnl/37.4.243.
• [4] Bergstra JA, Fokkink WJ, Ponse A. Process Algebra with recursive operations. In: Bergstra JA, Ponse A, Smolka SA (eds.), Handbook of Process Algebra, pp. 333-389. Elsevier, Amsterdam, 2001. doi:10.1016/B978-044482830-9/50023-0.
• [5] Sewell P. Bisimulation Is Not Finitely (First Order) Equationally Axiomatisable. In: LICS’94. IEEE Computer Society Press, 1994 pp. 62-70. doi:10.1109/LICS.1994.316086.
• [6] Bergstra JA, Middelburg CA. A Process Calculus with Finitary Comprehended Terms. Theory of Computing Systems, 2013. 53(4):645-668. doi:10.1007/s00224-013-9468-x.
• [7] Schneider FB. On Concurrent Programming. Graduate Texts in Computer Science. Springer-Verlag, Berlin, 1997. doi:10.1007/978-1-4612-1830-2.
• [8] Lamport L. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 1994. 16(3):872-923. doi:10.1145/177492.177726.
• [9] Sannella D, Tarlecki A. Algebraic Preliminaries. In: Astesiano E, Kreowski HJ, Krieg-Brückner B (eds.), Algebraic Foundations of Systems Specification, pp. 13-30. Springer-Verlag, Berlin, 1999. doi:10.1007/978-3-642-59851-7_2.
• [10] Wirsing M. Algebraic Specification. In: van Leeuwen J (ed.), Handbook of Theoretical Computer Science, volume B, pp. 675-788. Elsevier, Amsterdam, 1990. doi:10.1016/B978-0-444-88074-1.50018-4.
• [11] Pigozzi D, Salibra A. The Abstract Variable-Binding Calculus. Studia Logica, 1995. 55(1):129-179. doi:10.1007/BF01053036.
• [12] Baeten JCM, Bergstra JA. Global Renaming Operators in Concrete Process Algebra. Information and Computation, 1988. 78(3):205-245. doi:10.1016/0890-5401(88)90027-2.
• [13] Baeten JCM, Bergstra JA. Process Algebra with Signals and Conditions. In: Broy M (ed.), Programming and Mathematical Methods, volume F88 of NATO ASI Series. Springer-Verlag, 1992 pp. 273-323. doi:10.1007/978-3-642-77572-713.
• [14] Groote JF, Ponse A. Process Algebra with Guards: Combining Hoare Logic with Process Algebra. Formal Aspects of Computing, 1994. 6(2):115-164. doi:10.1007/BF01221097.
• [15] Bergstra JA, Middelburg CA. Splitting Bisimulations and Retrospective Conditions. Information and Computation, 2006. 204(7):1083-1138. doi:10.1016/j.ic.2006.03.003.
• [16] Baeten JCM, Bergstra JA. Process Algebra with Propositional Signals. Theoretical Computer Science, 1997. 177:381-405. doi:10.1016/S0304-3975(96)00253-8.
• [17] Baeten JCM, Verhoef C. A Congruence Theorem for Structured Operational Semantics with Predicates. In: Best E (ed.), CONCUR’93, volume 715 of Lecture Notes in Computer Science. Springer-Verlag, 1993 pp. 477-492. doi:10.1007/3-540-57208-2_33.
• [18] Milner R. A Complete Inference System for a Class of Regular Behaviours. Journal of Computer and System Sciences, 1984. 28(3):439-466. doi:10.1016/0022-0000(84)90023-0.
• [19] Fokkink WJ. On the Completeness of the Equations for the Kleene Star in Bisimulation. In: Wirsing M, Nivat M (eds.), AMAST 96, volume 1101 of Lecture Notes in Computer Science. Springer-Verlag, 1996 pp. 180-194. doi:10.1007/BFb0014315.
• [20] Cook SA. Soundness and Completeness of an Axiom System for Program Verification. SIAM Journal of Computing, 1978. 7(1):70-90. doi:10.1137/0207005.
• [21] Harel D, Pnueli A. On the development of reactive systems. In: Apt K (ed.), Logics and Models of Concurrent Systems, volume F13 of NATO ASI Series. Springer-Verlag, 1985 pp. 477-498. doi:10.1007/978-3-642-82453-1_17.
• [22] Owicki S, Gries D. An Axiomatic Proof Technique for Parallel Programs I. Acta Informatica, 1976. 6(4):319-340. doi:10.1007/BF00268134.
• [23] Apt KR, de Boer FS, Olderog ER. Verification of Sequential and Concurrent Programs. Texts in Computer Science. Springer-Verlag, Berlin, third edition, 2009. doi:10.1007/978-1-84882-745-5.
• [24] Hoare CAR. An Axiomatic Basis for Computer Programming. Communications of the ACM, 1969. 12(10):576-580, 583. doi:10.1145/363235.363259.
• [25] Lauer PE. Consistent Formal Theories of the Semantics of Programming Languages. Technical Report 25.121, IBM Laboratory Vienna, 1971.
• [26] Hoare CAR. Towards a Theory of Parallel Programming. In: Hoare CAR, Perrott RH (eds.), Operating Systems Techniques. Academic Press, 1972 pp. 61-71. doi:10.1007/978-1-4757-3472-0_6.
• [27] Apt KR, Francez N, de Roever WP. A Proof System for Communicating Sequential Processes. ACM Transactions on Programming Languages and Systems, 1980. 2(3):359-385. doi:10.1145/357103.357110.
• [28] Levin GM, Gries D. A Proof Technique for Communicating Sequential Processes. Acta Informatica, 1981. 15(3):281-302. doi:10.1007/BF00289266.
• [29] Hoare CAR. Communicating Sequential Processes. Communications of the ACM, 1978. 21(8):666-677. doi:10.1145/359576.359585.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).