Skip to main content
SpringerLink
Log in
Book cover

Modern Mathematical Methods and High Performance Computing in Science and Technology pp 45–70Cite as

Using MathLang to Check the Correctness of Specifications in Object-Z

  • Conference paper
  • First Online:

  • 782 Accesses

Part of the book series: Springer Proceedings in Mathematics & Statistics ((PROMS,volume 171))

Abstract

The importance of thoroughly checking software specifications is widely recognised in the software industry, particularly for software involved in dealing with safety critical systems. The MathLang project has been successfully used to check large mathematical texts for correctness in a stepwise fashion. Currently MathLang is being tested for checking the correctness of formal specifications written in Z. Since object-orientation is a vital concept for software specification, it is important that the tools available for thoroughly checking specifications can be used with a language powerful enough to express specifications for object-oriented software. This paper aims to test the usefulness of MathLang for the computerisation of formal specifications written in Object-Z.

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   89.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   119.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover 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

References

  1. Frentiu, M., Correctness, a very important quality factor in programming. Stud. Univ. Babes-Bolyai Ser. Inf. L(1), 11–20 (2005)

    Google Scholar 

  2. MacKenzie, D.: Computer-related accidental death: an empirical exploration. Sci. Public Policy 21(5), 233–248 (1994)

    Google Scholar 

  3. Dijkstra, E.W.: Notes on Structured Programming. Technological University Eindhoven, Department of Mathematics (1970)

    Google Scholar 

  4. DeMillo, R.A., Lipton, R.J., Perlis, A.J.: Social processes and proofs of theorems and programs. Commun. ACM 22(5), 271–280 (1979)

    Google Scholar 

  5. Li, Y., Pan, X., Hu, T., Sung, S.Y., Yuan, H.: Specifying complex systems in Object-Z: a case study of petrol supply systems. J. Softw. 9(7), 11 (2014)

    Google Scholar 

  6. Preibusch, S., Kamller, F.: Checking the TWIN Elevator System by Translating Object-Z to SMV. Formal Methods for Industrial Critical Systems: 12th International Workshop, FMICS, pp 38–57 (2007)

    Google Scholar 

  7. ISO/IEC 13568, Information technology Z formal specification notation Syntax, type system and semantics (2002)

    Google Scholar 

  8. Brucker, A.D., Rittinger, F., Wolff, B.: HOL-Z 2.0: a proof environment for Z-specifications. J. Univers. Comput. Sci. 9(2), 152–172 (2003)

    Google Scholar 

  9. https://www.brucker.ch/projects/hol-z/. Accessed April 2015

  10. Jones, R.: Methods and tools for the verification of critical properties. In: 5th Refinement Workshop, Springer Workshops in Computing (2004)

    Google Scholar 

  11. Arthan, R.: On Formal Specification of a Proof Tool. Lemma 1 Ltd

    Google Scholar 

  12. Kamareddine, F., Wells, J., Zengler, C., Barendregt, H.: Computerising mathematical text. Computational Logic. Handbook of the History of Logi, vol. 9, pp. 343–396. Elsevier (2014)

    Google Scholar 

  13. Burski, L., Kamareddine, F.: Translating Z into Isabelle Syntax using MathLang. Heriot Watt University, ULTRA Group (2015)

    Google Scholar 

  14. Smith, G.: The Object-Z Specification Language. Software Verification Research Centre, University of Queensland (1999)

    Google Scholar 

  15. Parker, T.: TOZE - A Graphical Editor for the Object-Z Specification Language with Syntax and Type Checking Capabilities. Masters Thesis, University of Wisconsin-La Crosse (2008)

    Google Scholar 

  16. Kimber, T.: Object-Z to Perfect Developer. Masters Thesis. Imperial College London, London (2007)

    Google Scholar 

  17. http://www.eschertech.com/products/perfect_developer.php. Accessed April 2015

  18. Oz Style File. http://web.mit.edu/tex/stuff/latex-dist/psnfss/oz.sty. Accessed August (2015)

  19. Community Z Tools. http://czt.sourceforge.net/. Accessed August (2015)

Download references

Author information

Authors and Affiliations

  1. School of Mathematical and Computer Sciences, Heriot Watt University, Edinburgh, EH14 4AS, UK

    David Feller, Fairouz Kamareddine & Lavinia Burski

Authors
  1. David Feller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fairouz Kamareddine
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lavinia Burski
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Fairouz Kamareddine .

Editor information

Editors and Affiliations

  1. Department of Applied Mathematics, Raj Kumar Goel Institute of Technology, Ghaziabad, Uttar Pradesh, India

    Vinai K. Singh

  2. Department of Mathematics and Statistics, University of Victoria, Victoria, British Columbia, Canada

    H.M. Srivastava

  3. Dipartimento di Matematica, University of Turin, Torino, Italy

    Ezio Venturino

  4. High Performance Computing Center (HLRS), University of Stuttgart, Stuttgart, Baden-Württemberg, Germany

    Michael Resch

  5. Department of Mathematics, Netaji Subhas Institute of Technology, New Delhi, India

    Vijay Gupta

Appendices

Appendices

A Credit Card ZCGa

figure e
figure f

B CheckIn ZCGa

figure g
figure h

C Rich Tea ZCGa

figure i
figure j
figure k
figure l

D OZCGa file

figure m
figure n

E A Breakdown of the Specification for Checking

figure o
figure p
figure q
figure r

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer Science+Business Media Singapore

About this paper

Cite this paper

Feller, D., Kamareddine, F., Burski, L. (2016). Using MathLang to Check the Correctness of Specifications in Object-Z. In: Singh, V., Srivastava, H., Venturino, E., Resch, M., Gupta, V. (eds) Modern Mathematical Methods and High Performance Computing in Science and Technology. Springer Proceedings in Mathematics & Statistics, vol 171. Springer, Singapore. https://doi.org/10.1007/978-981-10-1454-3_5

Download citation

Publish with us

Policies and ethics

Search

Navigation