Concrete Syntax for CASL
Examples of Structured Specifications

Michel Bidoit
Christine Choppy
Bernd Krieg-Brückner
Peter D. Mosses
Frédéric Voisin

17 February 1998

This document is available by FTP in various formats. It was converted to HTML using Hyperlatex 2.2.

Abstract

This document illustrates the concrete syntax of basic and structured specifications [BCKB+98]. The examples are shown only in the display format, but the intended input syntax should in general be easy to deduce--in fact, it should be the same text as displayed when browsing the HTML-formatted version of this document (modulo display annotations). The input syntax of the examples is now also available by FTP.

Note that the mathematical symbols for set membership and union, displayed in the LaTeX formatting of SIG1 and SIG2, are also to be produced by display annotations, and the input symbol for the set membership predicate should not be `in', since that is the keyword used for subsort membership formulae.

Please feel free to suggest improvements, both to the details of the examples themselves, and to the LaTeX formatting, which will later be provided as a package for general use. Note that the HTML formatting was done automatically from the LaTeX source of this document, using Hyperlatex.

N.B. The examples are intended merely to illustrate the possibilities of the CASL concrete syntax, and to give an impression of the display format. Some of them could be expressed much more elegantly and concisely in other ways in CASL!

Contents

  • 1 Specifications from the Bremen Proposal
  • 1.1 PO
  • 1.2 MONOID
  • 1.3 NAT
  • 1.4 SIG1
  • 1.5 SIG2
  • 2 Specifications from the Paris Proposal
  • 2.1 FILE
  • 2.2 PATH
  • 2.3 LIST_WITH_ORDER
  • 2.4 COMPOUND_SYMBOLS_ARE_NICE
  • 2.5 LIST
  • References

  • CoFI Document: CASL/SyntaxExamples --Version 0.99-- 17 February 1998.
    Comments to cofi-language@brics.dk