C.29.2:11.1 - Meaning and correctness before a larger claim

The current Dafny tutorial, “Loop Invariants” and “Termination”, demonstrates constructing a preserved relation to the answer and proving progress separately. Adapt that practice in :4.4 and :5.1: a short manual argument can establish the finite interpreter’s stated semantics; a few traces cannot establish its whole input class. Mechanized checking is a serious alternative when program complexity or assurance needs justify its specification and proof effort. Reopen the choice when the procedure or required assurance becomes too large for the retained argument.