exercises.md

Index of exercises

chapter01-basics

• chapter01-basics/exercises/exercise01.dfy
  Lemmas and assertions

• chapter01-basics/exercises/exercise02.dfy
  Boolean logic

• chapter01-basics/exercises/exercise03.dfy
  Functions

• chapter01-basics/exercises/exercise04.dfy
  Predicates

• chapter01-basics/exercises/exercise05.dfy
  Sets

• chapter01-basics/exercises/exercise06.dfy
  More set tools

• chapter01-basics/exercises/exercise07.dfy
  Sequences

• chapter01-basics/exercises/exercise08.dfy
  Type synonyms

• chapter01-basics/exercises/exercise09.dfy
  Struct (product) datatypes.

• chapter01-basics/exercises/exercise10.dfy
  include directive and Union (sum) datatypes

• chapter01-basics/exercises/exercise11.dfy
  Algebraic datatypes in their full glory.

• chapter01-basics/exercises/exercise12.dfy
  More with algebraic datatypes.

• chapter01-basics/exercises/exercise13.dfy
  Quantifiers

• chapter01-basics/exercises/exercise14.dfy
  Maps. Set, Map and Sequence comprehensions.

• chapter01-basics/exercises/exercise15.dfy
  Comprehensions, the finite heuristic, axioms, recursion

• chapter01-basics/exercises/exercise16.dfy
  IsEven -- Hoare logic

• chapter01-basics/exercises/exercise18.dfy
  Fibo -- Recursion challenge.

• chapter01-basics/exercises/exercise19.dfy
  FindMax -- Loop invariants.

• chapter01-basics/exercises/exercise20.dfy
  IsSeqSorted -- Build an entire imperative loop method implementation with loop invariants.

• chapter01-basics/exercises/exercise21.dfy
  Binary Search -- Method implementation; writing a Hoare spec.

• chapter01-basics/exercises/exercise22.dfy
  Binary Tree Is Sorted -- Prove an implementation meets its spec. Practice with proof diagnosis.

• chapter01-basics/exercises/exercise23.dfy
  Binary Tree Search -- Implement search in a binary tree and prove it works. Practice with proof diagnosis.

• chapter01-basics/exercises/lib_directions.dfy -- Library for exercises 10 & 13

• chapter01-basics/exercises/lib_lunch.dfy -- Library for exercises 12 & 13

chapter02-spec

• chapter02-spec/exercises/exercise01.dfy
  IsPrime I -- Basic specification.

• chapter02-spec/exercises/exercise02.dfy
  IsPrime II -- Working with an implementation proof

• chapter02-spec/exercises/exercise03.dfy
  Merge Sort -- More specification practice.

chapter03-sm

• chapter03-sm/exercises/exercise01.dfy
  Coke Machine -- The first state machine specification exercise: fill in actions.

• chapter03-sm/exercises/exercise02.dfy
  Dining Philosophers -- A more challenging state machine: define the state datatype.

• chapter03-sm/exercises/exercise03.dfy
  Single-Server Lock Service Model -- A complex state machine including a Safety predicate on the state type.

chapter04-inv

• chapter04-inv/exercises/exercise01.dfy
  Crawler -- Introduction to inductive invariants -- implement the visualization from the lecture.

• chapter04-inv/exercises/exercise02.dfy
  Single-Server Lock Service Proof -- A more realistic invariant proof of the previous chapter's lock service.

chapter05-dsm

• chapter05-dsm/exercises/exercise01.dfy
  Two Phase Commit Model -- Model a distributed protocol using compound state machines.

• chapter05-dsm/exercises/exercise02.dfy
  Two Phase Commit Safety Specification Predicate -- Express the English Atomic Commit safety properties as predicates over the compound state machine model from exercise01.

• chapter05-dsm/exercises/exercise03.dfy
  Two Phase Commit Safety Proof -- Prove that the 2PC distributed system (exercise01) accomplishes the Safety spec (exercise02)

• chapter05-dsm/exercises/model_for_ex03.dfy -- Given model for exercise03

chapter06-refine

• chapter06-refine/exercises/exercise01.dfy
  Sharded KV Store with Synchronous Communication -- Build a refinement from a protocol (distributed sharded state) to a specification (a logically-centralized abstract map).

• chapter06-refine/exercises/exercise02.dfy
  State Machine Spec for Atomic Commit -- Build an abstract behavioral model that captures the semantics of an evolving system to use as a refinement reference for its more-complicated implementation.

• chapter06-refine/exercises/exercise03.dfy
  Property Lemmas for Atomic Commit -- The state machine model captures AC2 nicely, but let's make it very clear that the model also obeys AC1, AC3 and AC4.

• chapter06-refine/exercises/exercise04.dfy
  Refinement proof for 2PC -- Show that Two Phase Commit refines the Atomic Commit sate machine spec.

• chapter06-refine/exercises/impl_model_for_ex04.dfy -- Implementation state machine for refinement proof in exercise04.

• chapter06-refine/exercises/spec_model_for_ex04.dfy -- Specification state machine for refinement proof in exercise04.

chapter07-async-clients

• chapter07-async-clients/exercises/exercise01.dfy
  KV Spec with Asynchronous Client Interface -- Modify the KV spec to encode asynchronous client requests.

chapter08-application-correspondence

• chapter08-application-correspondence/exercises/exercise01.dfy
  Application Correspondence with Synchronous Sharded KV Store -- How do we prevent a nonsense refinement theorem, for example one that does whatever it wants, but abstracts every protocol-level state to the initial spec state, so it can refine to a bunch of stutter steps?

final-project

• final-project/exercises/exercise01.dfy
  Final Project -- Design a Sharded Hash Table (SHT) protocol and prove it is correct.

midterm-project

• midterm-project/exercises/distributed_system.s.dfy
  DistributedSystem -- DO NOT EDIT THIS FILE! It's a trusted file that specifies how hosts interact with one another over the network.

• midterm-project/exercises/exercise01.dfy
  Midterm Project -- Build a distributed lock server. Define how a host implements your protocol in host.i; write your safety spec and proof here.

• midterm-project/exercises/host.i.dfy
  Host protocol -- Define the host state machine here: message type, state machine for executing one host's part of the protocol.

• midterm-project/exercises/network.s.dfy
  Network -- DO NOT EDIT THIS FILE! It's a trusted file that specifies how the network delivers packets, allowing reorder and duplicate delivery.