- Evaluating
`[x | x in set {2,...,5} & x > 2] = [3,4,5]`

`[x | x in set {3,5,2,4} & x*x > 22] = [2,3,4]`

- Express the following in VDM-SL:
- The sequence L has less than 5 distinct elements:
`card elems L < 5`

- The sequence L has no duplicated elements:
`card elems L = len L`

- The sequences L1 and L2 are non-empty and are disjoint (i.e. they have no elements in common):
`L1 <> [] and L2 <> [] and elems L1 inter elems L2 = {}`

- Write an explicit function definition for the inds operator.

```
Inds: seq of X -> set of nat
Inds(L) == {1,...,len L}
```

- If
`L`

is of type`seq of (seq of nat)`

, write an expression which says that all the sequences in`L`

are disjoint.

```
forall L1,L2 in set elems L & L1 <> L2 => elems L1 inter elems L2 = {}
```

```
Notice that the following is incorrect:
```

```
forall L1,L2 in set elems L & elems L1 inter elems L2 = {}
```

because `L1`

and `L2`

could evaluate to the same element sequence in `L`

. The erroneous expression above is going to be false for any `L`

except the sequence containing only the empty sequence (i.e. the case where `L = [[]]`

).

```
types
Array = seq of int
inv A == len A >=1;
functions
NoOverlap: Array * Array * nat * nat -> bool
-- no value in A between j and k is in B between k+1 and N
NoOverlap(A,B,j,k) ==
elems A(j,...,k) inter elems B(k+1,...,len B) = {}
pre j>=1 and k >=1 and j<=len A and k <= len A and k <= len B;
-- Tests: (a1,a2,1,3) - false; (b1,a2,3,4) - true
PerfectSquares: Array -> bool
PerfectSquares(A) ==
forall i in set inds A & A(i)=(len A - i + 1) * (len A - i + 1);
values
c1: Array = [3,6,7]; -- false
c2: Array = [16,9,4,1]; -- true
```

```
types
Line = seq of char;
functions
NumberOfOccur: char * Line -> nat
-- number of occurences of x in p
NumberOfOccur(x,p) == card {i| i in set inds p & p(i) =x};
NumOfDistinctEls: Line -> nat
-- returns number of distinct elements in p
NumOfDistinctEls(p) == card elems p;
Distance: Line * Line -> nat
-- returns number of distinct elements that are either in A or B but
-- not in both
Distance(A,B) ==
card ((elems A \ elems B) union (elems B \ elems A));
```

```
functions
Average: seq of real -> real
Average(L) ==
Sum(L) / len L;
Sum: seq of real -> real
Sum(L) ==
if L = []
then 0
else hd L + Sum(tl L)
```

```
types
X = token -- it could be defined to anything
-- using full VDM-SL these functions could actually be defined as polymorphic functions.
functions
Reverse: seq of X -> seq of X
Reverse(L) ==
if L = []
then []
else Reverse(tl L) ^ [hd L];
Reverse2: seq of X -> seq of X
Reverse2(L) ==
[L(len L + 1 - i) | i in set inds L];
```