Skip to main content
SpringerLink
Log in

A Theory of Classes from the Theoretical Foundations of LePUS3

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2011)

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

Included in the following conference series:

  • 869 Accesses

Abstract

LePUS3 is a formal design description language for specifying decidable (i.e. automatically verifiable) properties of object-oriented design. LePUS3 has been successfully applied to both design verification and reverse engineering applications. However, LePUS3 is becoming over zealously pragmatic. Its current definition is inflexible, limiting is expressivity, extensibility and reasoning capabilities. We present a new theory of classes derived from the theoretical foundations of LePUS3, and defined in the Typed Predicate Logic. The expressive power of our theory is demonstrated by specifying and reasoning over design patterns.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Beck, K., Cunningham, W.: Using pattern languages for Object-Oriented programs. In: OOPSLA 1987 workshop on the Specification and Design for Object-Oriented Programming, Florida, USA (September1987)

    Google Scholar 

  2. Blewitt, A., Bundy, A., Stark, I.: Automatic verification of design patterns in Java. In: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering, pp. 224–232. ACM, CA (2005)

    Chapter  Google Scholar 

  3. Craig, I.: The Interpretation of Object-Oriented Programming Languages, 2nd edn. Springer, Heidelberg (2000)

    Book  MATH  Google Scholar 

  4. Eden, A.H., Gasparis, E., Nicholson, J.: LePUS3 and Class-Z reference manual. Technical Report CSM-474, School of Computer Science and Electronic Engineering, University of Essex (December 2007); ISSN 1744-8050

    Google Scholar 

  5. Eden, A.H., Nicholson, J.: Codecharts: Roadmaps and Blueprints for Object-Oriented Programs. Wiley-Blackwell (2011)

    Google Scholar 

  6. Gamma, E., Helm, R., Johnson, R., Vlissides, J.M.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Professional, Reading (1994)

    MATH  Google Scholar 

  7. Gasparis, E.: Design Navigation: Recovering Design Charts From Object-Oriented Programs. PhD, University of Essex (February 2010)

    Google Scholar 

  8. Hinchey, M., Jackson, M., Cousot, P., Cook, B., Bowen, J.P., Margaria, T.: Software engineering and formal methods. Communications of the ACM 51(9), 54–59 (2008)

    Article  Google Scholar 

  9. Huth, M.R.A., Ryan, M.D.: Logic in Computer Science: Modelling and Reasoning about Systems, 2nd edn. Cambridge University Press, Cambridge (2000)

    MATH  Google Scholar 

  10. Maplesden, D., Hosking, J., Grundy, J.: A visual language for design pattern modeling and instantiation. In: Design Patterns Formalization Techniques. IGI Global, USA (2007)

    Google Scholar 

  11. Nicholson, J.: On the Theoretical Foundations of LePUS3 and its Application to Object-Oriented Design Verification. PhD, University of Essex, UK (2011)

    Google Scholar 

  12. Nicholson, J., Gasparis, E., Eden, A.H., Kazman, R.: Automated verification of design patterns in LePUS3. In: Proceedings of the 1st NASA Formal Methods Symposium, pp. 76–85. NASA, Moffett Field (2009)

    Google Scholar 

  13. Schmidt, D.C., Fayad, M., Johnson, R.E.: Software patterns. Communications of the ACM 39(10), 37–39 (1996)

    Article  Google Scholar 

  14. Spivey, J.M.: The Z Notation: a Reference Manual, 2nd edn. Prentice-Hall, Englewood Cliffs (1992)

    MATH  Google Scholar 

  15. Sun Microsystems Inc.: Java 6 SDK: standard edn. documentation (2006)

    Google Scholar 

  16. Taibi, T.: Design Patterns Formalization Techniques. IGI Global, Hershey (2007)

    Book  Google Scholar 

  17. Taivalsaari, A.: On the notion of inheritance. ACM Computing Surveys 28(3), 438–479 (1996)

    Article  Google Scholar 

  18. Turner, R.: Computable Models. Springer, Heidelberg (2009)

    Book  MATH  Google Scholar 

  19. Turner, R.: Logic and computation (May 2010), http://cswww.essex.ac.uk/staff/turnr/Mypapers/TPLessex.pdf

  20. Wing, J.M.: A specifier’s introduction to formal methods. Computer 23(9), 8–23 (1990)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Essex, UK

    Jonathan Nicholson

Authors
  1. Jonathan Nicholson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, Teesside University, UK

    Shengchao Qin

  2. LMAM and Department of Informatics, School of Mathematical Sciences,, Peking University, China

    Zongyan Qiu

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nicholson, J. (2011). A Theory of Classes from the Theoretical Foundations of LePUS3. In: Qin, S., Qiu, Z. (eds) Formal Methods and Software Engineering. ICFEM 2011. Lecture Notes in Computer Science, vol 6991. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24559-6_35

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-24559-6_35

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-24558-9

  • Online ISBN: 978-3-642-24559-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation