Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Stepwise refinement of heap-manipulating code in Chalice

  • 127 Accesses

  • 4 Citations

Abstract

Stepwise refinement is a well-studied technique for developing a program from an abstract description to a concrete implementation. This paper describes a system with automated tool support for refinement, powered by a state-of-the-art verification engine that uses an SMT solver. Unlike previous refinement systems, users of the presented system interact only via declarations in the programming language. Another aspect of the system is that it accounts for dynamically allocated objects in the heap, so that data representations in an abstract program can be refined into ones that use more objects. Finally, the system uses a language with familiar imperative features, including sequential composition, loops, and recursive calls, offers a syntax with skeletons for describing program changes between refinements, and provides a mechanism for supplying witnesses when refining non-deterministic programs.

This is a preview of subscription content, log in to check access.

References

  1. ABH+10

    Abrial J-R, Butler M, Hallerstede S, Hoang TS, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in Event-B. Int J Softw Tools Technol Transf

  2. Abr96

    Abrial J-R (1996) The B-Book: assigning programs to meanings. Cambridge University Press, Cambridge

  3. Abr03

    Abrial J-R (2003) Event based sequential program development: Application to constructing a pointer program. In: Araki K, Gnesi S, Mandrioli D (eds) FME 2003: formal methods, international symposium of formal methods Europe. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, pp 51–74

  4. Abr06

    Abrial J-R (2006) Formal methods in industry: achievements, problems, future. In: Osterweil LJ, Dieter Rombach H, Soffa ML (eds) 28th international conference on software engineering (ICSE 2006). ACM, New York, pp 761–768

  5. Abr10a

    Abrial J-R (2010a) Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge

  6. Abr10b

    Abrial J-R (2010b) Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge

  7. Bac78

    Back RJR (1978) On the correctness of refinement steps in program development. PhD thesis, University of Helsinki. Report A-1978-4.

  8. BCD+06

    Barnett M, Chang B-YE, DeLine R, Jacobs B, Leino KRM (2006) Boogie: a modular reusable verifier for object-oriented programs. In: de Boer FS, Bonsangue MM, Graf S, de Roever W-P (eds) Formal methods for components and objects: 4th international symposium, FMCO 2005. Lecture Notes in Computer Science, vol. 4111. Springer, Berlin, pp 364–387

  9. BDF+04

    Barnett M, DeLine R, Fähndrich M, Leino KRM, Schulte W (2004) Verification of object-oriented programs with invariants. J Object Technol 3(6): 27–56

  10. BFL+11

    Barnett M, Fähndrich M, Leino KRM, Müller P, Schulte W, Venter H (2011) Specification and verification: the Spec# experience. Commun. ACM 54(6): 81–91

  11. BFM+09

    Baudin P, Filliâtre JC, Marché C, Monate B, Moy Y, Prevosto V (2009) ACSL: ANSI/ISO C specification language, version 1.4. http://frama-c.com/

  12. BHL+10

    Ball T, Hackett B, Lahiri SK, Qadeer S, Vanegue J (2010) Towards scalable modular checking of user-defined properties. In: Leavens GT, O’Hearn P, Rajamani SK (eds) Verified software: theories, tools, experiments, (VSTTE 2010). Lecture Notes in Computer Science, vol 6217. Springer, Berlin, pp 1–24

  13. BMvW00

    Back R-J, Mikhaljova A, von Wright J (2000) Class refinement as semantics of correct object substitutability. Formal Aspects Comput 12(1): 18–40

  14. Boy03

    Boyland J (2003) Checking interference with fractional permissions. In: Cousot R (ed) Static analysis, 10th international symposium, SAS 2003. Lecture Notes in Computer Science, vol 2694. Springer, Berlin, pp 55–72

  15. BS91

    Back R-J, Sere K (1991) Stepwise refinement of action systems. Struct Program 12(1): 17–30

  16. BvW98

    Back R-J, von Wright J (1998) Refinement calculus: a systematic introduction. Graduate Texts in Computer Science. Springer, Berlin

  17. CD02

    Clarke D, Drossopoulou S (2002) Ownership, encapsulation and the disjointness of type and effect. In: Proceedings of the 2002 ACM SIGPLAN conference on object-oriented programming systems, languages and applications, OOPSLA 2002. ACM, New York, pp 292–310

  18. CDH+09

    Cohen E, Dahlweid M, Hillebrand M, Leinenbach D, Moskal M, Santen T, Schulte W, Tobies S (2009) VCC: a practical system for verifying concurrent C. In: Berghofer S, Nipkow T, Urban C, Wenzel M (eds) Theorem proving in higher order logics, 22nd international conference, TPHOLs 2009. Lecture Notes in Computer Science, vol 5674. Springer, Berlin, pp 23–42

  19. Cle

    ClearSy. Atelier B. http://www.atelierb.eu/.

  20. CMM05

    Carter G, Monahan R, Morris JM (2005) Software refinement with perfect developer. In: Aichernig BK, Beckert B (eds) Third IEEE international conference on software engineering and formal methods (SEFM 2005). IEEE Computer Society, New York, pp 363–373

  21. DD77

    Denning DE, Denning PJ (1977) Certification of programs for secure information flow. Commun ACM 20(7): 504–513

  22. Dij68

    Dijkstra EW (1968) A constructive approach to the problem of program correctness. BIT 8: 174–186

  23. Dij76

    Dijkstra EW (1976) A discipline of programming. Prentice Hall, Englewood Cliffs

  24. dMB08

    de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: TACAS 2008. Lecture Notes in Computer Science, vol 4963. Springer, Berlin, pp 337–340

  25. DMN70

    Dahl O-J, Myhrhaug B, Nygaard K (1970) Common base language. Publication S-22, Norwegian Computing Center

  26. Esc01

    Escher Technologies, Inc. (2001) Getting started with perfect. http://www.eschertech.com

  27. FOTSY10

    Filipović I, O’Hearn P, Torp-Smith N, Yang H (2010) Blaming the client: on data refinement in the presence of pointers. Formal Aspects Comput 22(5): 547–583

  28. GP85

    Gries D, Prins J (1985) A new notion of encapsulation. In: Proceedings of the ACM SIGPLAN 85 symposium on language issues in programming environments. SIGPLAN Notices, vol 20, No. 7. ACM, New York, pp 131–139

  29. GSR07

    Grandy H, Stenzel K, Reif W (2007) A refinement method for Java programs. In: Bonsangue MM, Johnsen EM (eds) Formal methods for open object-based distributed systems, 9th IFIP WG 6.1 international conference, FMOODS 2007. Lecture Notes in Computer Science, vol 4468. Springer, Berlin, pp 221–235

  30. GV90

    Gries D, Volpano D (1990) The transform—a new language construct. Struct Program 11(1): 1–10

  31. HKMS12

    Heule S, Kassios IT, Müller P, Summers AJ (2012) Verification condition generation for permission logics with abstraction functions. Technical Report 761, ETH Zurich

  32. HLL+12

    Hatcliff J, Leavens GT, Rustan M. Leino K, Müller P, Parkinson M (2012) Behavioral interface specification languages. ACM Comput Surv, 44(3)

  33. HLMS11

    Heule S, Rustan M. Leino K, Müller P, Summers AJ (2011) Fractional permissions without the fractions. In: 13th workshop on formal techniques for Java-like programs, FTfJP 2011

  34. Hoa72

    Hoare CAR (1972) Proof of correctness of data representations. Acta Informatica 1(4): 271–281

  35. Jac06

    Jackson D (2006) Software abstractions: logic, language, and analysis. MIT Press, Cambridge

  36. Jon90

    Jones CB (1990) Systematic software development using VDM. International Series in Computer Science, 2nd edn. Prentice Hall, Englewood Cliffs

  37. Jon96

    Jones CB (1996) Accommodating interference in the formal design of concurrent object-based programs. Formal Methods Syst Des 8(2): 105–122

  38. JP08

    Jacobs B, Piessens F (2006) The VeriFast program verifier. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven

  39. Kas06

    Kassios IT (2006) Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Misra J, Nipkow T, Sekerinski E (eds) FM 2006: formal methods, 14th international symposium on formal methods. Lecture Notes in Computer Science, vol 4085. Springer, Berlin, pp 268–283

  40. KSW10

    Klein G, Sewell T, Winwood S (2010) Refinement in the formal verification of seL4. In: Hardin DS (ed) Design and verification of microprocessor systems for high-assurance applications. Springer, Berlin, pp 323–339

  41. LB03

    Leuschel M, Butler M (2003) ProB: a model checker for B. In: Araki K, Gnesi S, Mandrioli D (eds) FME 2003: formal methods. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, pp 855–874

  42. Lea91

    Leavens GT (1991) Modular specification and verification of object-oriented programs. IEEE Softw 8(4): 72–80

  43. Lei10

    Leino KRM (2010) Dafny: an automatic program verifier for functional correctness. In: Clarke EM, Voronkov A (eds) LPAR-16. Lecture Notes in Computer Science, vol 6355. Springer, Berlin, pp 348–370

  44. LG86

    Liskov B, Guttag J (1986) Abstraction and specification in program development. MIT Electrical Engineering and Computer Science Series. MIT Press, Cambridge

  45. LM06

    Leino KRM, Müller P (2006) A verification methodology for model fields. In: Sestoft P (ed) Programming languages and systems, 15th European symposium on programming, ESOP 2006. Lecture Notes in Computer Science, vol 3924. Springer, Berlin, pp 115–130

  46. LM09

    Leino KRM, Müller P (2009) A basis for verifying multi-threaded programs. In: Castagna G (ed) Programming languages and systems, 18th European Symposium on Programming, ESOP 2009. Lecture Notes in Computer Science, vol 5502. Springer, Berlin, pp 378–393

  47. LMS09

    Leino KRM, Müller P, Smans J (2009) Verification of concurrent programs with Chalice. In: Aldini A, Barthe G, Gorrieri R (eds) Foundations of security analysis and design V: FOSAD 2007/2008/2009 tutorial lectures. Lecture Notes in Computer Science, vol 5705. Springer, Berlin, pp 195–222

  48. LN02

    Leino KRM, Nelson G (2002) Data abstraction and information hiding. ACM Trans Program Lang Syst 24(5): 491–553

  49. LR10

    Leino KRM, Rümmer P (2010) A polymorphic intermediate verification language: design and logical encoding. In: Esparza J, Majumdar R (eds) Tools and algorithms for the construction and analysis of systems, 16th international conference, TACAS 2010. Lecture Notes in Computer Science, vol 6015. Springer, Berlin, pp 312–327

  50. LW94

    Liskov B, Wing JM (1994) A behavioral notion of subtyping. ACM Trans Program Lang Syst 16(6)

  51. Mey88

    Meyer B (1998) Object-oriented software construction. Series in Computer Science. Prentice-Hall, NJ

  52. MLM+97

    Martin AJ, Lines A, Manohar R, Nyström M, Pénzes PI, Southworth R, Cummings U (1997) The design of an asynchronous MIPS R3000 microprocessor. In: 17th conference on advanced research in VLSI ARVLSI ’97. IEEE Computer Society, New York, pp 164–181

  53. Mor87

    Morris JM (1987) A theoretical basis for stepwise refinement and the programming calculus. Sci Comput Program 9(3): 287–306

  54. Mor90

    Morgan C (1990) Programming from specifications. Series in Computer Science. Prentice-Hall International, NJ

  55. Mor94

    Morgan C (1994) The cuppest capjunctive capping, and Galois. In: Roscoe AW (ed) A classical mind: essays in honour of C.A.R. Hoare. International Series in Computer Science. Prentice-Hall, NJ, pp 317–332

  56. Mor12

    Morgan C (2012) Compositional noninterference from first principles. Formal Aspects Comput 24(1): 3–26

  57. MS97

    Mikhaljova A, Sekerinski E (1997) Class refinement and interface refinement in object-oriented programs. In: Fitzgerald JS, Jones CB, Lucas P (eds) FME ’97: industrial applications and strengthened foundations of formal methods, 4th international symposium of formal methods Europe. Lecture Notes in Computer Science, vol 1313. Springer, Berlin, pp 82–101

  58. PB05

    Parkinson MJ, Bierman GM (2005) Separation logic and abstraction. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2005. ACM, New York, pp 247–258

  59. Rey02

    Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: 17th IEEE symposium on logic in computer science (LICS 2002). IEEE Computer Society, New York, pp 55–74

  60. SH02

    Shield J, Hayes IJ (2002) Refining object-oriented invariants and dynamic constraints. In: 9th Asia–Pacific software engineering conference (APSEC 2002). IEEE Computer Society, New York, pp 52–61

  61. SJP09

    Smans J, Jacobs B, Piessens F. Implicit dynamic frames: Combining dynamic frames and separation logic. In: Drossopoulou S (ed) ECOOP 2009—Object-oriented programming, 23rd European conference. Lecture Notes in Computer Science, vol 5653. Springer, Berlin, pp 148–172

  62. TBM10

    Tafat A, Boulmé S, Marché C (2010) A refinement methodology for object-oriented programs. In: Beckert B, Marché C (eds) Formal verification of object-oriented software, papers presented at the international conference, pp 143–159

  63. WD96

    Woodcock J, Davies J (1996) Using Z: Specification, refinement, and proof. Prentice Hall, NJ

  64. Wir71

    Wirth N (1971) Program development by stepwise refinement. Commun ACM 14: 221–227

Download references

Author information

Correspondence to K. Rustan M. Leino.

Additional information

Communicated by Peter Höfner, Robert van Glabbeek, Ian Hayes and Jim Woodcock

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Leino, K.R.M., Yessenov, K. Stepwise refinement of heap-manipulating code in Chalice. Form Asp Comp 24, 519–535 (2012). https://doi.org/10.1007/s00165-012-0254-3

Download citation

Keywords

  • Stepwise refinement
  • Data refinement
  • Heap refinement
  • Chalice
  • Abstract predicates
  • Fractional permissions
  • Program verification