Integer Division and Modulo
Working with division and modulo requires extra care, as Logika is finicky about both.
Division
Recall that Z (int) is the only numeric type in Logika, so any division is integer division. This means something like 9/2 evaluates to 4, just as it would in Java or C#.
Check for division by zero
Before doing division of the form numerator/denominator, either in a line of code or in a logic block, you must have a line in a previous logic block that states: denominator != 0. Other forms, such as denominator > 0 or 0 != denominator, will not work. You are even required to do this when dividing by a constant value that is obviously not zero.
For example, if we do:
import org.sireum.logika._
var x: Z = 10 / 2Then Logika will give us an error complaining we have not proved that the denominator is not zero. We must add the claim 2 != 0 as follows:
import org.sireum.logika._
l"""{
1. 2 != 0 algebra
}"""
var x: Z = 10 / 2Note that our justification is just, algebra, as we don’t need any extra information to claim that 2 is not equal to 0.
Pitfalls
Be careful when making claims that involve division. For example, the following claim will not validate in Logika:
l"""{
1. x == (x/3)*3 algebra //NO!
}"""While the claim x == (x/3)*3 is certainly true in math, it is not true with integer division. For example, if x is 7, then (x/3)*3 is 6 – so the two sides are not equal. In general, I recommend avoiding claims involving division if you can at all help it. Instead, try to find a way to express the same idea in a different way using multiplication.
Modulo
Modulo (%) works the same way in Logika as it does in other programming languages. For example, 20 % 6 evaluates to 2.
Modulo checks on numerator and denominator
Before using the modulo operator in the form numerator % denominator, either in a line of code or as a claim in a logic block, you must have EXACTLY these claims in the previous logic block:
numerator >= 0denominator > 0
For example:
...
l"""{
1. 2 > 0 algebra
2. a >= 0 (some justification)
}"""
x = a % 2
...Example
Consider the following Logika program:
import org.sireum.logika._
var num: Z = readInt("Enter positive number: ")
assume(num > 0)
val orig: Z = num
num = num * 2
assert(num % 2 == 0)
num = num + 2
assert(num % 2 == 0)
num = num/2 - 1
assert(num == orig)It can often be handy to walk through a program with sample numbers before trying to prove its correctness:
- Suppose our input value,
num, is 11 origis initialized to be 11 alsonumis multiplied by 2, and is 22- It makes sense that
numwould be even, since any number times two is always even (and indeed, 22 is even) - We add 2 to
num, so it is now 24 - It makes sense that
numwould still be even, as it was even before and we added 2 (another even number) to it. Indeed, 24 is still even. - We update
numby dividing it by 2 and subtracting 1, sonumis now back to its original value of 11 (the same asorig). This step “undoes” the changes we have made tonum– looking at the code, we can see that the final value ofnumisorig*2 + 2, so if we do(orig*2 + 2) / 2 - 1, we are left withorig.
Here is the completed verification, with comments at each step:
import org.sireum.logika._
var num: Z = readInt("Enter positive number: ")
assume(num > 0)
val orig: Z = num
num = num * 2
l"""{
1. num == num_old * 2 premise //we updated num to be its old value times 2
2. orig == num_old premise //orig equaled the old value of num (before our change)
3. num == orig * 2 algebra 1 2 //express the new value of num without referring to "_old"
4. 2 > 0 algebra //needed to use modulo in step 7
5. num_old > 0 premise //we assumed the old value of num (before its change) was > 0
6. num >= 0 algebra 1 5 //needed to use modulo in step 7
7. num % 2 == 0 algebra 1 //we have showed num is now even (needed for next assert)
}"""
assert(num % 2 == 0)
num = num + 2
l"""{
1. num == num_old + 2 premise //we updated num to be its old value plus 2
2. num_old >= 0 premise //from line 6 in previous block, but num has since changed
3. num_old % 2 == 0 premise //from line 7 in previous block, but num has since changed
//we know 2 > 0 from previous block - don't need to restate here
4. num >= 0 algebra 1 2 //needed to use modulo in step 5 (need to redo since num has changed)
5. num % 2 == 0 algebra 1 3 //we have showed num is still even (needed for next assert)
6. num_old == orig * 2 premise //from line 3 in block above, but num has since changed
7. num - 2 == orig * 2 algebra 1 6 //express new value of num without using "_old"
}"""
assert(num % 2 == 0)
l"""{
1. 2 != 0 algebra //needed for dividing by 2
}"""
num = num/2 - 1
l"""{
1. num == num_old/2 - 1 premise //we updated num to be its old value divided by 2 minus 1
2. num_old - 2 == orig * 2 premise //from line 7 in previous block, but num has since changed
3. num_old == orig * 2 + 2 algebra 2
4. num == (orig * 2 + 2)/2 - 1 algebra 1 3 //express new value of num without using "_old"
5. num == orig + 1 - 1 algebra 4
6. num == orig algebra 5 //we have showed num is back to being orig (needed for last assert)
//could have skipped straight here with "algebra 1 2"
assert(num == orig)Sometimes it can be tricky to figure out what to do at each step in order to get assert statements to pass. If you are unsure what to do, I recommend:
-
Walk through the program several times with sample numbers, keeping track of changes to variables. Why do the assert statements make sense to you? Convince yourself that they are valid claims before you worry about the formal verification.
-
Add a logic block after each variable mutation. Work from the top down:
- Write a premise for every variable assignment and assume statement since the previous logic block.
- Find all claims in the logic block just before you that do not use an “_old” reference – pull each claim into your current block, using an “_old” reference as needed for the most recently changed variable.
- Manipulate your claims that use an “_old” reference until you have statements that capture the current value of the recently changed variable that do not reference “_old”
- If your next statement is an assert, manipulate your claims until you have exactly the claim in the assert.
- If any claims
-
Add a logic block before each use of division (
numerator / denominator) and modulus (numerator % denominator). Pull in claims from previous blocks as described above to help you show what is needed aboutnumeratoranddenominator:- For division, build to the claim
denominator != 0 - For modulo, build to the claims
numerator >= 0anddenominator > 0 - If you can, avoid using division in logic block claims
- For division, build to the claim