# VDM types as Smalltalk objects

Although types are not the first class objects in VDM-family, ViennaTalk provides classes to prepresent VDM types. The following table shows mapping from VDM types to corresponding Smalltalk expressions.

type | Smalltalk expression | class | class of value |
---|---|---|---|

nat | ViennaType nat | ViennaNatType | Integer |

nat1 | ViennaType nat1 | ViennaNat1Type | Integer |

int | ViennaType int | ViennaIntType | Integer |

real | ViennaType real | ViennaRealType | Float |

bool | ViennaType bool | ViennaBoolType | Boolean |

ViennaType quote: #quote | ViennaQuoteType | Symbol | |

[t] |
t optional |
ViennaOptionType | the class of t’s value or UndefinedObject |

t1 * t2 |
t1 * t2 |
ViennaProductType | Array |

t1 | t2 |
t1 | t2 |
ViennaUnionType | either the class of t1 or t2’s value |

set of t |
t set |
ViennaSetType | Set |

seq of t |
t seq |
ViennaSeqType | OrderedCollection |

seq1 of t |
t seq1 |
ViennaSeq1Type | OrderedCollection |

map t1 to t2 |
t1 mapTo: t2 |
ViennaMapType | Dictionary |

inmap t1 to t2 |
t1 inmapTo: t2 |
ViennaInmapType | Dictionary |

t1 -> t2 |
t1 -> t2 |
ViennaPartialFunctionType | BlockClosure |

t1 +> t2 |
t1 +> t2 |
ViennaTotalFunctionType | BlockClosure |

compose t of f1 : t1 f2 :- t2 t3 end |
ViennaType compose: ‘t’ of: {{ f1 . false . t1}.{ f2 . true . t2}.{nil . false . t3}} |
ViennaCompositeType | ViennaComposite |

t inv pattern==expr |
t inv: [:v | expr] |
ViennaConstrainedType | the class of t’s value |

## Functionality of VDM types

As the first class objects of Smalltalk, VDM types in ViennaTalk provides protocols shown below.

## Type discrimination

Types responds to the `includes:` message with a value as the argument.

```
ViennaType nat includes: 1
```

will return `true`, and

```
ViennaType nat includes: -1
```

will return `false`.

Type invariants are also taken into account.

```
| t |
t := ViennaType nat inv: [:n | n < 10].
t includes: 100
```

returns `false`.

## Subtyping

You can check subtype relationship by sending `<=` message to a type object.

```
ViennaType nat <= ViennaType int
```

returns true as `nat` is a subtype of `int` in VDM.

## Enumerating values

A type is a set of values. A type object can enumerate its value by sending the `do:` message if the type is a finite set.

```
| bools |
bools := OrderedCollection new.
ViennaType bool do: [ :b | bools add: b].
bools asArray
```

The result is an array of `true` and `false`.
Other `Collection` protocols such as `collect:`, `select:` and `detect:` are also implemented.

You can check if a type is enumerable or not by sending the `isEnumerable` message.

```
| t |
t := ViennaType bool * ViennaType nat.
t isEnumerable
```

returns `false` because `nat` is infinite set.

## Composing a value

A composite type can create a value by sending the `applyTo:` message.

```
| t |
t := ViennaType
compose: 'T'
of: { { 'f' . false . ViennaType nat}.
{ nil . false . ViennaType bool optional } }.
t applyTo: { 1 . nil }
```

returns a composite value that represents `mk_T(1, nil)`.