Prev Up Next
Go backward to 1 Version History
Go up to Top
Go forward to 3 Semantic Annotations

2 Introduction

In this note, we propose a set of (parsing and semantic) annotations and some syntax extensions for literals in CASL. The parsing annotations (for precedences and associativity) and syntax extensions (for lists, characters, strings, and numbers) influence the parsing of CASL specifications. The semantic annotations express some requirements on extensions, namely to be conservative or definitional. They do not change the semantics of a CASL specification, but they can be seen as additional proof obligations which have to be discharged in order to enhance the confidence in the correctness of the specification. In the case that they cannot be discharged, the specification should be seen as erroneous, even if strictly speaking, it still has a semantics.

The annotations are illustrated with fragments of example specifications, which are taken from our proposal for a library of standard specifications [RM99] and from our our proposal for datatypes REAL and COMPLEX in CASL [MR99]. [RM99][MR99] can be seen as complementary notes, since they contain a rich fundus of specifications using the annotations and syntax extensions.

The note is organized as follows: section 3 discusses the semantic annotations, section 4 the parsing annotations. Section 5 describes the syntax extensions.

CoFI Note: L-11 -- Version: 0.1 -- 11 March 1999.
Comments to

Prev Up Next