Abstract
It is widely recognized that abstraction and modularization are indispensable for specification of real-world programs. In source-code level program specification and verification, model fields are a common means for those goals. However, it remains a challenge to provide a well-founded formal semantics for the general case in which the abstraction relation defining a model field is non-functional.
In this paper, we discuss and compare several possibilities for defining model field semantics, and we give a complete formal semantics for the general case. Our analysis and the proposed semantics is based on a generalization of Hilbert’s ε terms.
This work was supported by the German National Science Foundation (DFG) under project “Program-level Specification and Deductive Verification of Security Properties” within priority programme 1496 “Reliably Secure Software Systems – RS3”.
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
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Baudin, P., Cuoq, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language, Version 1.5 (2010)
Breunesse, C.B., Poll, E.: Verifying JML specifications with model fields. In: Formal Techniques for Java-like Programs (FTfJP), pp. 51–60. No. 408 in Technical Report, ETH Zurich (July 2003)
Bruns, D.: Formal Semantics for the Java Modeling Language. Diploma thesis, Universität Karlsruhe (2009)
Darvas, Á., Müller, P.: Formal encoding of JML level 0 specifications in JIVE. Tech. Rep. 559, ETH Zürich (2007)
Engel, C.: A translation from JML to JavaDL. Studienarbeit, Fakultät für Informatik, Universität Karlsruhe (February 2005)
Giese, M., Ahrendt, W.: Hilbert’s ε-Terms in Automated Theorem Proving. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol. 1617, pp. 171–185. Springer, Heidelberg (1999)
Hilbert, D., Bernays, P.: Grundlagen der Mathematik, vol. II. Springer (1939)
Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1, 271–281 (1972)
Jacobs, B., Poll, E.: A logic for the Java Modeling Language (JML). Tech. Rep. CSI-R0018, University of Nijmegen, Computing Science Institute (November 2000)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes 31(3), 1–38 (2006)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D.M.: JML Reference Manual (July 13, 2011)
Leino, K.R.M., Müller, P.: A Verification Methodology for Model Fields. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 115–130. Springer, Heidelberg (2006)
Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems 24(5), 491–553 (2002)
Tafat, A., Boulmé, S., Marché, C.: A Refinement Methodology for Object-Oriented Programs. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 153–167. Springer, Heidelberg (2011)
Weiß, B.: Deductive Verification of Object-Oriented Software — Dynamic Frames, Dynamic Logic and Predicate Abstraction. Ph.D. thesis, Karlsruhe Institute of Technology (January 2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beckert, B., Bruns, D. (2012). Formal Semantics of Model Fields in Annotation-Based Specifications. In: Glimm, B., Krüger, A. (eds) KI 2012: Advances in Artificial Intelligence. KI 2012. Lecture Notes in Computer Science(), vol 7526. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33347-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-33347-7_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33346-0
Online ISBN: 978-3-642-33347-7
eBook Packages: Computer ScienceComputer Science (R0)