The Type System of VCL - Visual Contract Language

5 downloads 151 Views 907KB Size Report
Sequence of formulas F is well-formed in E. E ⊢afs AFS : T. Arrows formula source AFS yields type T. Table 3.32 Type r
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 . . . . . . . . . . . . . . . . . A.2.5 Predicate AcyclicPkgs . . . . . . . . . . . . . . . . A.3 Auxiliary Functions . . . . . . . . . . . . . . . . . . . . . . A.3.1 Functions to extract information from PDs . . . . A.3.2 Function buildDE . . . . . . . . . . . . . . . . . . A.3.3 Function getGType . . . . . . . . . . . . . . . . . . A.3.4 Function superTy . . . . . . . . . . . . . . . . . . . A.3.5 Functions producing variable environments (VEs) . A.3.6 Function transferSDEntities . . . . . . . . . . . . . A.3.7 Function getDK . . . . . . . . . . . . . . . . . . . A.3.8 Functions to extract information from ADs . . . . A.3.9 Functions for AD lookup . . . . . . . . . . . . . . A.3.10 Functions for substitutions . . . . . . . . . . . . . A.3.11 Function getSIdFrScalarOrCollection . . . . . . . . B Alloy Metamodels of VCL Diagrams B.1 Package Diagrams . . . . . . . . . . . . . . B.2 Common . . . . . . . . . . . . . . . . . . . . B.3 Structural Diagrams . . . . . . . . . . . . . B.4 Common Assertion and Contract Diagrams B.5 Assertion Diagrams . . . . . . . . . . . . . .

3

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

43 44 44 44 44 44 44 45 45 45 46 46 47 48 48

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

49 49 52 61 68 73

Chapter 1

Introduction This document present a type system for the Visual Contract Language (VCL) [AK10, AKMG10]. This formalises a typed object-oriented system with subtyping. This type system has been implemented in the VCL tool, the Visual Contract Builder 1 [AGK11]. The following gives some background on VCL and an outline of the overall document.

1.1

Background: The Visual Contract Language (VCL)

VCL [AK10, AKMG10, AGK11] is a formal language designed for the abstract description of software systems. Its modelling paradigms are set theory, object-orientation and design-bycontract (pre- and post-conditions). VCL’s distinguishing features are its capacity to describe predicates visually and its approach to behavioural modelling based on design by contract. VCL’s semantics is based on set theory. Its semantics definition takes a translational approach. Currently, VCL has a Z semantics: VCL diagrams are mapped to ZOO [APS05, Amá07], a semantic domain of object orientation for the language Z [Spi92, ISO02].

1.1.1

VCL Diagrams

VCL’s diagram suite comprises package, structural, behaviour, assertion and contract diagrams. Package Diagrams Package diagrams (PDs) define VCL packages, coarse-grained modules representing concerns. Package are represented as clouds because they define a world of their own. Sample PDs from the secure simple bank case study [Amá11] are given in Fig. 1.1. PDs are as follows: • The package being defined or the current package is represented in bold. The current package can either be defined as a container (symbol ⌻) or ensemble (symbol ✶). Container packages merely contain sets and their local definitions. Ensemble packages have a global identity; they may include relations between sets and global invariants and operations. In Fig. 1.1, packages CommonTypes and RolesAndTasksBank are containers; all others are ensembles. 1 http://vcl.gforge.uni.lu/

4

(a) CommonTypes

(b) Bank

(c) Authentication

(d) TransactionsSwitch

(e) RolesAndTasksBank

(f) Authorisation

(g) SecForBank

(h) SecBank

Figure 1.1: Sample package diagrams of secure simple bank (from [Amá11]) • A current package may defined to use elements defined in other packages. Uses edges are represented with a hollow headed arrows. In Figs. 1.1b and 1.1c, packages Bank and Authentication use package CommonTypes. • The current package can incorporate other packages, which means that the current package includes the structures of incorporated packages plus some structures of its own. Package incorporation is expressed using enclosure. In Fig. 1.1h, package SecBank incorporates packages BankWithJI, SecForBank and TransactionsSwitch. • To resolve conflicts with package incorporations, it is possible to express in a PD conflict resolution dependencies using edges. There two kinds of such edges: overrides and merges. Override edges says that certain sets in the source package override those with the same name in the target package. Merge edges say that certain specified sets with the same name from the linked packages are to be merged. Figure 1.1f says that set User of package Authentication overrides User of AccessControl. • The current package may extend incorporated sets. This is specified using an extends list. In Fig. 1.1g, package SecForBank extends incorporated set User. Structural Diagrams Structural diagrams (SDs) define the structures that make the state space of a VCL package. Figure 1.2 gives sample SDs from secure simple bank. SDs are as follows: • SDs define two kinds of sets: value and class. Classes are distinguished from their value counterparts through a bold line. In Fig. 1.2a all sets are value. In SDs of Fig. 1.2, Customer, Account, User and Session are class sets; all others are value sets. • Sets that include symbol ⃝ are definitional. This means that they are defined by what they enclose. Sets that include symbol ⃝ followed by ↔ are derived. This means that they are 5

(a) CommonTypes

(b) Bank

(c) Authentication

Figure 1.2: Sample structural diagrams of secure simple bank (from [Amá11]) defined from primitive entities of the model. In Figs. 1.2b and 1.2c, sets CustType, AccType, LoginResult and UserStatus are enumerations defined by indicating their possible values. In Fig. 1.2a, TimeNat is a derived set defined from the set of natural numbers Nat2 . • Reference sets include symbol ↑; they are used to refer to sets defined in used packages as defined in the PD (those sets are visible). SDs of Figs. 1.2b and 1.2c have reference sets referring to Name and TimeNat defined in package CommonTypes (alias CT). • Edges with circled labels are relation edges. They define binary relations between sets. Directed edges are property-edges. They define state properties (attributes or fields) possessed by all objects of some set. In Figs. 1.2b and 1.2c, Holds and HasSession are relation-edges, and all outgoing edges with arrows emerging from sets Customer, Account, User and Session are property edges (e.g. name). • Assertions identify invariants, which are separately defined in ADs. Assertions connected to some set are local; those standing-alone are global. In VCB, double-clicking on an assertion takes the user to its AD (symbol ). In Figs. 1.2b and 1.2c, CorporateHaveNoSavings, HasCurrentBefSavings and HasSessionIffLoggedIn are global, SavingsArePositive and MaxPwMissesInv are local. • A SD can contain constants of sets and scalars. Constants have their labels preceded by symbol ©. Scalar constants are represented as objects (rectangles); set constants as set or 2 This

defines time as set of time points that are isomorphic to the natural numbers.

6

(a) Bank

(b) Authentication

(c) SecBank

Figure 1.3: Sample behaviour diagrams of secure simple bank (from [Amá11]) blobs. When placed inside sets, constants objects name values or objects of the enclosing set; this is a common idiom to define enumeration sets in VCL (e.g. sets CustType, AccType, LoginResult and UserStatus of the SDs of Fig. 1.2 are defined this way). A SD can also include constants with a type designator; such constants are local when attached to some set and global when they stands alone. In Fig. 1.2c, maxPwMisses defines a scalar constant of type Nat that is local to set User. Behaviour Diagrams A behaviour diagram (BD) declares the operations of a package. It may declare: (a) package operations to be separately specified in ADs and CDs or (b) operation compositions. Figure 1.3 presents sample BDs of secure simple bank. Specified operations of BDs are as follows: • There are two kinds of specified operations: update (or modifiers) and observe (or queries). Queries are represented as assertions, modifiers as contracts. In Fig. 1.3b, operations UserIsLoggedIn, GetUserGivenId and IsLoggedIn are queries; all others are modifiers. • Specified operations may be local or global: local when they are inside some set and global otherwise. The global operations of a package define the behaviour that the package offers to the outside world. Each specified operation needs to be defined in a AD or CD; doubleclicking takes the user to its definition (symbol ). BDs supports three kinds of operation compositions: integral, merge and join extension. Such compositions are defined in boxes; each box is named after the kind of composition. Operation compositions are as follows: • Integral extension promotes operations from incorporated packages to package operations so that they become available to the outside world as part of the package being defined. 7

