research-article

Open access

VDM and Z: A comparative case study

Author:

Ian HayesAuthors Info & Claims

Formal Aspects of Computing, Volume 4, Issue 1

Pages 76 - 99

https://doi.org/10.1007/BF01214957

Published: 01 January 1992 Publication History

PDF eReader

Abstract

The specification notations of VDM and Z are closely related. They both use model-based specification techniques and share a large part of their mathematical notation. However, the approaches taken to writing specifications differ in other, more subtle, ways.

We present a comparative case study of VDM and Z for specifying database systems. John Fitzgerald and Cliff Jones in their paper entitled “Modularising the formal description of a database system” in the proceedings ofVDM '90: VDM and Z (LNCS Vol. 428, Springer-Verlag) provide the basis for the comparison. We present equivalent Z specifications to the VDM specifications contained in their paper.

The approach taken in writing the Z specifications is to reuse as much as possible of the Z mathematical toolkit and to build the system specification from specifications of components of the system.

In their paper, Fitzgerald and Jones emphasise their modularisation facilities. While the facilities for modularisation in Z are not as powerful, they are adequate for the specification of the database systems presented.

References

[1]

Fitzgerald, J.S. and Jones, C.B.: Modularizing the Formal Description of a Database System. In:VDM'90: VDM and Z-Formal Methods in Software Development, D. Bjørner, C. A. R. Hoare, and H. Langmaack (eds.), pp. 189–210, Springer-Verlag, 1990. Lecture Notes in Computer Science, Vol. 428.

Google Scholar

[2]

Flinn, L. W. and Sørensen, I. H.: CAVIAR: A Case Study in Specification. In:Specification Case Studies, I. J. Hayes (ed.), pp 141–188, Prentice Hall International, 1987.

Google Scholar

[3]

Hayes, I. J. (ed.):Specification Case Studies. Prentice Hall International, 1987.

Google Scholar

[4]

Sufrin B. A. and Hughes J. A Tutorial Introduction to Relational Algebra Technical Report 1985 UK Programming Research Group, Oxford University

Google Scholar

[5]

Spivey, J. M.:The Z Notation: A Reference Manual. Prentice Hall International, 1989.

Google Scholar

[6]

Walshe, A.: NDB: The Formal Specification and Rigorous Design of a Single-User Database System. In:Case Studies in Systematic Software Development, C. B. Jones and R. C. F. Shaw (eds.), pp 11–45, Prentice Hall International, 1990.

Google Scholar

Cited By

View all

Li JLiu SLiu AHuang R(2021)Multilevel Traceability Links Establishments Between SOFL Formal Specifications and Java Codes Using Multi-dimensional Similarity Measures2021 IEEE 21st International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS54544.2021.00094(852-863)Online publication date: Dec-2021
https://doi.org/10.1109/QRS54544.2021.00094
Derrick JBoiten EDerrick JBoiten E(2018)ConclusionsRefinement10.1007/978-3-319-92711-4_12(263-269)Online publication date: 4-Sep-2018
https://doi.org/10.1007/978-3-319-92711-4_12
Jalila AMala D(2014)Object-oriented model-based specification languagesACM SIGSOFT Software Engineering Notes10.1145/2659118.265913239:5(1-4)Online publication date: 17-Sep-2014
https://dl.acm.org/doi/10.1145/2659118.2659132
Show More Cited By

Index Terms

VDM and Z: A comparative case study

Index terms have been assigned to the content through auto-classification.

Recommendations

Using KIDS as a tool support for VDM
ICSE '96: Proceedings of the 18th international conference on Software engineering

KIDS/VDM is an experimental environment that supports the synthesis of executable prototypes from VDM specifications. The development proceeds as a series of correctness preserving transformations under the strict control of the tool. A by-product of ...
A comparative evaluation of the Z, CSP, RSL, and VDM languages

The software engineering process has been described in many ways. Today, few of these deal specifically with the use of formal methods in software engineering. New software engineering uses formal specification languages in system analysis, requirement ...
Informal and Formal Requirements Specification Languages: Bridging the Gap

The differences between informal and formal requirements specification languages are noted, and the issue of bridging the gap between them is discussed. Using structured analysis (SA) and the Vienna development method (VDM) as surrogates for informal ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Formal Aspects of Computing Volume 4, Issue 1

Jan 1992

147 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 January 1992

Published in FAC Volume 4, Issue 1

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
85
Total Downloads

Downloads (Last 12 months)48
Downloads (Last 6 weeks)9

Reflects downloads up to 28 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Li JLiu SLiu AHuang R(2021)Multilevel Traceability Links Establishments Between SOFL Formal Specifications and Java Codes Using Multi-dimensional Similarity Measures2021 IEEE 21st International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS54544.2021.00094(852-863)Online publication date: Dec-2021
https://doi.org/10.1109/QRS54544.2021.00094
Derrick JBoiten EDerrick JBoiten E(2018)ConclusionsRefinement10.1007/978-3-319-92711-4_12(263-269)Online publication date: 4-Sep-2018
https://doi.org/10.1007/978-3-319-92711-4_12
Jalila AMala D(2014)Object-oriented model-based specification languagesACM SIGSOFT Software Engineering Notes10.1145/2659118.265913239:5(1-4)Online publication date: 17-Sep-2014
https://dl.acm.org/doi/10.1145/2659118.2659132
Wu NSimpson A(2014)Formal relational database design: an exercise in extending the formal template languageFormal Aspects of Computing10.1007/s00165-014-0299-626:6(1231-1269)Online publication date: 1-Nov-2014
https://dl.acm.org/doi/10.1007/s00165-014-0299-6
Derrick JBoiten EDerrick JBoiten E(2014)ConclusionsRefinement in Z and Object-Z10.1007/978-1-4471-5355-9_20(475-479)Online publication date: 2014
https://doi.org/10.1007/978-1-4471-5355-9_20
Wu NSimpson A(2010)Towards formally templated relational database representations in zProceedings of the Second international conference on Abstract State Machines, Alloy, B and Z10.1007/978-3-642-11811-1_27(363-376)Online publication date: 22-Feb-2010
https://dl.acm.org/doi/10.1007/978-3-642-11811-1_27
Bowen J(2005)Select Z bibliographyZUM '95: The Z Formal Specification Notation10.1007/3-540-60271-2_143(526-560)Online publication date: 1-Jun-2005
https://doi.org/10.1007/3-540-60271-2_143
Lindsay P(2005)On transferring VDM verification techniques to ZFME '94: Industrial Benefit of Formal Methods10.1007/3-540-58555-9_96(190-213)Online publication date: 1-Jun-2005
https://doi.org/10.1007/3-540-58555-9_96
Jones C(2005)Specification before satisfactionProceedings of the 4th international conference on Formal Specification and Development in Z and B10.1007/11415787_1(1-5)Online publication date: 13-Apr-2005
https://dl.acm.org/doi/10.1007/11415787_1
D'Inverno MLuck MGeorgeff MKinny DWooldridge M(2004)The dMARS ArchitectureAutonomous Agents and Multi-Agent Systems10.1023/B:AGNT.0000019688.11109.199:1-2(5-53)Online publication date: 1-Jul-2004
https://dl.acm.org/doi/10.1023/B%3AAGNT.0000019688.11109.19
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

References

Cited By

Index Terms

Recommendations

Using KIDS as a tool support for VDM

A comparative evaluation of the Z, CSP, RSL, and VDM languages

Informal and Formal Requirements Specification Languages: Bridging the Gap

Comments

Information

Published In

Publisher

Publication History

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Share

Share this Publication link

Share on social media

Affiliations