🚀 go-pugleaf

I queried comp.specification as follows:

>I'd like to get bibliographic references, and people's recommendations
>for introductory texts for the specification languages in the subject
>line.   The texts are intended for students doing individual study.
>[Perhaps there's a FAQ containing this?]

I summarize the reponses as (an untested!) bib file below.
I draw the readers attention to the entries marked "Highly
recommended", which I attached to an entry which was
highly recommended by a respondant, or showed up in several respondant's lists.
I am (as yet) in no position to judge, although I am
following the recommendation myself.

There was also a response from David Wright, a comp.specification 
reader about Z documents, which I append to the end.

Thanks very much to the respondents.


% File containing bibliographic entries about specification languages
% Thanks to:
%  pyoung@axion.bt.co.uk
%  nico@dutiba.tudelft.nl
%  drabik@be.tech.ascom.ch
%  jcrw@fmg.bt.co.uk
%  srinivas@kestrel.edu
%  S.P.vandeBurgt@research.ptt.nl

@book{bjorner:development,
        author =        "D. Bj{\o}rner and C. B. Jones",
        year =          "1982",
        publisher =     "Prentice Hall International",
        title =         "{Formal Specification and Software Development}",
        length =        "501 pages",
}

@article(Bolognesi:LOTOS-introduction,
  author     = "Tomasso Bolognesi and Ed Brinksma",
  title      = "{Introduction to the ISO specification language LOTOS}",
  journal    = "Computer Networks and ISDN Systems",
  volume     = 14,
  number     = ,
  pages      = "25-59",
  month      = ,
  year       = 1987,
  note       = "North-Holland",
  annotation = {Knowledgeable internet reader: There is a very useful introductory paper}
)

@inproceedings(Brinksma:tutorial,
        author =        "E. Brinksma",
        booktitle =     "Protocol Specification, Testing and Verification V",
        year =          "1986",
        editor =        "M. Diaz",
        publisher =     "Elsevier Science Publisher BV",
        pages =         "171-194",
        title =         "A tutorial on {LOTOS}",
        volume =        "V",
)

@misc{iso:lotos,
        title  =        "{LOTOS, A formal description technique
                          based on the temporal ordering of observational
                          behaviour}",
        author  =       "{ISO-8807}",
        year  =         "1988"
}

@book(Potter91a:Z-introduction,
  author = 	"Ben Potter and David Till and Jane Sinclair",
  title = 	"An Introduction to formal specification and Z",
  publisher = 	"Prentice-Hall",
  year = 	"1991"
  annotation = {Highly recommended}
)

@book(Wordsworth:Z-introduction,
  author =      "J. B. Wordsworth",
  title =       "Software Development with Z",
  publisher =   "Addison Wesley",
  year =        "1992",
  series =      "International Computer Science series",
  note =        "ISBN 0-210-62757-4"
  annotation = {Highly recommended}
)

@book(Woodcock:Z-introduction,
	author = "James C.P. Woodcock and Martin Loomes",
	title = "Software Engineering Mathematics: Formal Methods Demystified",
	publisher = "Pitman Publishing Ltd",
	address = "London, UK",
	year = "1988",
	note = "ISBN 0273026739"
)

@book(jones90a:VDM-classic,
   key          = "Jones 90",
   author       = "C.B. Jones",
   title        = "{Systematic Software Development using VDM (2nd edition)}",
   year         = "1990",
   annotation       = "",
   publisher    = "Prentice-Hall International"
)

@book{jones90b:VDM-case-studies,
   key          = "Jones 90",
   author       = "C.B. Jones, R. Shaw (editors)",
   title        = "{Case Studies in VDM}",
   year         = "1990",
   annotation       = "",
   publisher    = "Prentice-Hall International"
}

@book(hekmatpour88:VDM-in-prototyping,
   key          = "Hekmatpour 88",
   author       = "S. Hekmatpour, D. Ince",
   title        = "{Software Prototyping, Formal Methods and VDM}",
   publisher    = addison,
   year         = "1988",
   annotation       = "VDM and prototyping"
)

@book(andrews91a:VDM-introduction,
   key          = "Andrews 91",
   author       = "Derek Andrews, Darell Ince",
   title        = "{Practical Formal Methods with VDM}",
   publisher    = "McGraw Hill",
   year         = "1991",
   size         = "450",
   annotation   = "A recent introductory text"
)

@book(dawes91:VDM-reference,
   key          = "Dawes 91",
   author       = "John Dawes",
   title        = "{The VDM-SL Reference Guide}",
   publisher    = pitman,
   year         = "1991",
   size         = "217",
   annotation   = "A reference manual of the language, complete
  		but probably not for beginners"
)

@article(Logrippo92:LOTOS-introduction,
  author     = "L. Logrippo and M. Faci and M. Haj-Hussein"
  title      = "{An introduction to LOTOS: learning by examples}",
  journal    = "Computer Networks and ISDN Systems",
  volume     = 23,
  number     = ,
  pages      = "325-342",
  month      = ,
  year       = 1992,
  note       = "North-Holland",
  annotation = {}
)

@misc(Turner90:LOTOS-tutorial,
  author     = "Ken Turner",
  title      = "{The Formal Specification Language LOTOS: A Course for Users}",
  year       = 1990,
  note       = "",
  annotation = {Internet reader: For Lotos there is at present a lack
		of introductory texts. The best tutorial I have seen
		is produced by the University of Stirling, Scotland 
                and written by Ken Turner, kjt@cs.stir.ac.uk..
                I have heard it rumoured that this may be coming out
                in book form but cannot be sure.}
)

@incollection(abrial:z,
  author     = "J. R. Abrial",
  title      = "Programming as a mathematical exercise",
  booktitle  = "Mathematical Logic and Programming Languages",
  editor     = "C. A. R. Hoare and J. C. Shepherdson",
  publisher  = "Prentice Hall",
  pages      = "113-137",
  year       = 1985
)

@book(hayes:z,
  editor     = "Ian Hayes",
  title      = "Specification Case Studies",
  publisher  = "Prentice Hall",
  year       = 1985
)

@article(morgan:unix-filesystem,
  author     = "Carroll Morgan and Bernard Sufrin",
  title      = "Specification of the {UNIX} Filing System",
  journal    = tse,
  volume     = "SE-10",
  number     = 2,
  pages      = "128-142",
  month      = mar,
  year       = 1984
)

@book(spivey:manual,
  author     = "J. M. Spivey",
  title      = "The Z Notation: A Reference Manual",
  publisher  = "Prentice Hall",
  address    = "Englewood Cliffs, NJ",
  year       = 1989
)

@book(spivey:z,
  author     = "J. M. Spivey",
  title      = "Understanding Z: A specification language and its
		formal semantics",
  publisher  = "Cambridge University Press",
  address    = "Cambridge",
  year       = 1988
)

@article(sufrin:editor,
  author     = "Bernard Sufrin",
  title      = "Formal Specification of a Display-Oriented Text
		Editor",
  journal    = "Science of Computer Programming",
  volume     = 1,
  pages      = "157-202",
  year       = 1982,
  annotation = {Formal spec of an editor in Z. Extensive use of
		higher-order functions. E.g. direction of move,
		insert, delete, etc., move to boundary at character,
		word, line, document. Interesting observation: perfrom
		a domain analysis which describes entire
		functionality; in an actual implementation, use only
		some of the functions, e.g., no insert left, kill line
		to left, etc.}
)

------------------------ comp.specification.z FAQ ------------------------

From: zforum-request@comlab.ox.ac.uk
Subject: comp.specification.z Frequently Asked Questions (Monthly)
Date: 1 May 92 01:01:02 GMT
Organization: Oxford University Computing Laboratory, UK

<<stuff deleted>>

~Subject: What has been published about Z?

Publications: A BibTeX bibliography of Z-related publications is
available from the PRG archive server (see above).  Information on
Oxford University Programming Research Group (PRG) Technical Monographs
and Reports, including many on Z, is available from the librarian on
<library@comlab.ox.ac.uk>.
  The following books specifically concerning Z have been or are due to       |
be published (in approximate chronological order):                            |

  I.Hayes (ed.), Specification case studies, Prentice Hall International
      Series in Computer Science, 1987.
  J.M.Spivey, Understanding Z: a specification language and its formal
      semantics, Cambridge University Press, 1988.
  D.Ince, An introduction to discrete mathematics and formal system
      specification, Oxford University Press, 1988.
  J.C.P.Woodcock & M.Loomes, Software engineering mathematics, Pitman, 1988.
  J.M.Spivey, The Z notation: a reference manual, Prentice Hall
      International Series in Computer Science, 1989. +
  A.Diller, Z: an introduction to formal methods, Wiley, 1990.
  J.E.Nicholls (ed.), Z user workshop, Oxford 1989, Springer-Verlag,
      Workshops in Computing, 1990.
  B.Potter, J.Sinclair & D.Till, An introduction to formal specification
      and Z, Prentice Hall International Series in Computer Science, 1991.
  D.Lightfoot, Formal specification using Z, MacMillan, 1991.
  A.Norcliffe & G.Slater, Mathematics for software construction,
      Ellis Horwood, 1991.
  J.E.Nicholls (ed.), Z user workshop, Oxford 1990, Springer-Verlag,
      Workshops in Computing, 1991.
  I.Craig, The formal specification of advanced AI architectures,
      Ellis Horwood, September 1991.
  M.Imperato, An introduction to Z, Chartwell-Bratt, 1991.
To appear:                                                                    |
  I.Hayes (ed.), Specification case studies, 2nd ed., Prentice Hall
      International Series in Computer Science, 1992.
  J.A.McDermid & P.Whysall, Formal system specification and implementation
      using Z, Prentice Hall International Series in Computer Science, 1992.
  J.M.Spivey, The Z notation: a reference manual, 2nd ed., Prentice Hall
      International Series in Computer Science, 1992. +
  J.E.Nicholls (ed.), Z user workshop, York 1991, Springer-Verlag,
      Workshops in Computing, 1992.
  J.C.P.Woodcock, Using standard Z, Prentice Hall International Series
      in Computer Science, 1992-93.

  + Widely considered as the current de facto standard for Z.

-- 
Ira Baxter   email: baxter@slcs.slb.com   ph: 1-512-331-3714
Schlumberger Laboratory for Computer Science
8311 North RR 620   [for snail mail, use PO Box 200015 instead]
Austin, Texas, 78720