Abstract
The ideal goal of any program logic is to develop logically correct programs without the need for predominant debugging. Separation logic is considered to be an effective program logic for proving programs that involve pointers. Reasoning with pointers becomes difficult especially due to the way they interfere with the modular style of program development. For instance, often there is aliasing arising due to several pointers to a given cell location. In such situations, any alteration to that cell in one of the program modules may affect the values of many syntactically unrelated expressions in other modules. In this chapter, we try to explore these difficulties through some simple examples and introduce the notion of separating conjunction as a tool to deal with it. We introduce separation logic as an extension of Hoare Logic using a programming language that has four pointer-manipulating commands. These commands perform the usual heap operations such as lookup, update, allocation and de-allocation. The new set of assertions and axioms of separation logic are presented in a semi-formal style. Examples are given to illustrate unique features of the new assertions and axioms. Finally, the chapter concludes with proofs of some real programs using the axioms of separation logic.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
J.C. Reynolds, Separation logic: a logic for shared mutable data structures, in Proceedings Seventeenth Annual IEEE Symposium on Logic in Computer Science (Los Alamitos, California, IEEE Computer Society, 2002) pp. 55–74
C.A.R. Hoare, An axiomatic basis for computer programming. Commun. ACM. 12(10):576–580, 583 (1969)
G. Winskel, The Formal Semantics of Programming Languages (MIT Press, USA, 1993)
H. Yang, Local Reasoning for Stateful Programs. Ph. D. dissertation (University of Illinois, Urbana-Champaign, Illinois, 2001)
J.C. Reynolds, An Introduction to Separation Logic (Preliminary Draft). http://www.cs.cmu.edu/jcr/copenhagen08.pdf. 23 Oct 2008
J.C. Reynolds, Intuitionistic reasoning about shared mutable data structures, in Millennial Perspectives in Computer Science, ed. by J. Davies, B. Roscoe, J. Woodcock (Houndsmill, Hampshire, Palgrave, 2000) pp. 303–321
P.W. O’Hearn, J.C. Reynolds, H. Yang, Local reasoning about programs that alter data structures, in Proceedings of 15th Annual Conference of the European Association for Computer Science Logic: CSL 2001, Lecture Notes in Computer Science (Springer, Berlin, 2001)
R.M. Burstall, Some techniques for proving correctness of programs which alter data structures, in Machine Intelligence, ed. by B. Meltzer, D. Michie, vol 7 (Edinburgh University Press, Edinburgh, Scotland, 1972), pp 23–50
R. Bornat, Proving pointer programs in Hoare logic. Math. Program Constr. (2000)
H. Yang, An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm, in SPACE 2001: Informal Proceedings of Workshop on Semantics, Program Analysis and Computing Environments for Memory Management, ed by F. Henglein, J. Hughes, H. Makholm, H. Niss (IT University of Copenhagen, Denmark, 2001), pp. 41–68
Peter W. O’Hearn, David J. Pym, The logic of bunched implications. Bull. Symbol. Logic 5(2), 215–244 (1999)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer Science+Business Media Singapore
About this chapter
Cite this chapter
Singh, A.K., Natarajan, R. (2017). Separation Logic to Meliorate Software Testing and Validation. In: Mohanty, H., Mohanty, J., Balakrishnan, A. (eds) Trends in Software Testing. Springer, Singapore. https://doi.org/10.1007/978-981-10-1415-4_5
Download citation
DOI: https://doi.org/10.1007/978-981-10-1415-4_5
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-10-1414-7
Online ISBN: 978-981-10-1415-4
eBook Packages: EngineeringEngineering (R0)