# Logika Modes

Logika has different modes for programming logic verification. We can switch between modes by going to File->Settings->Tools->Sireum->Logika.

## Logika’s “manual” mode

Up to now, we have been running Logika in “manual mode”, which uses these Logika settings:

We are now reaching the point where additional practice in manual mode may no longer be a learning activity, and where the proof-blocks after claim transformations can become dozens of lines long.

## Logika’s SymExe mode

In Chapter 10, we will be switching to Logika’s “symexe mode”, which uses these Logika settings:

Symexe mode allows us to reason about our program by using ONLY invariants and function contracts. While the same work has to be done for a program to be verified (the precondition must be true before a function call, the loop invariant must be true before the loop begins, etc.), symexe mode does the work of analyzing your program statements to ensure that all parts of your loop invariant and function contract are satisified. When you use symexe mode, you will only need to include a function contract for each function and a loop invariant block for each loop, and it will do the grunt work.

### Multiplication example

In section 9.3, we did a verification of a multiplication a program using Logika’s manual mode. Here is how we would write the verification of the same program using Logika’s symexe mode:

``````import org.sireum.logika._

def mult(x: Z, y: Z) : Z = {
//function contract
l"""{
requires y >= 0         //precondition: y should be nonnegative
ensures result == x*y   //postcondition (we promise to return x*y)
}"""

var sum: Z = 0
var count: Z = 0

while (count != y) {
l"""{
invariant sum == count*x
modifies sum, count
}"""

sum = sum + x
count = count + 1
}

return sum
}

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

var one: Z = 3
var two: Z = 4

var answer: Z = mult(one, two)