LCL type specifications

To: cianca@cs.unibo.it
Subject: LCL type specifications
From: ymtan@larch.lcs.mit.edu (Yang Meng Tan)
Date: Wed, 13 Jul 94 16:48:43 -0400
Cc: larch-interest@src.dec.com, ymtan@larch.lcs.mit.edu
Delivery-Date: Wed, 13 Jul 94 13:57:00 -0700
In-Reply-To: Paolo Ciancarini's message of Mon, 11 Jul 1994 16:03:23 +0100 (METDST) <9407111407.AA11776@inet-gw-2.pa.dec.com>
Reply-To: ymtan@larch.lcs.mit.edu

   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.

@TECHREPORT(TanPhD,
   AUTHOR = {Yang Meng Tan},
   TITLE = {Formal Specification Techniques for Promoting Software
Modularity, Enhancing Software Documentation, and Testing
Specifications},
   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):

Re: LCL type specifications

From: Patrice Chalin <chalin@cs.concordia.ca>

Reference(s):

LCL type specifications

From: Paolo Ciancarini <cianca@DI.UniPi.IT>