I have a homework problem that I need help with that uses Logika:

6. Program 6.logika selects the median of 3 numbers. Note the opening assumptionit is included to make this problem substantially shorter.

Below is the file 6.logika associated with this problem. This needs to be logika verified:

import org.sireum.logika._ val X1 : Z = readInt() val X2 : Z = readInt() val X3 : Z = readInt() var Min: Z = readInt() var Max: Z = readInt() var M: Z = readInt() // get the median of the three numbers: X1, X2 and X3 assume (X1 <= X2) if (X2 <= X3) { M = X2 Min = X1 Max = X3 } else { if (X1 <= X3) { M = X3 Min = X1 Max = X2 } else { M = X1 Min = X3 Max = X2 } } // your goal is to prove that the following assertion holds assert(Min <= M & M <= Max)