Abstract
We present an axiomatic specification of a key fragment of DOM using structural separation logic. This specification allows us to develop modular reasoning about client programs that call the DOM.
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
Similar content being viewed by others
Notes
- 1.
It is possible to combine multiple cases into one by rewriting the pre- and postconditions as a disjunction of the cases and using logical variables to track each case. For clarity, we opt to write each case separately.
- 2.
Since DOM may be called by different client programs written in different languages, \(\mathsf {store} \) denotes a black-box predicate that can be instantiated to describe a variable store in the client language. Here, we instantiate it as the JavaScript variable store.
- 3.
All free logical variables on the right-hand side are parameters of the predicate on the left. We omit them for readability as they do not change throughout the execution. By contrast, the iteration number i, and the tag listeners \(\textsc {e}\) of node \(\textsc {n}\) may change (the latter may grow by getElementsByTagName) and are explicitly parameterised.
References
W3C DOM standard. www.w3.org/TR/REC-DOM-Level-1/level-one-core.html
Biri, N., Galmiche, D.: A separation logic for resource distribution. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 23–37. Springer, Heidelberg (2003)
Biri, N., Galmiche, D.: Models and separation logics for resource trees. J. Logic Comput. 17, 687–726 (2007)
Bodin, M., Chargueraud, A., Filaretti, D., Gardner, P., Maffeis, S., Naudz̆iūnienė, D., Schmitt, A., Smith, G.: A mechanised JavaScript specification. In: POPL (2014)
Calcagno, C., Dinsdale-Young, T., Gardner, P.: Adjunct elimination in context logic for trees. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 255–270. Springer, Heidelberg (2007)
Calcagno, C., Gardner, P., Zarfaty, U.: Context logic and tree update. In: POPL (2005)
Gardner, P., Maffeis, S., Smith, G.: Towards a program logic for JavaScript. In: POPL (2012)
Gardner, P., Raad, A., Wheelhouse, M., Wright, A.: Local reasoning for concurrent libraries: mind the gap. In: MFPS (2014)
Gardner, P., Smith, G., Wheelhouse, M., Zarfaty, U.: Local Hoare reasoning about DOM. In: PODS (2008)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. In: OOPSLA (1999)
Jensen, S.H., Møller, A., Thiemann, P.: Type analysis for JavaScript. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 238–255. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03237-0_17
Jensen, S.H., Madsen, M., Møller, A.: Modeling the HTML DOM and browser API in static analysis of JavaScript Web applications. In: ESEC/FSE 2011 (2013)
Lerner, B.S., Carroll, M., Kimmel, D.P., La Vallee, H.Q., Krishnamurthi, S.: Modeling and reasoning about DOM events. In: WebApps (2012)
Maffeis, S., Mitchell, J.C., Taly, A.: An operational semantics for JavaScript. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 307–325. Springer, Heidelberg (2008). doi:10.1007/978-3-540-89330-1_22
Park, C., Won, S., Jin, J., Ryu, S.: A static analysis of JavaScript web applications in the wild via practical DOM modeling (T). In: ASE (2015)
Parkinson, M.: Local reasoning for Java. Ph.D. thesis, Cambridge University (2006)
Raad, A.: Ph.D. thesis, Imperial College (2016, to appear)
Rajani, V., Bichhawat, A., Garg, D., Hammer, C.: Information flow control for event handling and the DOM in web browsers. In: CSF (2015)
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS (2002)
Russo, A., Sabelfeld, A., Chudnov, A.: Tracking information flow in dynamic tree structures. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 86–103. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04444-1_6
Møller, A., Jensen, S.H., Madsen, M.: Modeling the HTML DOM and browser API in static analysis of JavaScript web applications. In: FSE (2011)
Smith, G.: Local reasoning for web programs. Ph.D. thesis, Imperial College (2010)
Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higher-order programs with the Dijkstra Monad. In: PLDI (2013)
Thiemann, P.: A type safe DOM API. In: Bierman, G., Koch, C. (eds.) DBPL 2005. LNCS, vol. 3774, pp. 169–183. Springer, Heidelberg (2005). doi:10.1007/11601524_11
Wright, A.: Structural separation logic. Ph.D. thesis, Imperial College (2013)
Acknowledgements
This research was supported by EPSRC programme grants EP/H008373/1, EP/K008528/1 and EP/K032089/1.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Raad, A., Santos, J.F., Gardner, P. (2016). DOM: Specification and Client Reasoning. In: Igarashi, A. (eds) Programming Languages and Systems. APLAS 2016. Lecture Notes in Computer Science(), vol 10017. Springer, Cham. https://doi.org/10.1007/978-3-319-47958-3_21
Download citation
DOI: https://doi.org/10.1007/978-3-319-47958-3_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47957-6
Online ISBN: 978-3-319-47958-3
eBook Packages: Computer ScienceComputer Science (R0)