# Sequences in Functions

Sequences in Scala are passed to functions by reference. This means that if a function makes changes to a sequence parameter, then it will also change whatever sequence object was passed to the function. For example, the test code below passes `nums`

, which has the value `ZS(1,2,3)`

, to the `makeFirstZero`

function. The `makeFirstZero`

function changes the first position in its parameter (`seq`

) to be 0, which means that the `nums`

sequence in the test code will also have its first position set to 0 (making it have the value `ZS(0,2,3)`

).

```
// #Sireum #Logika
//@Logika: --background save
import org.sireum._
def makeFirstZero(seq: ZS): Unit = { // Unit is like void in Java and C#
seq(0) = 0
}
///////////// Test code /////////////////
var nums: ZS = ZS(1,2,3)
makeFirstZero(nums)
assert(nums == ZS(0,2,3))
```

## Preconditions with sequences

When writing the precondition for a function that takes a sequence parameter, we must consider whether our function will only work correctly for particular sequence values or sizes. For example, our `makeFirstZero`

function will not work if the size of the `seq`

parameter is zero. We would need to add this requirement to the function’s precondition (to its `Requires`

clause):

`seq.size > 0`

If we wanted to require that all values in a sequence parameter (say, `nums`

) be between 10 and 20, we would add the following to the precondition:

`∀ (0 until nums.size)(x => (nums(x) >= 10 ∧ nums(x) <= 20))`

Sometimes, functions with sequence parameters will work for any size/values – in those cases, we don’t need to list anything about the sequence in the precondition.

## Function `Modifies`

clause

We learned in chapter 9 that the format of a function contract is:

```
Contract(
Requires ( preconditions ),
Ensures ( postconditions )
)
```

However, there is actually a third portion of the function contract that we have ommitted until this point – the `Modifies`

clause. This clause is required whenever a function changes the values in a sequence parameter or changes global variables. For example, the `makeFirstZero`

function DOES change its sequence parameter, `seq`

, as it sets its first position to 0. `makeFirstZero`

should therefore include this `Modifies`

clause:

`Modifies ( seq ),`

This clause goes between the precondition (`Requires`

) and the postcondition (`Ensures`

), making the new template for the function contract look like this:

```
Contract(
Requires ( preconditions ),
Modifies ( comma-separated list of sequences/global variables modified by the function ),
Ensures ( postconditions )
)
```

If the function modifies more than one sequence or global variable, they are listed together in a comma-separated list in the `Modifies`

clause.

## Postconditions with sequences

When writing the postcondition for a function that uses a sequence parameter, we must consider two things:

- How the return value relates to the sequence
- How the function will change the sequence

### Relating return values to sequence elements

We will still use the `Res[Type]`

keyword for describing the function’s return value in the postcondition. For example, if a function was returning the smallest value in the integer sequence `nums`

, we would say:

```
Ensures(
∀ (0 until nums.size)(x => (Res[Z] <= nums(x))),
∃ (0 until nums.size)(x => (Res[Z] == nums(x)))
)
```

Here, the first postcondition states that our return value will be less than or equal to every value in the sequence, and the second postcondition states that our return value is one of the sequence elements. (The second postcondition prevents us from sneakily returning some negative number and claiming that it was the smallest element in the sequence, when in fact it wasn’t one of the sequence elements.)

Sometimes, our postconditions will promise to return a particular value if some claim about the sequence is true. Suppose we have a function that returns whether or not (i.e., a boolean) all elements in the sequence `a`

are negative. Our postcondition would be:

```
Ensures(
( ∀ (0 until a.size)(x => (a(x) < 0)) ) → (result == true),
( ∃ (0 until a.size)(x => (a(x) >= 0)) ) → (result == false),
)
```

Here, the first postcondition promises that if all sequence elements are negative, then the function will return true. The second postcondition promises the opposite – that if there is a nonnegative sequence element, then the function will return false.

### Describing how the function changes the sequence

Consider again the `makeFirstZero`

function:

```
def makeFirstZero(seq: ZS): Unit = {
seq(0) = 0
}
```

This function doesn’t return anything (hence the `Unit`

return type), but we do need to describe what impact calling this function will have on the sequence. We can partially accomplish our goal with this postcondition (in our `Ensures`

clause):

`seq(0) == 0`

Which promises that after the function ends, the first value in the sequence will be 0. However, suppose we wrote this instead for the `makeFirstZero`

function:

```
def makeFirstZero(seq: ZS): Unit = {
seq(0) = 0
seq(1) = 100
}
```

This version of the function DOES satisfy the postcondition – the first element is indeed set to 0 – but it changes other elements, too. The postcondition should be descriptive enough that anyone calling it can be certain EXACTLY what every single value in the sequence will be afterwards. Our postcondition needs to describe exactly what values in the sequence WILL change and exactly what values WON’T change.

