More Web Proxy on the site http://driver.im/

research-article

Open access

Modularising the specification of a small database system in extended ML

Author:

Edmund KazmierczakAuthors Info & Claims

Formal Aspects of Computing, Volume 4, Issue 1

Pages 100 - 142

https://doi.org/10.1007/BF01214958

Published: 01 January 1992 Publication History

Abstract

A case study in the modular specification and refinement of a small database system is presented in Extended ML. Two similar requirements specifications are given and a program development step from each these is presented. The structure resulting from the first program development step is similar to that given in [FiJ90] and is presented as an answer to the challenge problem given in that paper, while the second development step is presented as a possible alternative which is more suited to the Extended ML style of program development. In the context of these two development steps the module facilities of Extended ML, their role in specification and program development and their ability to meet the challenge of [FiJ90] are examined.

References

References

[1]

Cardelli L. and Wegner P. On Understanding Types, Data Abstraction and Polymorphism Computing Surveys 1985 17 4 471-522

Digital Library

[2]

Date, C.J.:An Introduction to Database Systems. Addison-Wesley, 1986.

[3]

Damas, L. and Milner, R.: Principle Type Schemes and Functional Programs. InPrinciples of Programming Languages, 207–212, 1982.

[4]

Ehrig, H. and Mahr. B.:Fundamentals of Algebraic Specification 1. EATCS: Monographs on Theoretical Computer Science. Springer-Verlag, 1985.

[5]

Ehrig, H. and Mahr, B.:Fundamentals of Algebraic Specification 2: Module Specifications and Constraints. EATCS: Monographs on Theoretical Computer Science. Springer-Verlag, 1990.

[6]

Fitzgerald, J. S. and Jones, C. B.: Modularising the Formal Description of a Database System. Technical Report UMCS-90-1-1, University of Manchester, January 1990.

[7]

Goguen, J. A. and Burstall, R. M.: The Semantics of Clear, A Specification Language. InAbstract Software Specifications, LNCS 86. Springer-Verlag, 1980.

[8]

Harper, R.: Introduction to Standard ML. Technical Report ECS-LFCS-86-14, University of Edinburgh, November 1986.

[9]

Harper, R., Milner, R. and Tofte, M.:The Definition of Standard ML. The MIT Press, 1990.

[10]

Jones, C.B.:Systematic Software Development Using VDM. Prentice-Hall International Series in Computer Science. Prentice-Hall International, 1986.

[11]

MacQueen, D.: Modules for Standard ML. Technical Report ECS-LFCS-86-2, University of Edinburgh, March 1986.

[12]

Milner, R.: A Theory of Type Polymorphism in Programming. Internal Report CSR-9-77, University of Edinburgh, Department of Computer Science, September 1977.

[13]

Milner, R. and Tofte, M.:Commentary on Standard ML. MIT Press, 1990.

[14]

Parnas D. On the Criteria to be Used in Decomposing Systems into Modules Communications of the ACM 1972 5 12 1053-1058

Digital Library

[15]

Sannella, D.: Formal Program Development in Extended ML for the Working Programmer. Technical Monograph ECS-LFCS-89-102, Laboratory for the Foundations of Computer Science, December 1989.

[16]

Sannella, D. and Burstall, R.: Structured Theories in LCF. InProceedings of the 8th Colloq. on Trees in Algebra and Programming, LNCS 159, 377–391. Springer Verlag, 1983.

[17]

Sannella, D., Sokolowski, S. and Tarlecki, A.: Toward Formal Development of Programs from Algebraic Specifications: Parameterisation Revisited. Technical Report Report 6/90, University of Bremen, 1990.

[18]

Sannella D. T. and Tarlecki A. On Observational Equivalence and Algebraic Specification Journal of Computer and System Sciences 1987 34 150-178

Digital Library

[19]

Sannella D. and Tarlecki A. Building Specifications in an Arbitrary Institution Information and Control 1988 76 165-210

Digital Library

[20]

Sannella, D. and Tarlecki, A.: Toward Formal Development of ML Programs: Foundations and Methodology: 0-Extended Abstract. InProceedings of the Colloquium on Current Issues in Programming Languages, LNCS 352, 375–389. Springer Verlag, 1989.

[21]

Sannella, D. and Tarlecki, A.: A Kernel Specification Formalism with Higher Order Parameterisation. In7th Workshop on Specification of Abstract Data Types. Lecture Notes in Computer Science, to appear. Springer Verlag, 1991.

[22]

Tofte, M.: Four Lectures on ML. Technical Report ECS-LFCS-89-73, University of Edinburgh, March 1989.

[23]

Walshe, A.: NDB: The formal specification and rigorous design of a single user database. In: C. B. Jones and R. F. C. Shaw, (eds),Case Studies in Systematic Software Development, 12–45. Prentice Hall International, 1990.

[24]

Winterbottom N. and Sharman G. C. H. NDB:Non-programmer database facility Technical Report IBM TR.12.179 1979 England IBM Hursley Laboratory

Cited By

Kahrs SSannella DTarlecki A(1997)The definition of extended MLTheoretical Computer Science10.1016/S0304-3975(96)00163-6173:2(445-484)Online publication date: 28-Feb-1997
https://dl.acm.org/doi/10.1016/S0304-3975%2896%2900163-6
Sannella DTarlecki A(1997)Essential concepts of algebraic specification and program developmentFormal Aspects of Computing10.1007/BF012110849:3(229-269)Online publication date: 1-May-1997
https://dl.acm.org/doi/10.1007/BF01211084

Recommendations

Design and Implementation of a Tool for Specifying Specification in SOFL
Revised Selected Papers of the Second International Workshop on Structured Object-Oriented Formal Language and Method - Volume 7787

Structure Object-oriented Formal Language SOFL is not just a formal language for writing formal specification. It is also an approach and a methodology. SOFL provides a three-step approach for modelling a software system using formal specification. ...
Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of ...
Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles
TASE '08: Proceedings of the 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering

Situated Multi-Agents Systems (MAS), and other Agent-based systems, are often complex. Formal reasoning is needed to ensure their correctness and structure their development. Event-B is a formal method with tool support allowing a stepwise development ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 4, Issue 1

Jan 1992

147 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© BCS 1992.

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

2
Total Citations
View Citations
39
Total Downloads

Downloads (Last 12 months)17
Downloads (Last 6 weeks)2

Reflects downloads up to 07 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Kahrs SSannella DTarlecki A(1997)The definition of extended MLTheoretical Computer Science10.1016/S0304-3975(96)00163-6173:2(445-484)Online publication date: 28-Feb-1997
https://dl.acm.org/doi/10.1016/S0304-3975%2896%2900163-6
Sannella DTarlecki A(1997)Essential concepts of algebraic specification and program developmentFormal Aspects of Computing10.1007/BF012110849:3(229-269)Online publication date: 1-May-1997
https://dl.acm.org/doi/10.1007/BF01211084

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents