1. Complete the ReconstructFromMaxSum() method in the given Dafny program so that it verifies. As indicated in Exercise 1.8 of the Program Proofs textbook, the method needs a precondition (i.e., stronger than true) in order to make implementation feasible. Missing are that precondition and the body of the method.
2. Complete the Median() method in the given Dafny program so that it verifies. Remember that ghost functions can be referred to within assert statements but not within code that is intended to be compilable. (Here, the Median() method is intended to be compiled.) You are encouraged to use assert statements freely, with at least one occurring in each of the (probably) several branches of nested if-else statements.
Also recall that functions can include if-then-else expressions, the syntax of which is different from the if-else statements in methods:
if <boolean_expr> then <expression> else <expression> |
if <boolean_expr> {
<statement>
}
else {
<statement>
}
|
| if-then-else expression | if-else statement |
|---|