Skip to main content
SpringerLink
Log in

A Precise Pictorial Language for Array Invariants

  • Conference paper
  • First Online:
Integrated Formal Methods (IFM 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11023))

Included in the following conference series:

Abstract

Pictorial languages, while intuitive and descriptive, are rarely used as the primary reasoning language in program verification due to lack of precision. In this paper, we introduce a precise pictorial language for specifying array invariants that preserves visual perspicuity. The language extends Reynold’s partition diagrams with the notion of a coloring, allowing assertions over portions of an array to be expressed by color-coding. The semantics of a coloring is given by a legend, mapping a colored partition of an array into a universally quantified predicate over the array. The pictorial syntax is an extension toinvariant diagrams, transition graphs where preconditions, postconditions and invariants, rather than the program code, determine the main program structure. We demonstrate the approach with three examples, verified using the Why3 theorem prover frontend.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Dijkstra, E.W.: A Discipline of Programming, 1st edn. Prentice Hall PTR, Upper Saddle River (1997)

    MATH  Google Scholar 

  2. Astrachan, O.L.: Pictures as invariants. In: Dale, N.B. (ed.) Proceedings of the 22nd SIGCSE Technical Symposium on Computer Science Education 1991, San Antonio, Texas, USA, 7–8 March 1991, pp. 112–118. ACM (1991)

    Google Scholar 

  3. Gries, D.: The Science of Programming, 1st edn. Springer, Secaucus (1987). https://doi.org/10.1007/978-1-4612-5983-1

    Book  MATH  Google Scholar 

  4. Reynolds, J.C.: The Craft of Programming. Prentice Hall PTR, Upper Saddle River (1981)

    MATH  Google Scholar 

  5. Back, R.J.: Invariant based programming: basic approach and teaching experiences. Form. Asp. Comput. 21(3), 227–244 (2009)

    Article  Google Scholar 

  6. Filliâtre, J.C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_8

    Chapter  Google Scholar 

  7. Back, R.J., Preoteasa, V.: Semantics and proof rules of invariant based programs. In: Proceedings of the 2011 ACM Symposium on Applied Computing, SAC 2011, pp. 1658–1665. ACM, New York (2011)

    Google Scholar 

  8. De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  9. Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  10. Ginat, D.: Loop invariants and mathematical games. SIGCSE Bull. 27(1), 263–267 (1995)

    Article  Google Scholar 

  11. Fava, D., Shapiro, D., Osborn, J., Schäef, M., Whitehead Jr., E.J.: Crowdsourcing program preconditions via a classification game. In: Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, pp. 1086–1096. ACM, New York (2016)

    Google Scholar 

  12. Logas, H., Vallejos, R., Osborn, J., Compton, K., Whitehead, J.: Visualizing loops and data structures in Xylem: the code of plants. In: Proceedings of the Fourth International Workshop on Games and Software Engineering, GAS 2015, pp. 50–56. IEEE Press, Piscataway (2015)

    Google Scholar 

  13. Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, pp. 338–350. ACM, New York (2005)

    Google Scholar 

  14. Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pp. 105–118. ACM, New York (2011)

    Google Scholar 

  15. Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 193–206. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_23

    Chapter  Google Scholar 

  16. Moremedi, K., van der Poll, J.A.: Transforming formal specification constructs into diagrammatic notations. In: Cuzzocrea, A., Maabout, S. (eds.) MEDI 2013. LNCS, vol. 8216, pp. 212–224. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-41366-7_18

    Chapter  Google Scholar 

  17. Jami, M., Ireland, A.: A verification condition visualizer. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 72–86. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12154-3_5

    Chapter  Google Scholar 

  18. Eriksson, J.: Tool-supported invariant-based programming. Ph.D. thesis, Turku Centre for Computer Science, Finland (2010). http://urn.fi/URN:ISBN:978-952-12-2446-1

Download references

Author information

Authors and Affiliations

  1. Department of Information Technologies, Åbo Akademi University, Vesilinnantie 3, 20500, Turku, Finland

    Johannes Eriksson, Masoumeh Parsa & Ralph-Johan Back

Authors
  1. Johannes Eriksson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Masoumeh Parsa
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ralph-Johan Back
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Masoumeh Parsa .

Editor information

Editors and Affiliations

  1. Università della Svizzera Italiana, Lugano, Switzerland

    Carlo A. Furia

  2. University of Queensland, Brisbane, Queensland, Australia

    Kirsten Winter

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Eriksson, J., Parsa, M., Back, RJ. (2018). A Precise Pictorial Language for Array Invariants. In: Furia, C., Winter, K. (eds) Integrated Formal Methods. IFM 2018. Lecture Notes in Computer Science(), vol 11023. Springer, Cham. https://doi.org/10.1007/978-3-319-98938-9_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-98938-9_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-98937-2

  • Online ISBN: 978-3-319-98938-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation