Sequences in Functions

Sequences in Logika 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 above 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)).

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:

requires seq.size > 0

If we wanted to require that all values in a sequence parameter (say, nums) be between 10 and 20, we would write:

requires ∀ x: (0..<nums.size) (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:

l"""{
    requires (preconditions)
    modifies (sequences/globals changed in this function)
    ensures (postconditions)
}"""

Until this point, we have been leaving off the modifies clause because our functions have not used sequences or global variables. We now need to include that clause whenever a function CHANGES the values in a sequence parameter. 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

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

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 result keyword for describing the function’s return value in the postcondition. For example, if a function was returning the smallest value in the sequence nums, we would say:

ensures ∀ x: (0..<nums.size) result <= nums(x)
    ∃ x: (0..<a.size) result == 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 large 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 bool) all elements in the sequence a are negative. Our postcondition would be:

ensures (∀ x: (0..<nums.size) nums(x) < 0) → (result == true)
    (∃ x: (0..<nums.size) nums(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:

ensures 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 sequenceName_in 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
    ∀ x: (1..<seq.size) seq(x) == seq_in(x)

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

Postcondition: size doesn’t change

Logika has an oddity with programs that modify sequence parameters – in those cases, you must also include as a postcondition that the size of the sequence will not change (i.e., that the resulting sequence size will equal the original sequence size. For example, if a function modified the sequence seq, we would need to add the postcondition:

seq.size == seq_in.size

Logika is concerned that any function that modifies a sequence might also change the size of that sequence. While it is possible to append and prepend to Logika sequences (much like with Python lists), we cannot do so to sequence parameters. As a rule, Logika functions cannot assign to ANY parameter value (they are read-only). However, we still must state that the size doesn’t change or the program will not be verified. Whenever you list a sequence in the modifies clause to a function, you must also include a postcondition to say that its size doesn’t change.

If you are writing a function that uses a sequence parameter but doesn’t change that parameter, you should not list that sequence in a modifies clause, and you should not state that the sequence size doesn’t change (or anything else about the ..._in value of the sequence).

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 in Logika’s symexe mode:

import org.sireum.logika._

//"Unit" is like a void return type
def makeFirstZero(seq: ZS): Unit = {
    l"""{
        requires seq.size >= 1  //we need at least 1 element
        modifies seq            //we are changing the sequence
        ensures
            //we promise the first element will be a 0
            seq(0) == 0

            //we promise every other element is the same as its original value
            A x: (1..<seq.size) seq(x) == seq_in(x)

            //we promise the sequence size won't change
            seq.size == seq_in.size
    }"""

    seq(0) = 0
}

///// Test code ///////////

var nums: ZS = ZS(1,2,3)
makeFirstZero(nums)

//we want to claim that nums is what it was, but with the first
//element as a 0
assert(nums == ZS(0,2,3))

Example: swap program

Suppose we have the following swap program:

import org.sireum.logika._

def swap(list: ZS, pos1: Z, pos2: Z): Unit = {
    var temp: Z = list(pos1)
    list(pos1) = list(pos2)
    list(pos2) = temp
}

///////////// Calling 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 list_in(pos2))
  • list(pos2) has the value that was originally at list(pos1) (i.e, the value at list_in(pos1))
  • All other positions are unchanged (i.e., they are the same as they were in list_in)
  • The size doesn’t change (which we must always list if a sequence is modified)

We can now complete the function contract for swap:

import org.sireum.logika._

def swap(list: ZS, pos1: Z, pos2: Z): Unit = {
    l"""{
        //pos1 and pos2 need to be valid positions
        requires pos1 >= 0
            pos2 >= 0
            pos1 < list.size
            pos2 < list.size
        modifies list
        ensures
            list(pos1) == list_in(pos2)
            list(pos2) == list_in(pos1)
            list.size == list_in.size

            //all the other spots stay the same
            A x:(0..<list.size) (x != pos1 ^ x != pos2) -> list(x) == list_in(x)
    }"""

    var temp: Z = list(pos1)
    list(pos1) = list(pos2)
    list(pos2) = temp
}

///////////// Calling 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))

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.

5.18.0

Last modified by: Julie Thornton Apr 28, 2023