Abstract
We formalise proofs by structural induction on sets, specified as an algebraic data type. The core idea is that the standard scheme for constructor induction can be used for the derivation of alternative schemes. This way, considerable flexibility can be obtained for proofs in the inductive theory for the sets. For more general purposes we formulate a rule for ‘hybrid’ induction, which allows a variety of induction schemes.
A number of examples is provided, most of which contain well-known and intuitively clear facts about sets that are nevertheless not always easy to prove. We also use our material on sets for proving some interesting properties of two special processes that have sets as a parameter, specified in μCRL style, representing generalised alternative and parallel compositions of processes. We moreover demonstrate how our generalised parallel composition can be used for a specification of broadcasting.
Partly supported by the Foundation for Computer Science in the Netherlands (SION) and by the Netherlands Organisation for Scientific Research (NWO).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M.A. Bezem and J.F. Groote. A formal verification of the alternating bit protocol in the calculus of constructions. Technical Report Logic Group Preprint Series No. 88, Utrecht University, 1993.
J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Control, 60(1/3): 109–137, 1984.
J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.
J.J. Brunekreef, J.P. Katoen, R.L.C. Koymans and S. Mauw. Design and analysis of dynamic leader election protocols in broadcast networks. Technical report P9324, University of Amsterdam, 1993.
J.F. Groote and H. Korver. A correctness proof of the bakery protocol in μCRL. In this volume: A. Ponse, C. Verhoef and S.F.M. van Vlijmen, editors. Proceedings of ACP94. Workshops in Computing, Springer-Verlag, 1994.
J.F. Groote and A. Ponse. The syntax and semantics of μCRL. In this volume: A. Ponse, C. Verhoef and S.F.M. van Vlijmen, editors. Proceedings of ACP94. Workshops in Computing, Springer-Verlag, 1994.
J.F. Groote and A. Ponse. Proof theory for μCRL. Technical Report CS-R9138, CWI, Amsterdam, 1991.
J.F. Groote and A. Ponse. Proof theory for μCRL: a language for processes with data. In D.J. Andrews, J.F. Groote and C.A. Middelburg, editors, Proceedings of the International Workshop on Semantics of Specification Languages, pages 232–251. Workshops in Computing, Springer-Verlag, 1994.
J.F. Groote and J.J. van Wamel. Algebraic data types and induction in μCRL. Report P9409, University of Amsterdam, 1994.
H.P. Korver and J. Springintveld. A computer-checked verification of Milner’s scheduler. In H.P. Korver, Protocol Verification in μCRL, PhD thesis, University of Amsterdam, 1994.
J. Meseguer and J.A. Goguen. Initiality, induction and computability. In M. Nivat and J. Reynolds, editors, Algebraic Methods in Semantics, pages 459–541. Cambridge University Press, 1985.
R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.
A.S. Troelstra and D. van Dalen. Constructivism in Mathematics, An Introduction (vol I). North-Holland, 1988.
M. Wirsing. Algebraic specification. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science (vol II), pages 677–788. Elsevier Science Publishers B.V., 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 British Computer Society
About this paper
Cite this paper
van Wamel, J. (1995). Inductive Proofs with Sets, and some Applications in Process Algebra. In: Ponse, A., Verhoef, C., van Vlijmen, S.F.M. (eds) Algebra of Communicating Processes. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-2120-6_4
Download citation
DOI: https://doi.org/10.1007/978-1-4471-2120-6_4
Publisher Name: Springer, London
Print ISBN: 978-3-540-19909-0
Online ISBN: 978-1-4471-2120-6
eBook Packages: Springer Book Archive