Problem Set 1

Basic information

Problem Set 1 covers Chapter 1 (Dafny mechanics) and Chapter 2 (Specification).

Submissions will be done via the autograder.io website. Links below. You need to login with a @gmail.com email address.

You can get the code by cloning/pulling on the code repo:

git clone git@github.com:GLaDOS-Michigan/boost-2025.git

You can also find individual files linked below.

Submission rules

• You may not use /* */ comments. These are reserved for use by the autograder.
• You must leave the existing /* */ comments in place.
• You can only change text between /*{*/ and /*}*/ markers.
  For example, in the following code, only the 5 < 3 part of the text is editable. Changing any other parts of the text will result in the autograding rejecting this exercise.
  

  //#title Lemmas and assertions
  
  lemma IntegerOrdering()
  {
    // An assertion is a **static** check of a boolean expression -- a mathematical truth.
    // This boolean expression is about (mathematical) literal integers.
    // Run dafny on this file. See where it fails. Fix it. 
    assert /*{*/ 5 < 3 /*}*/;
  }

  
  
• You must submit all files that are required for verifying any exercises you have completed, even if those files do not have any editable regions.
• You are not allowed to introduce axioms or otherwise trivialize the solution (for example, by requires false).

You can (and should) use your local Dafny installation to check whether your solution verifies before submitting to the autograder. Note, however, that the autograder sometimes includes additional checks to ensure that your definitions are correct. It is therefore possible that a file which locally verifies will not succeed when submitted to the autograder.

Chapter 1 - Dafny Mechanics

Chapter 1 includes a number of exercises on Dafny mechanics. You will find most exercises rather simple (though the last few are non-trivial).

Submission link here.

Exercise checklist

You can use the following checklist to track your progress on Chapter 1 exercises. The page will remember which boxes you have checked.

• exercise01.dfy Lemmas and assertions
  
• exercise02.dfy Boolean logic
  
• exercise03.dfy Functions
  
• exercise04.dfy Predicates
  
• exercise05.dfy Sets
  
• exercise06.dfy More set tools
  
• exercise07.dfy Sequences: Literals, indexing
  
• exercise08.dfy Sequences: Slices
  
• exercise09.dfy Sequences: Types, Cardinality
  
• exercise10.dfy Type synonyms
  
• exercise11.dfy Struct (product) datatypes
  
• exercise12.dfy include directive and Union (sum) datatypes
  
• exercise13.dfy More with algebraic datatypes
  
• exercise14.dfy Quantifiers
  
• exercise15.dfy Maps. Set, Map and Sequence comprehensions
  
• exercise16.dfy Hoare Logic: IsEven
  
• exercise17.dfy Fibo recursion challenge
  
• exercise20.dfy Binary search
  
• exercise21.dfy Binary tree is sorted
  
• exercise22.dfy Binary tree search
  

Chapter 2 - Specification

Chapter 2 covers specification.
Submission link here.

Exercise checklist

You can use the following checklist to track your progress on Chapter 2 exercises. The page will remember which boxes you have checked.

• exercise01.dfy IsPrime spec
  
• exercise02.dfy IsPrime implementation
  
• exercise04.dfy Merge sort