Assignment 6

This assignment continues to build up MiniDafny and focuses on weakest preconditions.

You should download WeakestPrec.zip. This contains the template for the exercise - the standard stack/cabal boilerplate, as well as a few Haskell files. There are minor difference in Syntax clearly marked so. If you want to use your Parser and Pretty printer, you’ll have to update them to simplify Predicates and While Loop invariants. The WP.hs file actually contains your homework: fill in that file by following its instructions and submit just that file through Gradescope.

The deadline for this is Friday, April 19th, 11:59 pm Eastern.