The promoted operation is made available in the new package unaltered (hence name integral). Operations to be integrally extended are represented inside an integral extension box (there is at most one); they are represented visually as normal operations connected to the package where they come from. Special operation All refers to all operations of a package and it may include a list of operations to exclude. BD of Fig. 1.3c says that all operations of package TransactionsSwitch with the exception of IsSuspended and Init are to be integrally extended; likewise for all operations of package SecForBank except UserIsLoggedInAndHasPerm and Init. • Merge extension is a form of composition that merges or joins separate behaviours coming from different packages. Merge extensions are specified in a merge box; all separate operations that are included in the merge box with the same name are merged into a new package operation joining the separate behaviours. Semantically, merged operations are combined using an operator that is akin to logical conjunction. BD of Fig. 1.3c includes a merge box saying that Init of SecForBank is to be merged with Init of TransactionsSwitch. • Join extension is VCL’s aspect-oriented like mechanism. It inserts a certain extra behaviour into a group of operations. Join extensions involve placing the group of operations to extend inside a join box; the extra behaviours to insert are specified as join contracts, comprising a pre- and post-condition, that is connected to the box through a fork edge. There are two kinds of fork edges: concurrent (symbol ∧) and sequential (symbol ⌻). BD of Fig. 1.3c includes a join extension, saying that all operations of BankWithJI are to be concurrently joined with contract AuthACJoin. Assertion Diagrams Assertion Diagrams (ADs) describe predicates over a single state of the modelled system. They are used to describe invariants and observe operations. Sample ADs are given in Fig. 1.4. ADs are as follows: • An AD is made of two compartments: declarations (top) and predicate (bottom). This is illustrated in the ADs of Fig. 1.4. • An AD may have a global or a local scope. Global ADs include names of package and assertion; local ADs include names of package, set and assertion. In Fig. 1.4, ADs of Figs. 1.4a and 1.4b are local; all others are global. • The declarations compartment may includes variables, which are either scalar (represented as objects) or collections (represented as sets or blobs). Each variable has a name and a type. Variables can denote either inputs (name suffixed by ‘?’) or outputs (name suffixed by ‘!’). Figure 1.4d declares output set accs!. Figures. 1.4a, 1.4c and 1.4e declare several input and output objects. • The declarations compartment may include imported assertions, either standing alone or combined in logical formulas. Double-clicking on an imported assertion takes the user to its AD definition (symbol ). An assertion import comprises an optional up arrow symbol ↑, name of imported assertion with optional origin qualifier and an optional rename list. ↑ symbol indicates that the import is total (variables and predicate are imported); when not present the import is partial (only the predicate is imported). Rename list indicates variables of imported assertion that are to be renamed (e.g. [a!/a?] says that a! replaces a?). Fig. 1.4c has two assertion imports: one total and one partial. Total assertion import says that assertion GetBalance is to be called on Account object a!; as import is total, variable 8

(a)

(b)

(c)

(d)

(f)

(e)

(g)

(h)

Figure 1.4: Sample ADs of packages of secure simple bank (from [Amá11]) bal ! defined in Account.GetBalance (Fig. 1.4a) is also defined in AccGetBalance. Partial import of GetAccountGivenAccNo means that output a! is visible in AccGetBalance, but is not made available to the outside world; input aNo? is made available to the outside world as is also defined in AccGetBalance. • The predicate compartment includes visual formulas combining set expressions, predicates 9

and propositional logic operators. Figure 1.4a expresses an equality predicate using a predicate property edge to say that bal! is to hold value Account.balance. Figure 1.4b expresses an implication formula to say that if the property aType of Account has value savings then the property balance must be greater or equal than 0. Figure 1.4d outputs the set of accounts with negative balances; this builds a set using a set definition construction (symbol ⃝) by constraining set Account using predicate property edges (arrows); the constructed set is then assigned to output ‘accs!’. Figure 1.4e expresses a set membership predicate using a predicate property edge to say that output a! belongs to accounts with property accNo equal to aNo? (there is at least one). Figure 1.4f comprises a set formula that defines a set by constraining the relation Holds, using property edge modifiers with operators domain (▹) and range restriction (◃), to give the set of tuples made of corporate customers and savings accounts; outer shading (reinforced with symbol ∅) then says that this set must be empty. Contract Diagrams Contract Diagrams (CDs) describe system dynamics. They comprise a pair of predicates corresponding to pre- and post- conditions. Pre-condition describes what holds before operation is executed. Post-condition describes effect of operation, saying what holds after execution. CDs are used to describe operations that change the state of modelled system. Sample CDs are given in Fig. 1.5. CDs are as follows: • Like ADs, CDs are made of two main compartments for declarations and predicate. In CDs, the predicate compartment is subdivided in two for pre-condition (left) and post-condition (right). This is illustrated in CDs of Fig. 1.5. • CDs are similar to ADs in terms of what can be included in the declarations compartment. The only difference is that CDs can include both imported assertions and contracts. This is illustrated in CDs of Fig. 1.5. In Fig. 1.5e, import of contract HasSessionAddNew includes a renaming. In Fig. 1.5f, the two imported contracts are combined using a disjunction to say that a login operation is either successful (LoginOk, Fig. 1.5e) or not (LoginNotOk, Fig. 1.5d). • In CDs, pre- and post- condition compartments are made of the same sort of visual formulas used in the predicate compartment of ADs. In the post-condition compartment, the variables that change state are bold-lined. In Figs. 1.5a and 1.5c, pre- and post-conditions compartments are made of arrows formulas stating equality predicates; the post-state variables are bold-lined in the post-condition compartment.

