Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2014 | OriginalPaper | Buchkapitel

A Logical Analysis of Framing for Specifications with Pure Method Calls

verfasst von : Anindya Banerjee, David A. Naumann

Erschienen in: Verified Software: Theories, Tools and Experiments

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

For specifying and reasoning about object-based programs it is often attractive for contracts to be expressed using calls to pure methods. It is useful for pure methods to have contracts, including read effects to support local reasoning based on frame conditions. This leads to puzzles such as the use of a pure method in its own contract. These ideas have been explored in connection with verification tools based on axiomatic semantics, guided by the need to avoid logical inconsistency, and focusing on encodings that cater for first order automated provers. This paper adds pure methods and read effects to region logic, a first-order program logic that features frame-based local reasoning and a proof rule for linking of clients with modules to achieve end-to-end correctness by modular reasoning. Soundness is proved with respect to a conventional operational semantics and using the extensional (i.e., relational) interpretation of read effects.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Nächstes Kapitel Efficient Refinement Checking in VCC
Fußnoten
1
Please note that \(\mathbin {\cdot \!\small \mathbf{/ \!.}}\) is not syntax in the logic; it’s a function in the metalanguage that is used to obtain formulas from effects; see Sect. 6.
 
2
This does not preclude nondeterminacy modulo an equivalence relation, which is especially important for ‘weakly pure’ methods that return freshly allocated references [13]. For VCs this is explored in [10].
 
3
Under these conditions, if the specifications in \(\varTheta \) refer to methods in \(\varDelta \), \(\varTheta \) is not swf on its own, and then it is not meaningful to call \(\theta \) a \(\varTheta \)-interpretation.
 
Literatur
1.
Banerjee, A., Naumann, D.A.: Local reasoning for global invariants. Part II: Dynamic boundaries. J. ACM 60(3), 19:1–19:73 (2013)
2.
Banerjee, A., Naumann, D.A., Rosenberg, S.: Local reasoning for global invariants. Part I: Region logic. J. ACM 60(3), 18:1–18:56 (2013)MathSciNet
3.
Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL (2004)
4.
Bobot, F., Filliâtre, J.-C.: Separation predicates: a taste of separation logic in first-order logic. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 167–181. Springer, Heidelberg (2012)CrossRef
5.
Darvas, A., Müller, P.: Reasoning about method calls in interface specifications. J. Object Technol. 5, 59–85 (2006)CrossRef
6.
Heule, S., Kassios, I.T., Müller, P., Summers, A.J.: Verification condition generation for permission logics with abstract predicates and abstraction functions. In: Castagna, G. (ed.) ECOOP 2013. LNCS, vol. 7920, pp. 451–476. Springer, Heidelberg (2013)CrossRef
7.
Hoare, C.A.R.: Proofs of correctness of data representations. Acta Inf. 1, 271–281 (1972)CrossRefMATH
8.
9.
Krishnaswami, N.R., Aldrich, J., Birkedal, L.: Verifying event-driven programs using Ramified frame properties. In: TLDI (2010)
10.
Leino, K.R.M., Müller, P.: Verification of equivalent-results methods. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 307–321. Springer, Heidelberg (2008)CrossRef
11.
Nanevski, A., Ahmed, A., Morrisett, G., Birkedal, L.: Abstract predicates and mutable ADTs in Hoare type theory. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 189–204. Springer, Heidelberg (2007)CrossRef
12.
Nanevski, A., Banerjee, A., Garg, D.: Dependent type theory for verification of information flow and access control policies. ACM Trans. Program. Lang. Syst. 35(2), 6 (2013)
13.
14.
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. ACM Trans. Prog. Lang. Syst. 31(3), 1–50 (2009)CrossRef
15.
Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: POPL (2005)
16.
Rosenberg, S., Banerjee, A., Naumann, D.A.: Local reasoning and dynamic framing for the composite pattern and its clients. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 183–198. Springer, Heidelberg (2010)CrossRef
17.
Rosenberg, S., Banerjee, A., Naumann, D.A.: Decision procedures for region logic. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 379–395. Springer, Heidelberg (2012)CrossRef
18.
Smans, J., Jacobs, B., Piessens, F., Schulte, W.: Automatic verification of Java programs with dynamic frames. Formal Aspects Comput. 22(3–4), 423–457 (2010)CrossRefMATH
19.
Summers, A.J., Drossopoulou, S.: A formal semantics for isorecursive and equirecursive state abstractions. In: Castagna, G. (ed.) ECOOP 2013. LNCS, vol. 7920, pp. 129–153. Springer, Heidelberg (2013)CrossRef
20.
Yang, H.: Relational separation logic. Theor. Comput. Sci. 375(1–3), 308–334 (2007)CrossRefMATH
Metadaten
Titel
A Logical Analysis of Framing for Specifications with Pure Method Calls
verfasst von
Anindya Banerjee
David A. Naumann
Copyright-Jahr
2014
Buch
Verified Software: Theories, Tools and Experiments

Print ISBN: 978-3-319-12153-6

Electronic ISBN: 978-3-319-12154-3

Copyright-Jahr: 2014

DOI
https://doi.org/10.1007/978-3-319-12154-3_1

Premium Partner

    Bildnachweise