×

Specification patterns and proofs for recursion through the store. (English) Zbl 1342.68207

Owe, Olaf (ed.) et al., Fundamentals of computation theory. 18th international symposium, FCT 2011, Oslo, Norway, August 22–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22952-7/pbk). Lecture Notes in Computer Science 6914, 310-321 (2011).
Summary: Higher-order store means that code can be stored on the mutable heap that programs manipulate, and is the basis of flexible software that can be changed or re-configured at runtime. Specifying such programs is challenging because of recursion through the store, where new (mutual) recursions between code are set up on the fly. This paper presents a series of formal specification patterns that capture increasingly complex uses of recursion through the store. To express the necessary specifications we extend the separation logic for higher-order store given by J. Schwinghammer et al. [Lect. Notes Comput. Sci. 5771, 440–454 (2009; Zbl 1257.03056)], adding parameter passing, and certain recursively defined families of assertions. Finally, we apply our specification patterns and rules to an example program that exploits many of the possibilities offered by higher-order store; this is the first larger case study conducted with logical techniques based on work by Schwinghammer et al. [loc. cit.], and shows that they are practical.
For the entire collection see [Zbl 1220.68019].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Citations:

Zbl 1257.03056
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] The Crowfoot website (includes a version of the example in this paper), http://www.informatics.sussex.ac.uk/research/projects/PL4HOStore/crowfoot/
[2] Abadi, M., Cardelli, L.: A Theory of Objects. Springer-Verlag New York, Inc, Secaucus (1996) · Zbl 0876.68014 · doi:10.1007/978-1-4419-8598-9
[3] Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006) · Zbl 05189668 · doi:10.1007/11804192_6
[4] Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules for Algol-like languages. LMCS, vol. 2(5) (2006) · Zbl 1127.68019
[5] Charlton, N., Horsfall, B., Reus, B.: Formal reasoning about runtime code update. In: Abiteboul, S., Böhm, K., Koch, C., Tan, K.-L. (eds.) ICDE Workshops, pp. 134–138. IEEE, Los Alamitos (2011)
[6] Corbet, J., Rubini, A., Kroah-Hartman, G.: Linux device drivers, 3rd edn. O’Reilly Media, Sebastopol (2005)
[7] Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: OOPSLA, pp. 213–226 (2008)
[8] Gamma, E., Helm, R., Johnson, R.E., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995) · Zbl 0887.68013
[9] Henderson, B.: Linux loadable kernel module HOWTO, v1.09 (2006), http://tldp.org/HOWTO/Module-HOWTO/
[10] Honda, K., Yoshida, N., Berger, M.: An observationally complete program logic for imperative higher-order functions. In: LICS, pp. 270–279 (2005) · Zbl 1358.68071
[11] Jacobs, B., Smans, J., Piessens, F.: A quick tour of the veriFast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 304–311. Springer, Heidelberg (2010) · Zbl 05825369 · doi:10.1007/978-3-642-17164-2_21
[12] Krishnaswami, N.R., Aldrich, J., Birkedal, L., Svendsen, K., Buisse, A.: Design patterns in separation logic. In: TLDI, pp. 105–116 (2009)
[13] Landin, P.J.: The mechanical evaluation of expressions. Computer Journal 6(4), 308–320 (1964) · Zbl 0122.36106 · doi:10.1093/comjnl/6.4.308
[14] Neamtiu, I., Hicks, M.W., Stoyle, G., Oriol, M.: Practical dynamic software updating for C. In: PLDI, pp. 72–83 (2006) · doi:10.1145/1133981.1133991
[15] Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: POPL, pp. 320–333 (2006) · Zbl 1369.68150 · doi:10.1145/1111037.1111066
[16] Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: POPL, pp. 75–86 (2008) · Zbl 1295.68091 · doi:10.1145/1328438.1328451
[17] Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)
[18] Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested hoare triples and frame rules for higher-order store. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 440–454. Springer, Heidelberg (2009) · Zbl 1257.03056 · doi:10.1007/978-3-642-04027-6_32
[19] Stoyle, G., Hicks, M., Bierman, G., Sewell, P., Neamtiu, I.: Mutatis mutandis: Safe and predictable dynamic software updating. ACM Trans. Program. Lang. Syst. 29(4) (2007) · Zbl 05459404 · doi:10.1145/1255450.1255455
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.