Re: Applications for Category Theory

[categories <cat-dist@mta.ca>]

Date: Thu, 28 Aug 1997 13:29:08 -0700 (PDT)
From: Joseph Goguen <goguen@cs.ucsd.edu>

Im enjoying the discussion of CT and CS or SWE, although it seems to me to be
a bit theoretical.  Id like to mention three tools, real implemented software
systems that have been and are being used in real software engineering:
SpecWare \cite{specware}, LILEANNA \cite{traczth,tracz93}, and TOOR
\cite{toor}.  

All are based on a category theoretic module system called parameterized
programming \cite{ppp}.  The idea is that specs are theoires and that putting
specs together is just colimit; this goes back to work on general systems
theory from the late 1960s \cite{gst} and work of Clear from the late 1970s
\cite{bg77,bg80sh}.

SpecWare actually has colimit as a top level command, but it fails to provide
all the module operations which make parameterized programming so powerful.
However, it can generate code from sufficiently detailed specs, and has very
good documentation, a good user base, and a verification capability.  It is
produced by Kestrel Inst.

LILEANNA fully implements parameterized programming and can compose Ada
modules, but it only generates glue code.  It was built at Martin-Marietta,
and has been used for helicopter navigation software.

TOOR supports requirements evolution and full parameterized programming,
without verification, but with a good user interface.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@incollection(bg77,
title = "Putting Theories together to Make Specifications",
author = "Rod Burstall and Joseph Goguen",
booktitle = "Proceedings, Fifth International Joint Conference on Artificial
  Intelligence",
editor = "Raj Reddy",
publisher = "Department of Computer Science, Carnegie-Mellon University",
year = 1977,
pages = "1045--1058")

@incollection(bg80sh,
author = "Rod Burstall and Joseph Goguen",
title = "The Semantics of {C}lear, a Specification Language",
booktitle = "Proceedings, 1979 Copenhagen Winter School on
  Abstract Software Specification",
editor = "Dines Bjorner",
note = "Lecture Notes in Computer Science, Volume 86",
publisher = "Springer",
pages = "292--332",
year = 1980)

@techreport(specware,
title = "Spec{W}are Language Manual, Version 2.0",
author = "Y.V.\ Srinivas and Richard J{\"u}llig",
institution = "Kestrel",
year = 1996)

@inproceedings(tracz93,
author = "Will Tracz",
title = "{\sc lileanna}: a Parameterized Programming Language",
booktitle = "Proceedings, Second International Workshop on Software Reuse",
month = "March", 
year = 1993,
note = "Lucca, Italy",
pages = "66--78")
		  
@phdthesis(traczth,
title = "Formal Specification of Parameterized Programs in {\sc lilleanna}",
author = "William Joseph Tracz",
school = "Stanford University",
year = 1997)

@incollection(gst71,
title = "Mathematical Representation of Hierarchically Organized Systems",
author = "Joseph Goguen",
year = 1971,
editor = "E. Attinger",
booktitle = "Global Systems Dynamics",
publisher = "S. Karger",
location = "Basel",
city = "Basil",
pages = "112--128")

@incollection(gst73,                          
title = "Categorical Foundations for General Systems Theory",
author = "Joseph Goguen",
booktitle = "Advances in Cybernetics and Systems Research",
editor = "F. Pichler and R. Trappl",
year = 1973,
publisher = "Transcripta Books",
location = "London",
pages = "121--130")

@article(toor,
title = "An Object-Oriented Tool for Tracing Requirements",
author = "Francisco Pinheiro and Joseph Goguen",
journal = "IEEE Software",
note = "Special issue of papers from ICRE '96",
year = "March 1996",
pages = "52--64")

@incollection(ppp,
title = "Principles of Parameterized Programming",
author = "Joseph Goguen",
booktitle = "Software Reusability, Volume {I}: Concepts and Models",
editor = "Ted Biggerstaff and Alan Perlis",
publisher = "Addison Wesley",
year = 1989,
pages = "159--225")