I have a homework problem that uses the Logika program that I need help with. Here is the problem:

3. Apropos of Election Day, Program 3 contains half the logic for a program, which calculates the winner by opening a single (to avoid a loop) unopened ballot. Be sure to understand the reasoning of the program to declare a winner.

Below is the file 3.logika that corresponds with this problem and with comments instructing what needs to be done. The file can be pasted into the Logika program for modification. The code in this file needs to be modified to be logika verified through the logika program:

 import org.sireum.logika._ // Declare variables to hold the total number of ballots and the // majority of votes ("half the total") necessary to win // Note: this is not a realistic way to address a voting situation (we should calculate // what is necessary to win, and we should count the total as we go, but we // make this simplifying assumption for this assignment) val totalvotes: Z = readInt("total number of votes: ") val halfvotes: Z = readInt("total number of votes: ") // Get the count of uncounted ballots var unopenvotes: Z = readInt("number of unopened votes: ") // Get the counts of what was counted manually up to this point var candidate1votes: Z = readInt("number of votes candidate1 get so far: ") var candidate2votes: Z = readInt("number of votes candidate2 get so far: ") // Initialize the "winner" variable (to be set to either candidate "1" or "2") var winner: Z = 0 // Assume some consistency properties assume (totalvotes == unopenvotes + candidate1votes + candidate2votes) assume (totalvotes == 2 * halfvotes) // 1: for candidate1 // 2: for candidate2 val vote: Z = readInt("read in the vote: ") // assume that vote should be valid that it's either for candidate1 or candidate2 assume (vote == 1 | vote == 2) // the unopened votes is decreased by 1 unopenvotes = unopenvotes - 1 if (vote == 1) { candidate1votes = candidate1votes + 1 } else { candidate2votes = candidate2votes + 1 } if (candidate1votes > candidate2votes & candidate1votes > halfvotes) { winner = 1 } else { // pass -- we leave this "else" branch below for some proof steps } // similar for candidate2, it's ignored here for simplification of this homework // if(candidate2votes > candidate1votes & candidate2votes > halfvotes) { // winner = 2 // } else { // // pass // } // prove that the following assertions hold assert (totalvotes == unopenvotes + candidate1votes + candidate2votes) // assert ((winner == 1)  (candidate1votes > candidate2votes and candidate1votes > halfvotes)) // Our assertion language does not have implication so represent the implication in terms of // disjunction "|" and not "!" assert (!(winner == 1) | (candidate1votes > candidate2votes & candidate1votes > halfvotes))