LSL Traits for SPECS

Purpose

This page is a guide to an archive of traits for use in Al Baker's SPECS family of specification languages. The traits are written in the Larch Shared Language (LSL).

The traits are freely available, both through this page, an alphabetical index, and by anonymous ftp from ftp.cs.iastate.edu in file pub/larch/SPECS/SPECS-traits.tar.gz. (The README file contains similar information to this page.)

This collection of traits constitutes a small LSL handbook. (Other handbooks are also available.) Corrections are welcome.

Overview of the traits

To use these traits with the LSL checker, you will have to use the SPECS init file (described below) and also the mathematical traits handbook for any specifications involving the real numbers.

Init File

To use these traits you need to use the LSL init file in SPECS_lslinit.lsi. This file simply defines boolean as a synonym for the LSL sort Bool. When using the LSL checker, you should invoke it with a -i option as follows.

	lsl -i SPECS_lslinit.lsi file.lsl ...

Unstructured Types

Models of the SPECS unstructured types are found in the following traits.

• SPECS_boolean
• SPECS_char
• SPECS_real
• SPECS_integer
• SPECS_empty_tuple

Structured Types

Models of the structured types set and sequence, are found in the following traits.

• SPECS_set, which is based on the trait SPECS_set_basics
• SPECS_sequence which is based on the trait SPECS_sequence_basics

The sugars for constructors for these types are found in the traits SPECS_set_sugars and SPECS_sequence_sugars.

Tuples, and enumerations are type constructors, and as such don't have a general translation into LSL. Instead we give examples of the translations into LSL for specific examples:

• The trait SPECS_FullName is an example of the tuple notation.
• The trait SPECS_Color is an example of the enumeration notation.

Sugars

The SPECS_neq_sugar defines the operator != as a synonym for ~=.

Acknowledgements

Thanks to Al Baker and the participants in the seminar "Specification and Verification using Larch/C++" in Fall 1995 at Iowa State for comments and help with these traits. Thanks to John Penix for his lsl2html tool.

This work was supported in part by NSF grant CCR-9593168.

Copyright

Permission is granted for you to use the traits in the ftp directory for educational and scholarly purposes, and for commercial use in specifying software, but the copies may not be sold or otherwise used for direct commercial advantage; this premission is granted provided that this copyright and permission notice is preserved on all copies. All other rights reserved.