The Type System of VCL - Visual Contract Language

Sequence of formulas F is well-formed in E. E ⊢afs AFS : T. Arrows formula source AFS yields type T. Table 3.32 Type rules for assertion diagrams. (AD GBL).
907KB Sizes 0 Downloads 82 Views
The Type System of VCL

Nuno Amálio Laboratory for Advanced Software Systems University of Luxembourg 6, rue R. Coudenhove-Kalergi L-1359 Luxembourg

TR-LASSY-12-11

Contents Contents

2

1 Introduction 1.1 Background: The Visual Contract Language 1.1.1 VCL Diagrams . . . . . . . . . . . . Package Diagrams . . . . . . . . . . Structural Diagrams . . . . . . . . . Behaviour Diagrams . . . . . . . . . Assertion Diagrams . . . . . . . . . Contract Diagrams . . . . . . . . . . 1.1.2 Semantics . . . . . . . . . . . . . . . 1.2 Outline . . . . . . . . . . . . . . . . . . . .

(VCL) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

4 4 4 4 5 7 8 10 10 12

2 Syntax 2.1 Metamodels . . . . . . . . . . . . . . . . 2.1.1 Package Diagrams . . . . . . . . 2.1.2 Common . . . . . . . . . . . . . 2.1.3 Structural Diagrams . . . . . . . 2.1.4 Common Assertion and Contract 2.1.5 Assertion Diagrams . . . . . . . 2.2 Grammars . . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . Diagrams . . . . . . . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

13 13 13 15 16 17 18 19

3 Type System 3.1 Types and Environments . 3.2 Basic Rules . . . . . . . . 3.3 Common Rules . . . . . . 3.4 Package Diagrams . . . . 3.5 Structural Diagrams . . . 3.6 Assertion Diagrams . . . . 3.7 VCL Models . . . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

22 22 23 25 29 33 36 39

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

References A Auxiliary Definitions A.1 Environment Operators . . . . . . A.2 Predicates . . . . . . . . . . . . . . A.2.1 Predicate Ayclic . . . . . . A.2.2 Predicates IsSeqOfPEP and

40 . . . . . . . . . . . . . . . . . . . . . . . . IsSeqOfPEM

2

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

42 42 43 43 43

A.2.3 Predicate NoClashes . . . . . . . . . . . . . . . . . A.2.4 Predicate PkgsOnce . . . . . . . . . . . . . .