Intro to Sequences

Sequences in Logika are fairly similar to lists in Python and arrays in Java and C#. As with lists and arrays, Logika sequences are ordered. Each element is stored at a particular (zero-based) position, and there are no gaps in the sequence.

Logika sequences can either store integers (type ZS) or booleans (type BS).

Sequence syntax

We can create new sequence variables like this:

//creates the sequence (5, 10, 15)
var seq: ZS = ZS(5,10,15)

//creates the sequence (false, true)
var bools: BS = BS(false, true)

//creates an empty sequence of integers
var empty: ZS = ZS()

Given the following sequence:

var a: ZS = ZS(1, 2, 3)

Here is a table of the different sequence operations we will use in this course:

Sample program with a sequence

Here is a sample Logika program that uses a sequence. The makeFirstZero function sets the first element in a sequence to 0:

import org.sireum.logika._

//"Unit" is like a void return type
def makeFirstZero(seq: ZS): Unit = {
    seq(0) = 0
}

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

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

makeFirstZero(nums)
assert(nums == ZS(0,2,3))

This program will not run (or be verified) as we have not yet provided a function contract for makeZeroFirst. We will complete the verification for the program later in the section.

Predicate logic statements with sequences

When we write function contracts and loop invariants with sequences, we will need to make statements about all or some elements in a sequence. We can do this with predicate logic statements.

Statements about all sequence elements

As we did in chapters 4 and 5, we will use the universal (∀) quantifier for statements involving all elements in a sequence. The basic forms of specifying some claim P(a(x)) holds for every element in a sequence a are:

Here are several sample claims and explanations about integer sequence a:

Statements about some sequence elements

We will use the existential (∃) quantifier for statements involving one or more elements in a sequence. The basic forms of specifying claims is the same as for the universal quantifier, but using the existential quantifier instead of the universal quantifier.

Here are several sample claims and explanations about integer sequences a and b: