6.S057: 6.S057: Verified Software Engineering

Problem Set 9

Loops

The deadline for this problem set is Wednesday, November 25 at 9pm.

Submit your work on Gradescope at Problem Set 9.

Before you start this problem set

Please fill out a survey about the time you spent on Problem Set 8.

Download

The structure here follows that of previous psets: read pset09_definitions.dfy to see our supporting definitions, complete pset09.dfy with implementations of verified methods, and use pset09_validator.dfy to confirm you’re done.

Recursive specs, iterative implementations. // This problem set is about practing with loops, so we’re going to impose an // extra rule: no method that we ask you to write should execute a recursive // call, whether in a method or a function. You’ll want to make use of // recursive functions in specifying and proving methods, but those // functions should only appear in ghost code, present only for verification // purposes.

See also pset09_hints.dfy for suggestions, in case you get stuck. But beware that this file may give away some of the interesting challenges.

Copyright 6.S057 course staff.