Skip to main content
SpringerLink
Log in
Book cover

International Joint Conference on Automated Reasoning

IJCAR 2008: Automated Reasoning pp 100–115Cite as

Efficient Well-Definedness Checking

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 5195))

Abstract

Formal specifications often contain partial functions that may lead to ill-defined terms. A common technique to eliminate ill-defined terms is to require well-definedness conditions to be proven. The main advantage of this technique is that it allows us to reason in a two-valued logic even if the underlying specification language has a three-valued semantics. Current approaches generate well-definedness conditions that grow exponentially with respect to the input formula. As a result, many tools prove shorter, but stronger approximations of these well-definedness conditions instead.

We present a procedure which generates well-definedness conditions that grow linearly with respect to the input formula. The procedure has been implemented in the Spec# verification tool. We also present empirical results that demonstrate the improvements made.

This is a preview of subscription content, 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 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. UML 2.0 OCL Specification (May 2006), http://www.omg.org/docs/formal/06-05-01.pdf

  2. Abrial, J.-R.: The B Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)

    MATH  Google Scholar 

  3. Abrial, J.-R., Mussat, L.: On using conditional definitions in formal theories. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 242–269. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Arthan, R.: Undefinedness in Z: Issues for specification and proof. In: CADE Workshop on Mechanization of Partial Functions (1996)

    Google Scholar 

  5. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)

    Google Scholar 

  6. Barrett, C.W., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)

    Google Scholar 

  7. Barringer, H., Cheng, J.H., Jones, C.B.: A logic covering undefinedness in program proofs. Acta Informatica 21, 251–269 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  8. Behm, P., Burdy, L., Meynadier, J.-M.: Well Defined B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 29–45. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  9. Berezin, S., Barrett, C., Shikanian, I., Chechik, M., Gurfinkel, A., Dill, D.L.: A practical approach to partial functions in CVC Lite. In: Workshop on Pragmatics of Decision Procedures in Automated Reasoning (2004)

    Google Scholar 

  10. Chalin, P.: Are the logical foundations of verifying compiler prototypes matching user expectations? Formal Aspects of Computing 19(2), 139–158 (2007)

    Article  MATH  Google Scholar 

  11. Chalin, P.: A sound assertion semantics for the dependable systems evolution verifying compiler. In: ICSE, pp. 23–33. IEEE Computer Society Press, Los Alamitos (2007)

    Google Scholar 

  12. Cheng, J.H., Jones, C.B.: On the usability of logics which handle partial functions. In: Refinement Workshop, pp. 51–69 (1991)

    Google Scholar 

  13. Crow, J., Owre, S., Rushby, J., Shankar, N., Srivas, M.: A tutorial introduction to PVS. In: Workshop on Industrial-Strength Formal Specification Techniques (1995)

    Google Scholar 

  14. de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Google Scholar 

  15. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (2003)

    Google Scholar 

  16. Gries, D., Schneider, F.B.: Avoiding the undefined by underspecification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 366–373. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  17. Guttag, J.V., Horning, J.J.: Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer, Heidelberg (1993)

    MATH  Google Scholar 

  18. Hähnle, R.: Many-valued logic, partiality, and abstraction in formal specification languages. Logic Journal of the IGPL 13(4), 415–433 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  19. Hoogewijs, A.: On a formalization of the non-definedness notion. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 25, 213–217 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  20. Jones, C.B.: Systematic software development using VDM. Prentice-Hall, Englewood Cliffs (1986)

    MATH  Google Scholar 

  21. Kiniry, J.R., Cok, D.R.: ESC/Java2: Uniting ESC/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005)

    Google Scholar 

  22. Kleene, S.C.: On a notation for ordinal numbers. Journal of Symbolic Logic 3, 150–155 (1938)

    Article  MATH  Google Scholar 

  23. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes 31(3), 1–38 (2006)

    Article  Google Scholar 

  24. McCarthy, J.: A basis for a mathematical theory of computation. In: Braffort, P., Hirschberg, D. (eds.) Computer Programming and Formal Systems, pp. 33–70. North-Holland, Amsterdam (1963)

    Google Scholar 

  25. Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  26. Rudich, A., Darvas, Á., Müller, P.: Checking well-formedness of pure-method specifications. In: Cuellar, J., Maibaum, T. (eds.) Formal Methods (FM). LNCS, vol. 5014, pp. 68–83. Springer, Heidelberg (2008)

    Google Scholar 

  27. Rushby, J., Owre, S., Shankar, N.: Subtypes for Specifications: Predicate Subtyping in PVS. IEEE Transactions on Software Engineering 24(9), 709–720 (1998)

    Article  Google Scholar 

  28. Schieder, B., Broy, M.: Adapting calculational logic to the undefined. The Computer Journal 42(2), 73–81 (1999)

    Article  MATH  Google Scholar 

  29. Spivey, J.M.: Understanding Z: a specification language and its formal semantics. Cambridge University Press, Cambridge (1988)

    MATH  Google Scholar 

  30. Sutcliffe, G., Suttner, C.B., Yemenis, T.: The TPTP Problem Library. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 252–266. Springer, Heidelberg (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ETH Zurich, Switzerland

    Ádám Darvas, Farhad Mehta & Arsenii Rudich

Authors
  1. Ádám Darvas
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Farhad Mehta
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Arsenii Rudich
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Alessandro Armando Peter Baumgartner Gilles Dowek

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Darvas, Á., Mehta, F., Rudich, A. (2008). Efficient Well-Definedness Checking. In: Armando, A., Baumgartner, P., Dowek, G. (eds) Automated Reasoning. IJCAR 2008. Lecture Notes in Computer Science(), vol 5195. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71070-7_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-71070-7_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-71069-1

  • Online ISBN: 978-3-540-71070-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation