Abstract
We propose a unifying treatment of multi-valued logic in the general context of specification, presented in the style of the Unifying Theories of Programming of Hoare and He. At a low level, UTP theories correspond to different types of three-valued logic. At higher levels they correspond to individual specifications. Designs are considered as their models, but members of other unifying theories of computation can serve as models just as well. Using this setup we have the opportunity to show correspondences between specification languages that use different logics.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Woodcock, J., Saaltink, M., Freitas, L.: Unifying theories of undefinedness. In: Summer School Marktoberdorf 2008: Engineering Methods and Tools for Software Safety and Security. NATO ASI Series F. IOS Press, Amsterdam (2009)
Bochvar, D.A., Bergmann, M.: On a three-valued logical calculus and its application to the analysis of the paradoxes of the classical extended functional calculus. History and Philosophy of Logic 2(1), 87–112 (1981)
McCarthy, J.: A basis for a mathematical theory of computation. In: Computer Programming and Formal Systems, pp. 33–70. North-Holland (1963)
Barringer, H., Cheng, J.H., Jones, C.B.: A logic covering undefinedness in program proofs. Acta Informatica 21 (1984)
Woodcock, J., Davies, J.: Using Z. Specification, Refinement, and Proof. Prentice-Hall (1996)
Farmer, W.M.: A partial functions version of Church’s simple theory of types. Journal of Symbolic Logic, 1269–1291 (1990)
Woodcock, J., Bandur, V.: Unifying theories of undefinedness in UTP. In: Wolff, B., Gaudel, M.-C., Feliachi, A. (eds.) UTP 2012. LNCS, vol. 7681, pp. 1–22. Springer, Heidelberg (2013)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall (1998)
Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. Journal of the ACM 39(1), 95–146 (1992)
Goguen, J., Burstall, R.: A study in the foundations of programming methodology: Specifications, institutions, charters and parchments. In: Poigné, A., Pitt, D.H., Rydeheard, D.E., Abramsky, S. (eds.) Category Theory and Computer Programming. LNCS, vol. 240, pp. 313–333. Springer, Heidelberg (1986)
Meseguer, J.: General logics. In: Logic Colloquium 87, pp. 275–329. North Holland (1989)
Cerioli, M., Meseguer, J.: May I borrow your logic (transporting logical structures along maps). Theor. Comput. Sci. 173(2), 311–347 (1997)
Tarlecki, A.: Moving between logical systems. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 478–502. Springer, Heidelberg (1996)
Mayoh, B.: Galleries and institutions. Technical Report DAIMI PB-191, Aarhus University (1985)
Gavilanes-Franco, A., Lucio-Carrasco, F.: A First-Order Logic for Partial Functions. Theoretical Computer Science 74(1) (July 1990)
Hoogewijs, A.: Partial-predicate logic in computer science. Acta Informatica 24(4), 381–393 (1987)
Blikle, A.: Three-valued predicates for software specification and validation. In: Bloomfield, R.E., Jones, R.B., Marshall, L.S. (eds.) VDM 1988. LNCS, vol. 328, pp. 243–266. Springer, Heidelberg (1988)
Hoogewijs, A.: A partial-predicate calculus in a two-valued logic. Mathematical Logic Quarterly 29(4), 239–243 (1983)
Jones, M.: A typed logic of partial functions reconstructed classically. Acta Informatica 31 (1994)
Fitzgerald, J.S., Jones, C.B.: The connection between two ways of reasoning about partial functions. Information Processing Letters 107(3-4), 128–132 (2008)
Woodcock, J., Freitas, L.: Linking VDM and Z. In: ICECCS, pp. 143–152. IEEE Computer Society (2008)
Jones, C.B.: Systematic Software Development using VDM. Prentice Hall (1990)
Larsen, P.G., Battle, N., Ferreira, M., Fitzgerald, J., Lausdahl, K., Verhoef, M.: The Overture initiative – integrating tools for VDM. SIGSOFT Softw. Eng. Notes 35, 1–6 (2010)
Rose, A.: A lattice-theoretical characterisation of three-valued logic. Journal of the London Mathematical Society s1 - 25(4), 255–259 (1950)
Woodruff, P.W.: Logic and truth value gaps. In: Lambert, K. (ed.) Philosophical Problems in Logic: Some Recent Developments, pp. 121–142. D. Reidel Publishing Co., Dordrecht (1970)
Belnap, N.: A useful four-valued logic. In: Dunn, J.M., Epstein, G. (eds.) Modern Uses of Multiple-valued Logic, pp. 8–37. D. Reidel (1977)
Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, New York (1972)
Bandur, V.: Unifying Theories of Multi-Valued Logic and Specification. PhD thesis, The University of York (in preparation, 2013)
Woodcock, J., Cavalcanti, A., Fitzgerald, J., Larsen, P., Miyazawa, A., Perry, S.: Features of CML: A formal modelling language for systems of systems. In: 7th SoSE. IEEE Systems Journal, vol. 6. IEEE (July 2012)
Foster, S., Woodcock, J.: Unifying theories of programming in Isabelle. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming. LNCS, vol. 8050, pp. 109–155. Springer, Heidelberg (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bandur, V., Woodcock, J. (2013). Unifying Theories of Logic and Specification. In: Iyoda, J., de Moura, L. (eds) Formal Methods: Foundations and Applications. SBMF 2013. Lecture Notes in Computer Science, vol 8195. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41071-0_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-41071-0_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41070-3
Online ISBN: 978-3-642-41071-0
eBook Packages: Computer ScienceComputer Science (R0)