An attempt to apply formal methods (D. Gries style) to specification and verification of code-writting tasks for CS students.