This Article 
 Bibliographic References 
 Add to: 
The Formal Specification of a Small Bookshop Information System
February 1988 (vol. 14 no. 2)
pp. 263-272

A specification, and its development, for a small bookshop information system are discussed. the specification is presented using mathematics and the scheme calculus of C. Morgan and B. Sufrin. An insight is given into how the specification was developed and why a formal specification is appropriate.

[1] R. M. Buratall, "An informal introduction to specification using Clear," inThe Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore, Eds. New York: Academic, 1981.
[2] D. W. Bustard, "Software engineering notes," Queen's Univ., Belfast, Ireland, 1985.
[3] Euclid,Elements, c. 330-320 B.C.
[4] J. V. Guttag, J. J. Homing, and J. M. Wing, "Larch in five easy pieces," Digital Corp., Res. Rep. 5, 1985.
[5] I. Hayes, "Examples of specification using mathematics,"FACS-FACTS Newslett., Mar. 1985.
[6] C.B. Jones,Systematic Software Development Using VDM, Prentice Hall Int'l, 1986.
[7] R. A. Kemmerer, "Testing formal specifications to detect design errors,"IEEE Trans. Software Eng., vol. SE-11, no. 1, pp. 32-43, Jan. 1985.
[8] C. Morgan and B. Sufrin, "Specification of the UNIX filing system,"IEEE Trans. Software Eng., vol. SE-10, no. 2, pp. 128-142, Mar. 1984.
[9] C. Morgan, "The Schema language," Programming Res. Group, Oxford Univ., July 1984.
[10] B. Sufrin, C. Morgan, I. Sorensen, and I. Hayes, "Notes for a Z handbook," Programming Res. Group, Oxford Univ., Jan. 1985.

Index Terms:
set theory; formal specification; small bookshop information system; scheme calculus; programming theory; software engineering
D. Gray, "The Formal Specification of a Small Bookshop Information System," IEEE Transactions on Software Engineering, vol. 14, no. 2, pp. 263-272, Feb. 1988, doi:10.1109/32.4644
Usage of this product signifies your acceptance of the Terms of Use.