Recall these laws of weakest precondition (wp) with respect to a predicate:
wp Assignment Law: wp[x:=E,Q] ≡ Q[x:=E] ∧ def(E)
In cases where we can safely assume that E is well-defined, we ignore the def(E) conjunct.
wp Conditional Law: wp[IF,Q] ≡ (B ⇒ wp[S,Q]) ∧ (¬B ⇒ wp[T,Q])
where IF is the statement if B { S } else { T }
where B is a guard (i.e., boolean expression) and both S and T are statements (or sequences thereof).
wp Sequential Composition Law: wp[S;T,Q] ≡ wp[S, wp[T,Q]]
where each of S and T is a statement (or sequence thereof).
In the file hw3_s26.dfy are several Dafny methods involving assignment statements, conditional statements, and one instance of a sequential composition of statements. The first method (which is a solution to Exercise 2.18 in the Program Proofs textbook) is fully annotated with assert statements, as well as comments indicating the order in which those assert were placed into the code. That order reflects a process during which, starting with the method's postcondition (and working upwards), an attempt was made to calculate wp[S,Q], where S is the method's body and Q is its postcondition (i.e., the conjunction of the predicates in the method's ensures clauses).
Having finally calculated that the weakest precondition of the method's body is x == 50, that predicate was chosen as the method's precondition (as indicated in the method's requires clause).
Where it seemed fruitful, assert statements were inserted for the purpose of simplification. For example, (3.1) was inserted in the line preceding (3) because it is equivalent to, but simpler than, (3). The same relationship holds between (4.1) and (4). The same applies to (5.1) and (5) and then (5.2) and (5.1). (5.2), being the (simplest rendition of the) weakest precondition of the method body with respect to its postcondition, was chosen to be the method's precondition (and thus appears in the method's requires clause).
The student's task is to annotate the remaining methods in a similar fashion, with the goal of making each one's requires clause be the weakest it could possibly be while at the same time being verifiable by Dafny.
For the purpose of making the given program syntactically correct, each method's requires clause makes true its precondition. In most cases you will need a stronger precondition to enable Dafny to verify the method.