LCL type specifications

   From: Paolo Ciancarini <cianca@DI.UniPi.IT>
   Date: Mon, 11 Jul 1994 16:03:23 +0100 (METDST)

   More precisely, we need info about different use of LCL
   abstract types:
		   - Mutable
		   - Immutable
		   - Spec

   When is better to use one instead of the others ?
   We are very interested in having semantics hints and some examples.

The mutability of an abstract type is a design choice: it depends on
your modeling needs.  An immutable type is often used to model objects
that have fixed values, e.g., numbers.  A mutable type is useful for
modeling real-world objects whose values change over time.

An LCL spec type is local to a specification module.  It is useful if
you don't want clients of the module to have access to it.  Spec types
need not be implemented.  

A reference you may find useful is my PhD thesis.  In particular,
Chapter 4 describes the LCL specs of a case study.  Chapter 7
describes the semantics of LCL.

   AUTHOR = {Yang Meng Tan},
   TITLE = {Formal Specification Techniques for Promoting Software
Modularity, Enhancing Software Documentation, and Testing
   INSTITUTION = {MIT Laboratory for Computer Science},
   YEAR = {1994},
   TYPE = {TR},
   NUMBER = {619},
   MONTH = {June},
   NOTE = {PhD Thesis, EECS Dept}

thesis abstract URL: http://larch-www.lcs.mit.edu:8001/~ymtan/phd-abstract.html
thesis postscript URL: ftp://larch.lcs.mit.edu/pub/ymtan/mit-lcs-tr-619.ps.Z

- Yang Meng Tan

Follow-Up(s): Reference(s):