zbMATH — the first resource for mathematics

Stepwise refinement of heap-manipulating code in Chalice. (English) Zbl 1259.68034
Summary: 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.
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: DOI
[1] 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] Abrial J-R (1996) The B-Book: assigning programs to meanings. Cambridge University Press, Cambridge · Zbl 0915.68015
[3] 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] 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] Abrial J-R (2010a) Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge · Zbl 1213.68214
[6] Abrial J-R (2010b) Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge · Zbl 1213.68214
[7] Back RJR (1978) On the correctness of refinement steps in program development. PhD thesis, University of Helsinki. Report A-1978-4.
[8] 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] 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 · Zbl 05431131 · doi:10.5381/jot.2004.3.6.a2
[10] 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 · Zbl 05928243 · doi:10.1145/1953122.1953145
[11] 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] 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] Back R-J, Mikhaljova A, von Wright J (2000) Class refinement as semantics of correct object substitutability. Formal Aspects Comput 12(1): 18–40 · Zbl 0963.68103 · doi:10.1007/s001650070034
[14] 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 · Zbl 1067.68537
[15] Back R-J, Sere K (1991) Stepwise refinement of action systems. Struct Program 12(1): 17–30
[16] Back R-J, von Wright J (1998) Refinement calculus: a systematic introduction. Graduate Texts in Computer Science. Springer, Berlin
[17] 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] 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] ClearSy. Atelier B. http://www.atelierb.eu/ .
[20] 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] Denning DE, Denning PJ (1977) Certification of programs for secure information flow. Commun ACM 20(7): 504–513 · Zbl 0361.68033 · doi:10.1145/359636.359712
[22] Dijkstra EW (1968) A constructive approach to the problem of program correctness. BIT 8: 174–186 · Zbl 0167.46002 · doi:10.1007/BF01933419
[23] Dijkstra EW (1976) A discipline of programming. Prentice Hall, Englewood Cliffs · Zbl 0368.68005
[24] 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] Dahl O-J, Myhrhaug B, Nygaard K (1970) Common base language. Publication S-22, Norwegian Computing Center
[26] Escher Technologies, Inc. (2001) Getting started with perfect. http://www.eschertech.com
[27] 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 · Zbl 1214.68118 · doi:10.1007/s00165-009-0125-8
[28] 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] 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] Gries D, Volpano D (1990) The transform–a new language construct. Struct Program 11(1): 1–10
[31] 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] Hatcliff J, Leavens GT, Rustan M. Leino K, Müller P, Parkinson M (2012) Behavioral interface specification languages. ACM Comput Surv, 44(3) · Zbl 1293.68078
[33] 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] Hoare CAR (1972) Proof of correctness of data representations. Acta Informatica 1(4): 271–281 · Zbl 0244.68009 · doi:10.1007/BF00289507
[35] Jackson D (2006) Software abstractions: logic, language, and analysis. MIT Press, Cambridge
[36] Jones CB (1990) Systematic software development using VDM. International Series in Computer Science, 2nd edn. Prentice Hall, Englewood Cliffs
[37] Jones CB (1996) Accommodating interference in the formal design of concurrent object-based programs. Formal Methods Syst Des 8(2): 105–122 · Zbl 05477976 · doi:10.1007/BF00122417
[38] Jacobs B, Piessens F (2006) The VeriFast program verifier. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven
[39] 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] 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] 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] Leavens GT (1991) Modular specification and verification of object-oriented programs. IEEE Softw 8(4): 72–80 · Zbl 05101975 · doi:10.1109/52.300040
[43] 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 · Zbl 1253.68095
[44] Liskov B, Guttag J (1986) Abstraction and specification in program development. MIT Electrical Engineering and Computer Science Series. MIT Press, Cambridge · Zbl 0644.68001
[45] 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] 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 · Zbl 1234.68078
[47] 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] Leino KRM, Nelson G (2002) Data abstraction and information hiding. ACM Trans Program Lang Syst 24(5): 491–553 · Zbl 05459296 · doi:10.1145/570886.570888
[49] 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] Liskov B, Wing JM (1994) A behavioral notion of subtyping. ACM Trans Program Lang Syst 16(6)
[51] Meyer B (1998) Object-oriented software construction. Series in Computer Science. Prentice-Hall, NJ
[52] 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] Morris JM (1987) A theoretical basis for stepwise refinement and the programming calculus. Sci Comput Program 9(3): 287–306 · Zbl 0624.68017 · doi:10.1016/0167-6423(87)90011-6
[54] Morgan C (1990) Programming from specifications. Series in Computer Science. Prentice-Hall International, NJ · Zbl 0697.68018
[55] 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] Morgan C (2012) Compositional noninterference from first principles. Formal Aspects Comput 24(1): 3–26 · Zbl 1242.68071 · doi:10.1007/s00165-010-0167-y
[57] 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] 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 · Zbl 1369.68151
[59] 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] 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] 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] 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] Woodcock J, Davies J (1996) Using Z: Specification, refinement, and proof. Prentice Hall, NJ · Zbl 0855.68060
[64] Wirth N (1971) Program development by stepwise refinement. Commun ACM 14: 221–227 · Zbl 0214.43005 · doi:10.1145/362575.362577
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.