This means that our `makeFirstZero`

function needs to state that the first element in `seq`

gets set to 0, and that every other value in the sequence *stays the same as its original value*. To help us describe the *original value* of a sequence, we can use the special `In(sequenceName)`

syntax, which holds the value of a sequence parameter `sequenceName`

at the time the function was called. (This `In`

syntax can only be used in logic blocks, not in the code.)

We can specify exactly what happens to each sequence element in our first version of `makeFirstZero`

like this:

```
Ensures(
seq(0) == 0,
∀ (1 until seq.size)(x => ( seq(x) == In(seq)(x)))
)
```

The second postcondition says: “All elements from position 1 on keep their original values”.

## Example: finished `makeFirstZero`

verification

Now that we have seen all the pieces of writing function contracts for functions that work with sequences, we can put together the full function contract for our `makeFirstZero`

function. The assert statement in the test code will be verified by Logika’s auto mode:

```
// #Sireum #Logika
//@Logika: --background save
import org.sireum._
def makeFirstZero(seq: ZS): Unit = {
Contract(
Requires( seq.size > 0 ),
Modifies( seq ),
Ensures(
seq(0) == 0,
∀ (1 until seq.size)(x => ( seq(x) == In(seq)(x)))
)
)
seq(0) = 0
}
//////////////// Test code //////////////
var nums: ZS = ZS(1,2,3)
makeFirstZero(nums)
assert(nums == ZS(0,2,3))
```

## Example: swap program

Suppose we have the following swap program:

```
// #Sireum #Logika
//@Logika: --background save
import org.sireum._
def swap(list: ZS, pos1: Z, pos2: Z): Unit = {
val temp: Z = list(pos1)
list(pos1) = list(pos2)
list(pos2) = temp
}
///////////// Test code ///////////////////
var testList: ZS = ZS(1,2,3,4)
swap(testList,0,3)
//the values in positions 0 and 3 should be swapped
//all other elements should be the same
assert(testList == ZS(4,2,3,1))
```

Here, `swap`

takes an integer sequence (`list`

) and two positions (`pos1`

and `pos2`

). It uses a temp variable to swap the values in `list`

at `pos1`

and `pos2`

. We would like to write an appropriate function contract so the assert statement in the test code holds.

We must first consider the precondition – does `swap`

have any requirements about its parameters? Since `swap`

uses `pos1`

and `pos2`

as positions within `list`

, we can see that `swap`

will crash if either position is out of bounds – either negative or past the end of the sequence.

The function is changing the sequence, so we will need a `Modifies`

clause. Finally, we must consider the postcondition. This function isn’t returning a value, but it is changing the sequence – so we should describe exactly what values HAVE changed (and their new values) and what values have NOT changed. We want to say that:

`list(pos1)`

has the value that was originally at`list(pos2)`

(i.e, the value at`In(list)(pos2)`

)`list(pos2)`

has the value that was originally at`list(pos1)`

(i.e, the value at`In(list)(pos1)`

)- All other positions are unchanged (i.e., they are the same as they were in
`In(list)`

) - The size doesn’t change (which we must always list if a sequence is modified)

We can now complete the function contract for `swap`

:

```
// #Sireum #Logika
//@Logika: --background save
import org.sireum._
def swap(list: ZS, pos1: Z, pos2: Z): Unit = {
Contract(
Requires(
0 <= pos1 & pos1 < list.size, // pos1 is a valid index
0 <= pos2 & pos2 < list.size // pos2 is a valid index
),
Modifies(list), // documents list is modified
Ensures(
list(pos1) == In(list)(pos2),
list(pos2) == In(list)(pos1),
list.size == In(list).size,
∀ (0 until list.size)(x => (x != pos1 & x != pos2 → list(x) == In(list)(x)))
)
)
val temp: Z = list(pos1)
list(pos1) = list(pos2)
list(pos2) = temp
}
//////////////// Test code //////////////
var testList: ZS = ZS(1,2,3,4)
swap(testList,0,3)
assert(testList == ZS(4,2,3,1))
```

If we test this program in Logika’s symexe mode, the final assert will hold – we have enough information to make a claim about EXACTLY what the sequence will look like after calling `swap`

.

Note that we could have simplified the postcondition by using the *sequence update notation* described at the end of section 10.2. We want to say that the value of `list`

at the end of the function is equivalent to the value of list at the beginning of the function (`In(list)`

) with the following exceptions:

- The new value at
`pos1`

should be the original value at`pos2`

(`In(list)(pos2)`

) - The new value at
`pos2`

should be the original value at`pos1`

(`In(list)(pos1)`

)

Here is the equivalent (but shorter) postcondition for `swap`

:

```
Ensures(
list ≡ In(list)(pos1 ~> In(list)(pos2), pos2 ~> In(list)(pos1))
)
```