Advertisement

Safe Modification of Pointer Programs in Refinement Calculus

  • Susumu Nishimura
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5133)

Abstract

This paper discusses stepwise refinement of pointer programs in the framework of refinement calculus. We augment the underlying logic with formulas of separation logic and then introduce a pair of new predicate transformers, called separating assertion and separating assumption. The new predicate transformers are derived from separating conjunction and separating implication, which are fundamental logical connectives in separation logic. They represent primitive forms of heap allocation/deallocation operators and the basic pointer statements can be specified by means of them. We derive several refinement laws that are useful for stepwise refinement and demonstrate the use of the laws in the context of correctness preserving transformations that are intended for improved memory usage.

The formal development is carried out in the framework of higher-order logic and is based on Back and Preoteasa’s axiomatization of state space and its extension to the heap storage [BP05, Pre06]. All the results have been implemented and verified in the theorem prover PVS.

Keywords

Pointer Program Separation Logic Predicate Transformer Local Scope Refinement Calculus 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Bac88]
    Back, R.-J.: A calculus of refinements for program derivations. Acta Informatica 25(6), 593–624 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  2. [BFP03]
    Back, R.-J., Fan, X., Preoteasa, V.: Reasoning about pointers in refinement calculus. In: 10th Asia-Pacific Software Engineering Conference (APSEC 2003), pp. 425–434 (2003)Google Scholar
  3. [BP05]
    Back, R.-J., Preoteasa, V.: An algebraic treatment of procedure refinement to support mechanical verification. Formal Aspects of Computing 17(1), 69–90 (2005)zbMATHCrossRefGoogle Scholar
  4. [BvW98]
    Back, R.-J., von Wright, J.: Graduate Texts in Computer Science. In: Refinement Calculus: A Systematic Introduction, Springer, Heidelberg (1998)Google Scholar
  5. [COY07]
    Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: 22nd IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 366–378. IEEE Computer Society, Los Alamitos (2007)Google Scholar
  6. [Gro00]
    Groves, L.J.: Evolutionary Software Development in the Refinement Calculus. PhD thesis, Victoria University of Wellington (2000)Google Scholar
  7. [LvW97]
    Laibinis, L., von Wright, J.:Context handling in the refinement calculus framework. Technical Report 118, TUCS Technical Report (1997)Google Scholar
  8. [Mor94]
    Morgan, C.: Programming from specifications, 2nd edn. Prentice-Hall International Series in Computer Science. Prentice-Hall International, Englewood Cliffs (1994)zbMATHGoogle Scholar
  9. [ORY01]
    O’Hearn, P., Reynolds, J.C., Yang, H.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  10. [OYR04]
    O’Hearn, P., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 268–280. ACM Press, New York (2004)CrossRefGoogle Scholar
  11. [Pre06]
    Preoteasa, V.: Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 508–523. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. [Rey02]
    Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 55–74. IEEE Computer Society, Los Alamitos (2002)CrossRefGoogle Scholar
  13. [SRSC01]
    Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference. Computer Science Laboratory, SRI International (November 2001), http://pvs.csl.sri.com/
  14. [YO02]
    Yang, H., O’Hearn, P.: A Semantic Basis for Local Reasoning. In: Nielsen, M., Engberg, U. (eds.) ETAPS 2002 and FOSSACS 2002. LNCS, vol. 2303, pp. 402–416. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Susumu Nishimura
    • 1
  1. 1.Dept. of Mathematics, Graduate School of ScienceKyoto University, Sakyo-kuKyotoJapan

Personalised recommendations