# Correctness of Simple Programs

For a homework assignment I am asked to provide claim sequences to verify that the given conditional does indeed satisfy its speciﬁcation (to compute in r the absolute value of x).

val x: Z = readInt()
var r: Z = x

l"""{ 1. r == x               premise }"""

if (x < 0) {
l"""{
1. x < 0              premise
2. r = x              premise
3. r < 0              algebra 1 2
}"""
r = -x
l"""{
1. r = -x                premise
2. x < 0                 premise
3. r_old < 0             premise
}"""
} else {
l"""{
//   also in this branch, you must prove all the 3 assertions
}"""
}
assert(!(x < 0)  | r == -x)   // if x < 0 then r = -x
assert(!(x > 0)  | r ==  x)   // if x > 0 then r = x
assert(!(x == 0) | r ==  0)   // if x = 0 then r = 0


This is the code we are given to start and are asked to prove the 3 assertions. Im having trouble starting out because I am not sure what structure I need to use. Do I need 3 sub proofs in each conditional in order to prove the three assertions?