LSL: Larch Shared Language
Language Design

Version 0.1

[ Outline | ABEL | ACT-ONE+TWO | ASF+SDF | Asspegique+ | Clear |
   EML | LPG | LSL | OBSCURE | RSL | SMoLCS | SPECTRAL | Spectrum | Z ]

This document is part of the CoFI Catalogue of Algebraic Specification Frameworks. It was provided by Stephen J. Garland; any comments and corrections should be addressed to garland@larch.lcs.mit.edu.

It will be made available formatted for printing as compressed Postscript (~100Kb) and DVI (~50Kb).

The WWW version provides only a rough approximation (mostly generated automatically by Hyperlatex) to the symbols used in the formatted versions. Please inform pdmosses@brics.dk about any places where an alternative approximation is desirable!

N.B. All sections of the catalogue are TENTATIVE first versions, unless explicitly marked otherwise. Sections dealing with Methodology, Tools, and Documentation will be added later.

Here is a first attempt at answering those questions I understand. I would be happy to provide more information, but felt that it was better to get something to you quickly than to take the extra time required to do a thorough job.
Steve Garland
  • 1 Specification in the Small
  • 1.1 Basic Constructs
  • 1.1.1 signatures
  • 1.1.2 axioms
  • 1.1.3 models
  • 1.1.4 constraints
  • 1.1.5 status
  • 1.1.6 other
  • 1.2 Types
  • 1.2.1 predefined types
  • 1.2.2 algebra of types
  • 1.2.3 parametrized type constructors
  • 1.2.4 polymorphic types
  • 1.2.5 dependent types
  • 1.2.6 other
  • 1.3 Partiality
  • 1.3.1 subtypes defined by predicates
  • 1.3.2 subtypes declared in the signature
  • 1.3.3 equations
  • 1.3.4 (un)definedness
  • 1.3.5 logic
  • 1.3.6 strictness
  • 1.3.7 other
  • 1.4 Notations
  • 1.4.1 offside rule
  • 1.4.2 graphical symbols
  • 1.4.3 overloading
  • 1.4.4 mixfix notation
  • 1.4.5 operator precedence
  • 1.4.6 associativity
  • 1.4.7 values of predefined types
  • 1.4.8 other
  • 1.5 Abbreviations
  • 1.5.1 type inference
  • 1.5.2 conditionals
  • 1.5.3 variable abstraction
  • 1.5.4 variable inference
  • 1.5.5 lambda-abstraction
  • 1.5.6 other
  • 1.6 Other
  • 2 Specification in the Large
  • 2.1 Structuring Concepts
  • 2.1.1 structure of specifications v. programs
  • 2.1.2 structuring logic/institution-independence
  • 2.1.3 other
  • 2.2 Basic Constructs
  • 2.2.1 naming
  • 2.2.2 union
  • 2.2.3 renaming
  • 2.2.4 hiding
  • 2.2.5 sub-specifications
  • 2.2.6 nesting of signatures
  • 2.2.7 morphisms as entities
  • 2.2.8 behavioural encapsulation
  • 2.2.9 other basic structuring constructs
  • 2.2.10 other
  • 2.3 Parametrization
  • 2.3.1 specifications parametrized by programs
  • 2.3.2 specifications of parametrized programs
  • 2.3.3 higher-order parametrization
  • 2.3.4 dependent specifications
  • 2.3.5 uniqueness of instantiations
  • 2.3.6 other
  • 2.4 Multiple Logics
  • 2.4.1 heterogeneous specifications
  • 2.4.2 heterogeneous developments
  • 2.4.3 logic morphisms, representation morphisms
  • 2.4.4 navigation in logic graph
  • 2.4.5 composition, instantiation, sub-framework
  • 2.4.6 other
  • 2.5 Other
    • LSL, May 14, 1996