Assignment 5

This assignment continues to build up MiniDafny and focuses on verification conditions.

You should download VCGen.hs. This contains just the template for the exercise. You should add this file to your directory with the previous MiniDafny homeworks - it operates on the same syntax. You should also modify the miniDafny.cabal file to include VCGen under the “exposed-modules” in the library and “other-modules” in the executable. Fill in VCGen.hs by following its instructions and submit just that file through Gradescope.

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