Problem Set 2

Basic information

Problem Set 2 covers Chapter 3 (State machines) and Chapter 4 (Invariants).

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 3 - State machines

Chapter 2 includes exercises on state machines. You will notice that exercise03 is written in a slightly different style (called Jay Normal Form). This is an optimized variant for the Next predicate, which gathers all the non-deterministic parameters into a single exists. Its general form is the following:

datatype Step = 
  | Action1Step( <parameters> )
  | Action2Step( <parameters> )
  ...

ghost predicate NextStep(v: Variables, v’: Variables, step:Step)
{
  match step
    case Action1Step(<parameters>) => Action1(v, v’, <parameters>)
    case Action2Step(<parameters>) => Action2(v, v’, <parameters>)
    ...		
}
predicate Next(v: Variables, v’: Variables)
{
    exists step :: NextStep(v, v’, step)
}

Submission link here.

Exercise checklist

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

• exercise01.dfy Coke machine
  
• exercise02.dfy Dining philosophers
  
• exercise03.dfy Single-server Lock Service Protocol
  

Chapter 4 - Invariants

Chapter 4 covers (inductive) invariants.
Submission link here.

Exercise checklist

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

• exercise01.dfy Crawler
  
• exercise02.dfy Single-Server Lock Service Proof
  
• exercise03.dfy Crawler quadrants