1.1.2

Semantics

VCL’s modelling paradigms are set theory, object-orientation and design-by-contract (pre- and post-conditions). VCL’s semantics is based on set theory. Its semantics definition takes a translational approach: diagrams are mapped to ZOO [APS05, Amá07], an object-oriented semantic domain for Z [Spi92, ISO02]. Briefly, VCL’s semantics is as follows: • Objects are atoms; members of some set. • Property edges are properties shared by all objects of the set. Relational edges are binary relations between sets. 10

(a)

(b)

(c)

(d)

(e)

(f)

Figure 1.5: Sample CDs of package Authentication of secure simple bank (from [Amá11]) • An ensemble package is defined as the conjunction of all class sets, relational edges and global invariants. • An assertion describes a condition of a particular state structure or ensemble. It is therefore represented as a predicate over a single state structure or ensemble. • Operations are relations between a before-state (pre-condition) and an after-state (postcondition) of particular state structure or ensemble.

11

1.2

Outline

The remainder of this document is as follows: • Chapter 2 presents the syntactic descriptions using metamodels and grammars. The type system is defined in the grammar. • Chapter 3 presents the actual VCL type system made up of type rules. • Appendix A presents the auxiliary definitions that are used to describe VCL’s type system presented here. • Appendix B presents the VCL metamodels described using the Alloy formal modelling language.

12

Chapter 2

Syntax This chapter presents the syntax of VCL package, structural behavioural and assertion diagrams. It starts by presenting the syntax of these notation using visual metamodels. Then, it presents their equivalent grammars. The next chapter defines the type system based on the grammar representation.

2.1

Metamodels

The metamodels of the VCL notations presented here have been defined in the Alloy specification language [Jac06]. They are given in appendix B. Here, we present these metamodels using UML class diagrams, which partially describe what is described in Alloy: the Alloy describes constraints that are not describable using class diagrams. The Alloy metamodels for the different VCL diagram types comprise the following Alloy modules: package diagrams (section B.1), common (section B.2), structural diagrams (section B.3), common assertion and contract diagrams (section B.4), and assertion diagrams (section B.5). The following class diagrams describe each of these modules.

2.1.1

Package Diagrams Name

ExtendsList

PackageDiagram

extElems: [*, Set]Name extends

0..1

defines kind

CurrPackage * uses

inside *

VCLPackage name: Name alias : [0..1] Name

PkgKind -Container -Ensemble

target * edges

PkgEdgeKind

PkgEdge names: [*, Set]Name

kind

-Overrides -Merges

Figure 2.1: The metamodel of VCL Package diagrams A VCL package diagram (PD) defines a package (the current package) and its relations with other VCL packages. In VCL, packages are represented using a cloud symbol. The metamodel of VCL PDs (Fig. 2.1), corresponding to the Alloy module of section B.1, is as follows: 13

*

SetElement

SetExtension

elems VCLObject id : Name

Pair idElem1 : Name idElem2 : Name

ConstrainedSet desig : TypeDesignator

Num

SetInsideExpression

0..*

Expression

def

SetExpressionID bd: TypeDesignator

SetExpressionDef

SetExpressionEmpty exp2

ObjExpression

ObjExpId id : Name

exp

ObjExpNum

SetExpressionCard

exp1

exp ObjExpBin

TypeDesignatorNat

SetDefOp -Domain -Range -Union -Intersection -CrossProduct -SetMinus -None

sExp

mop EdgeOperatorMod -DRES -RRES -DSUB -RSUB

TypeDesignatorInt

sdop SetDef

SetExpression

PropEdgeMod

bop

num

InsideExpSDs

{ordered} setDefs

pes {ordered} * target PropEdge

uop

EdgeOperatorBin -EQ -NEQ -IN -LT -LEQ -GT -GEQ -SubsetEQ

Assertion id : Name

insideExp

PropEdgePred designator [0..1]: Name

EdgeOperatorUnary -CARD -THE -NONE

InsideDef

ObjExpUMinus

TypeDesignatorId

bop

