1
$\begingroup$

For a homework assignment I am asked to provide claim sequences to verify that the given conditional does indeed satisfy its specification (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?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.