Here is a Dafny proof of the “exercise for the reader” from section 5 of E.W.Dijkstra’s “Notes on Structured Programming” monograph in the book “Structured Progr…