ObjExpBinOp -Plus -Minus -Times -Div

ObjExpPar

name TypeDesignator

Name

Figure 2.2: The common metamodel • A PD (class PackageDiagram) comprises the package being defined (defines associationend), an instance of CurrPackage, which is just a special Package (inheritance relation). A CurrPackage is depicted with a bold line; it can either be Ensemble or Container (kind association-end): containers have their label preceded by symbol ⌻, and ensembles by symbol ✶ . A CurrPackage can: (a) enclose other packages to represent the packages it incorporates (inside association-end), (b) be connected with uses arrows to other packages (uses association -end) and (c) contain an extends list (ExtendsList class) to indicate sets being extended. A container cannot incorporate ensembles. All packages being incorporated and used must have been defined. • The packages being incorported may be connected with edges (PkgEdge). There are two kinds of edges (kind association-end): Overrides and Merges. An edge has a label indicating the blobs being overridden or merged (names attribute). Only blobs with no local properties (property edges) may be overridden. Edges define package relations that are anti-reflexive and anti-symmetric.

14

2.1.2

Common

The metamodel of the part that is common to both SDs and ADs (Fig. 2.2), corresponding to the Alloy module of section B.2, is as follows: • Several constructions have a name attribute; the metaclass (Name, bottom-left) denotes all names of a VCL model. Several constructions use the type designator (TypeDesignator, bottom-left). A type designator can either denote the set of natural numbers (TypeDesignatorNat), the set of integers (TypeDesignatorInt), or some set defined by a blob or relation edge and denoted by their identifier (TypeDesignatorId). • A property edge (PropEdge) can either be of type predicate (PropEdgePred) or modifier (PropEdgeMod). PropEdgePreds comprise a unary and binary operator (uop and bop association-ends), an instance of EdgeOperatorUn and EdgeOperatorBin, respectivelly, a target Expression (target association-end) and an optional designator (attribute designator) to refer to some property of a blob. A PropEdgeMod comprises a modifier operator (mop association-end) an instance of EdgeOperatorMod. • A modifier edge operator (EdgeOperatorMod) is an enumeration comprising the operators: domain restriction (DRES, ▹), range restriction (RRES, ◃), domain subtraction (DSUB, ⌫) and range subtraction (RSUB, ⌦). A predicate edge operator is enumeration comprising the operators: equality (EQ, =), non-equality (NEQ, ̸=), set membership (IN, ∈), less then (LT, ), greater or equal then (GEQ, ≥), and subsetting (SubsetEQ, ⊆). • There are two kinds of expressions: object (ObjExpression), represented as objects (rectangles), and set (SetExpression), represented as blobs (rectangles with rounded corners). An object expression can either be: an identifier (ObExpId); a number (ObjExpNum); a unary minus expression (ObjExpUMinus), comprising another expression (exp association-end); a binary object expression, comprising two expressions (association-ends exp1 and exp2) and an infix operator (bop association-end); or a parenthesised expression, comprising another expression (exp association-end). A binary object-expression operator (ObjExpBinOp) is an enumeration comprising the operators: Plus (+), Minus (−), Times (∗), and Div (div). • A SetExpression can either refer to some existing set (SetExpressionId), denote the empty set (a blob that is shaded), be a cardinality operator applied to another set expression SetExpressionCard, or be a set definition (SetExpressionDef). A SetExpressionId comprises a designator of the set being referred (attribute desig). A SetExpressionCard is the cardinality operator applied to another set expression (sExp association-end). A SetExpressionDef comprises a set definition (association-end def), an instance of SetDef. • Set definitions (SetDef) are defined by the things they have inside. They comprise an inside expression (insideExp association-end), representing the expression placed inside the blob, and by a set definition operator (sdop association-end). A set definition operator (SetDefOp) is an enumeration defining the operators Domain (symbol ←), Range (symbol →), Union (symbol ∪), Intersection (symbol ∩), CrossProduct (symbol ×), SetMinus (symbol \) or None (no operator). • A set inside expression (SetInsideExpression is either an inside definition (InsideDef) or a sequence of set definitions (InsideExpSDs). A InsideExpSDs comprises a sequence of set definitions (setDefs association-end). An InsideDef is an abstract class, which comprises either a SetExtension or a ConstrainedSet. A ConstrainedSet represents 15

elements *

SDiag

SDElem name : Name

definition

(Common)

0..1 RelEdge multS : Mult multT : Mult

source

target IntSet

Set

PrimarySetDef isDef : boolean *

DerivedSet

ReferenceSet pkgId : Name

SetWithProps SetDef (Common)

*

lProps

PropEdgeDef mult : Mult Mult

MOne

MOpt

VCLObject (Common)

hasInsideO

kind SetKind -Value -Class

ConstantKind -Reference -Definition

PkgBlob lb

MOneOrMany

ub

MRange MSeq

lInvariants

*

peTarget

definition

*

Constant kind : ConstantKind type [0..1] : Name origin [0..1] : Name * lConstants

hasInsideSet * PrimarySet

NatSet

* invariants Assertion

Int

UBound

UBoundInt val : Int UBoundStar

MMany

Figure 2.3: The metamodel of VCL Structural diagrams a set constrained with an ordered collection of property edges (association-end pes). A set extension (SetExtension) represents a set defined extensionally by a set of elements (association-end elems), which are instances of SetElem. • A SetElem is represented visually as a rectangles; it can either be a VCLObject (a member of set) or a Pair (a member of a relation). A VCLObject comprises a name (the name of the object); a Pair comprises a pair of names.

2.1.3

Structural Diagrams

The metamodel of VCL structural diagrams (SDs) (Fig. 2.3), corresponding to the Alloy module of section B.3, is as follows: • A SD (SDDiag) is made of structural elements (SDElem) and invariants (Assertion). A SDElem can be a relation edge (RelEdge), constant (Constant) or set (Set). • In a SD, an Assertion represents an invariant. If they belong to the overall SD (associationend invariants) they represent global invariants; if they are connected to a set (associationend lInvariants), the invariant is local to the set. • A relation edge (RelEdge), or association, represents an edge between two sets: the source and the target. It holds two attributes to record the multiplicities attached to source and target (multS and multT). • Like invariants, constants (Constant) are global if they are not connected to any set and local otherwise (association-end lConstants). 16

DeclObj optional : Boolean

DeclCompartment decls

TypedDecl dName : Name dTy : TypeDesignator

*

Decl

DeclSet sequence : Boolean RenamingExp subExp : Name varToSub : Name

DeclFormulaNot FormulaSource

frmlSrc

FormulaSourceElem elem : SetElement

dFrml1

df

*

renameExp

DeclFormula FormulaSourceSet FormulaSourceUnary FormulaSourceSetId setId : Name

dFrml2 DeclFormulaBin

FormulaSourceSetDef

setDef SetDef (Common)

operator FormulaSourceUOp -Cardinality -Domain -Range -The

dfop FormulaBinOp -implies -and -or -equiv -seqcomp

DeclFormulaAtom refId : Name import : Boolean origin [0..1] : Name refKind DeclRefKind -Simple -Call -NewCall -Package

Figure 2.4: The common metamodel of VCL assertion and contract diagrams • A set can be primary (PrimarySet), derived (DerivedSet) or one of the sets corresponding to primitive types: integers (IntSet) or natural numbers (NatSet). • A derived set has a name (attribute id) and is associated with a set definition (SetDef, defined in common metamodel). • A primary set has a kind (SetKind), indicating whether the set is Class or Value. A primary set comprises a set of local constants (association-end lConstants), a set of local invariants (association-end lInvariants), and a set of property edge definitions (associationend lProps). A primary set may have other primary sets and objects inside (associationends hasInsideSet and hasInsideO). • A property edge definition (PropEdgeDef) has a set has the edge’s target (association-end peTarget) indicating the type of the property, and a multiplicity constraint (attribute mult). • In SDs, VCL objects (VCLObject) may be placed inside blobs to represent objects of some set. This construction is used to define enumerations in VCL SDs. • Multiplicities (Mult) are attached to relation edges and property edge definitions. A multiplicity can either be single (MOne), optional (MOpt), sequence (MSeq), multiple with 0 or more (Many), multiple with at least one (MOneToMany), or be defined as a range (MRange) comprising a lower and an upper bound (association-ends ub and lb).

2.1.4

Common Assertion and Contract Diagrams

The metamodel of common assertion and contract diagrams (Fig. 2.4), corresponding to the Alloy module of section B.4, is as follows: 17

FormulaNot

PropEdgePred ( Common)

pes frml 0..1 Formula predicate * frml1 frml2

ADiag aName : Name

*

ArrowsFormula

SetFormula declarations DeclCompartment (AD_CD_Common) SetExpression

FormulaBin setop : FormulaBinOp

hasInside

(Common)

source FormulaSource (AD_CD_Common)

SetFormulaShaded setId : TypeDesignator

FormulaSubset setId : TypeDesignator

SetFormulaDef shaded : Boolean setId [0..1] : TypeDesignator

setdef

SetDef (Common)

Figure 2.5: The metamodel of VCL assertion diagrams • A declarations compartment (DeclCompartment) comprises several declarations (Decl), which can either be a typed declaration (TypedDecl) or a declaration formula (DeclFormula). A typed declaration has a name (dName) and a type (dTy), and it can either be a declaration of an object (DeclObj) or the declaration of a set (DeclSet). The sequence attribute of DeclSet indicates whether the set is a normal set (value false) or a sequence (value true). The optional attribute of DeclObj indicates whether the object is optional or not. • A declarations formula (DeclFormula) can either be a declarations formula atom (DeclFormulaAtom), which comprises a declaration reference, a negated declaration formula (DeclFormulaNot), which comprises the declarations formula being negated, or a binary declaration formula (DeclFormulaBin), which comprises an operator (DeclFormulaBinOp) and two declarations formulas. • FormulaSource represents the source of a predicate formula in AD or CDs. It can either be a formula source element (FormulaSourceElem), which comprises a set Element (defined in Common, Fig. 2.2), or a blob element (FormulaSourceBlob).

2.1.5

Assertion Diagrams

The metamodel of VCL assertion diagrams (Fig. 2.5), corresponding to the Alloy module of section B.5, is as follows: • An assertion diagram (ADiag) comprises a name (aName), a set of declarations corresponding to the declarations compartment (declarations association-end), and a set of formulas corresponding to the predicate compartment (predicate association-end). • A formula (Formula) can either be a negation formula (FormulaNot), a binary formula (FormulaBin), an object formula (ObjFormula) or a set formula (SetFormula). • A negation formula (FormulaNot) comprises another formula corresponding to the formula being negated (frml association-end). A binary formula (FormulaBin) comprises two formulas corresponding to the formulas being combined (frml1 and frml2 association-ends),

18

VCL Pkg

::= ::=

Pkg PD SD AD Figure 2.6: Syntax of VCL Models

and an operator (op association-end). A binary formula operator (FormulaBinOp) can either be an implication (implies), a conjunction (and), a disjunction (or), or an equivalence (equiv). • An arrows formula (ArrowsFormula) comprises a set of predicate property edges (pes association-end). • A set formula (SetFormula) can either be a subset formula (FormulaSubset), a shaded blob formula (SetFormulaShaded) or a set definition formula (SetFormulaDef). A subset formula (FormulaSubset) corresponds to the situation where one set is placed inside another to denote the subset relationship; it has a set identifier (attribute setId) and a set expression to denote the inside set (hasInside association-end). A shaded set formula corresponds to the situation where some set is shaded; it comprises a set identifier (attribute setId). A definition set formula (SetFormulaDef) comprises a SetDef (association-end setdef) from the common metamodel (Fig. 2.2); it can be shaded or have an identifier (either one or the other).

2.2

Grammars

The metamodels presented above are the basis for the implementation of diagram editors in VCL’s tool. To specify type systems, grammars are a more convenient representation. The following presents the grammars of VCL package, structural and assertion diagrams; they are equivalent to the visual metamodels presented above. The grammars use the following operators: • x for zero or more repetitions of x; • x 1 for one or more repetitions of x; • x | y for a choice of x or y; • [x ] for an optional x. In addition, • xc for some character symbol c means zero or more occurrences of x separated with c; • xc 1 for some character symbol c means one or more occurrences of x separated with c; Symbols are set in bold type when they are to be interpreted as terminals to avoid confusion with grammar symbols. We introduce two syntactic sets, representing terminals: the set of identifiers Id , and the set of numeric constants (Num). Figure 2.6 defines the grammar of a VCL model. A VCL model (VCL) comprises a sequence of package models (Pkg). A package model (Pkg) comprises one package diagram (PD), one structural diagram (SD) and several assertion diagrams (ADs). The grammars defining the syntax of the different VCL diagrams are as follows:

19

• Figure 2.7 presents the grammar of package diagrams (PDs). • Figure 2.8 describes the syntactic constructions that are common to both SDs and ADs. • Figure 2.9 presents the grammar of structural diagrams (SDs). • Figure 2.10 presents the grammar of assertion diagrams (ADs). PK PD

::= ::=

PRef PExts PDep PEdgKind

::= ::= ::= ::=

container | ensemble PK package Id [uses PRef ,] [incorporates PRef ,] { PDep [PExts] } Id [as Id] 1 extends (Id , ) 1 Id PEdgKind Id on ( Id , ) merges | overrides Figure 2.7: Syntax of Package Diagrams

TD O P SE A PE PEP UEOp BEOp PEM MOp TExp OExp OEOp SExp SDef SOp IExp IDef

::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::=

Int | Nat | [Id ::] Id object Id pair (Id, Id) O|P assertion AId (PEP | PEM) TExp [UEOp] [Id.] → [BEOp] # | ◉| ⊥ = | ̸= | ∈ | < | ≤ | > | ≥ | ⊆ [ MOp ] ⇒ ▹ |◃|⌫| ⌦ object [OExp] | SExp Id | Num | −OExp | OExp OEOP OExp | (OExp) + | − | ∗ | div set TD | SDef | set shaded | # SExp set ⃝ SOp hasIn {IExp} ←|→|∩|∪|×|\|⊥ IDef | SDef ; 1 1 set TD { PE } | SE Figure 2.8: Common syntactic constructions to ADs and SDs

20

SD SDE GC C CR M RE SK Set RSet PSet PSetDef ExtSet PkgE PED

::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::=

SDE A GC | RE | Set | PkgE C | CR const Id : TD | const Id : TD ↔ A ↑ const [Id.] Id ↔ Assertion opt | one | some | many | seq | Num .. (Num | *) relEdge Id (M TD, M TD) value | class PSet | RSet | Id ↔ set SetDef ↑ set [Id ::] Id PSetDef | ExtSet set Id SK [⃝] { C PED A } [hasIn {(O | PSet)}] ↓ set Id { C PED A } [hasIn {(O | PSet)}] pkg Id { PED } Id → M TD Figure 2.9: Syntax of structural diagrams

AD D DV R DFA DF FOp F AFS AFSS FSOp AF SF

::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::= ::=

AD Id [:Id] decls {D} pred {F } DV Id : TD | DF object [?] | set : [[]] Id / Id [↑] A [R] | [↑] assertion Id (→ | . | ::) Id [R] DFA | ¬ ( DF ) | ( DF FOp DF ) ⇒|⇔|∧|∨|⌻ AF | SF | ¬ [F] | [F] FOp [F] SE | AFSS | FSOp AFS set Id | SDef #|←|→|◉ AFS { PEP } [shaded] [Id] SDef | set shaded TD | set TD hasIn {SExp} Figure 2.10: Syntax of Assertion Diagrams

21

Chapter 3

Type System This chapter presents VCL’s type system. It starts by defining VCL’s types and typing environments (section 3.1). Then, it presents the basic (section 3.2) and common rules (section 3.3) of the type system. Finally, it presents the rules that are specific to package (section 3.4), structural (section 3.5) and assertion diagrams (section 3.6).

3.1

Types and Environments

A variable environment (VE ) denotes a set of bindings, mapping identifiers to their types: VE == Id → 7 T VCL’s types (set T ) are as follows: T

::=

Int | Nat | Null | Set T | Seq T | Opt T | Top | Obj | Set Id | Pair (T, T) | Assertion [VEv , VEh ] | Contract [ VEv , VEh ] | Pkg Id

Here, (a) Int represents the integers, (b) Nat the natural numbers; (c) Null represents erroneous results (implementation only); (d) Set T represents a powerset of some set; (e) Seq T represents a sequence of some type; (f) Opt T represents an optional (either it exists or is empty); (g) Top is a maximal type (type of all well-formed terms); (h) Obj is the maximal type of all well-formed objects; (i) Set represents primary sets; (j) Pair represents a cartesian product of two types; (k) Assertion represents assertions (variable environments indicate assertion’s variables, which are either visible, VEv , or hidden, VEh ); (l) Contract represents assertions; and (i) Pkg represents packages. VCL’s type rules use and manipulate environments (set E below), which are made of four components: (a) variable, (b) package, (c) set and (d) subtyping. Variable environments give the type bindings of some scope. Package environments (PE ) map identifiers to a pair made up of the package’s kind (PK, Fig. 2.7) and the package’s environment. Set environments (SE ) map identifiers to a quadruple made up of the set’s kind (value or class), definitional status (DK ), identifier of owning package and local variable environment. Subtyping environments (set SubE ) are the subtyping relations between types:

22

Table 3.1 Judgements associated with the basic rules of VCL’s type system E ⊢T T is well-formed type in E E ⊢ T1