The LM3 specication language

Cours the LM3 specication language, tutoriel & guide de travaux pratiques en pdf.

The LM3 speci cation language

An LM3 interface speci cation consists of a Modula-3 interface de nition together with some annotations within pragma brackets. A speci cation contains type speci cations, variable and constant declarations, procedure speci cations and an interface invariant. In the following sections, we con-sider these in turn.
We introduce the following grammatical conventions:
terminal symbols | term non-terminals | nonTerm
foo, means zero or more foo’s separated by a , foo;+ means one or more foo’s separated by a ; [foo] means zero or one foo
extensions to the Modula-3 grammar are indicated as foo

Interfaces
The top-level unit in an LM3 speci cation, like that of a Modula-3 program, is the interface. A Modula-3 interface is annotated with a list of traits that de ne the meaning of the symbols used within predicates to specify the functionality of the interface components. Any renaming necessary to remove ambiguity must be done here, using LSL mechanisms.
There may be an initial condition and an invariant associated with the interface. In an interface that declares variables, the initial condition constrains the initial value of the variables. The invariant would normally be used to state relationships that must always be maintained between these variables. It may also be used to specify relationships between procedures within the interface.
Since grammar fragments are not the most enlightening way of under-standing a language, we develop a simple example1 as we introduce each new construct. A skeleton of the interface is given as:
INTERFACE Stack;
<* USING Stack(Real for E, RealStack for C) *>
(* declarations of exported type and procedures – see below *)
END Stack.
The USING clause associates all symbols used in the speci cation with those found in the trait named Stack, with the appropriate renaming. All interfaces implicitly use a trait LM3Trait which gives the de nitions of the primitive operations of Modula-3. See Chapter 4. The trait Stack, from the Larch Shared Language Handbook[8], is given in Appendix A.
1 Our excuse for using the ubiquitous stack example is that we are following the Modula-3 Report, which uses Stack as its example of an interface.

Declarations

Declarations in Modula-3 interfaces include constants, types, variables, ex-ceptions and procedures. In this section, we describe the LM3 speci cations for each since the form of the speci cation depends on the kind of declara-tion.

Constants
An interface may export any number of constants. The grammar for con-stant declarations is:
constDecl ::= ident [: type] = constExpr
A constant declaration for LM3 is just a Modula-3 constant declaration, with the restriction that the constExpr must be a term of the LM3 expression language.
For example, if we wished to give an upper bound to the stack, we could write:
CONST MaxSize = 100;

Variables
LM3 adds no extra information to the declaration of exported variables.
Any restrictions may be placed in either the type or the interface invariant.

Private variables
It is often the case that the speci cation uses information that does not have to be accessible to the implementation.
To facilitate this, LM3 allows the declaration of private variables, which are notionally part of the state but which may be referenced only within speci cations. These variables exist only within the speci cation domain and are associated with LSL sorts, not with types. For convenience, the obvious sorts are available to represent the common programming language types.
The rst clause associates the type with a sort, which must be de ned in one of the traits in the USING list. In particular, for any variable v of type T which is based on sort S, the value of v must be equal to a term of sort S for which T’s invariant is true.
The initial clause, indicated by INITIALLY, introduces a predicate that must hold for initial values of a type. For a simple type this predicate constrains the initial values supplied in variable declarations. For an object type it is a constraint on the result of calls to NEW. Satisfaction of this constraint is an obligation of clients that use the type.
The invar clause, indicated by INVARIANT, introduces a predicate that is notionally conjoined to the pre- and post-condition of all procedures that may reference an element of the type. Such a procedure may assume the invariant on invocation and must guarantee it on exit. Object types, where invariants are inherited, are discussed separately in Section 2.3.3.
The ident represents a variable bound by universal quanti cation over the type.
Each type declared in the interface is associated with a sort. There are two categories of types:
1. types with modi able values (REF types). That is T <: REFANY or ROOT. If such a T is BASED ON a sort S, the sort actually used to represent the type is SRef.
2. types with unmodi able values (VAL types). In this case, there is no indirection and the sort is the one given in the BASED ON. Parameters of such a type are unmodi able (and it is a checked error to try to modify a parameter of a VAL type). Modi cations of such parameters are permitted only if they are declared as VAR. In this case the sort of the parameter is SVar which can be regarded as implicitly introducing an extra level of reference.

1 Introduction 
1.1 Background
1.2 The relationship between Modula-3 and LM3
2 The LM3 specication language 
2.1 Interfaces
2.2 Declarations
2.2.1 Constants
2.2.2 Variables
2.2.3 Private variables
2.2.4 Types
2.2.5 Procedures
2.3 Other Modula-3 features
2.3.1 Procedure parameters
2.3.2 Intermediate states
2.3.3 Object types and methods
3 The Syntax of LM3 
3.1 The LM3 reference grammar
4 The semantics and checking of LM3 
4.1 The translation functions
4.2 The LM3Trait
4.2.1 The interfaces
4.2.2 The trait
5 Examples 
5.1 The Threads interface
5.1.1 Mutex, Acquire, Release
5.1.2 Semaphore, P, V
5.1.3 Blocking and unblocking on condition variables
5.1.4 Alerts
5.2 The IO Streams interface
5.2.1 An IOStreams package
5.2.2 The Rd interface
5.2.3 The RdClass interface
Bibliography

Cours gratuitTélécharger le cours complet

Télécharger aussi :

Laisser un commentaire

Votre adresse e-mail ne sera pas publiée. Les champs obligatoires sont indiqués avec *