Software Specification Exercises: Reasoning about Functions in Dafny

Software Specification, MEIC @ IST, 2019/20

jff

## Instructions - You can use the arrow keys, PgDown and PgUp to browse these exercises - You can use Escape to see an overview - You can use Ctrl+Click to zoom in

## Introduction The goal of this lab is to practice proving simple inductive properties of recursive functions. **First**, ensure that you have Dafny working in your PC. You can also run [Dafny online](https://rise4fun.com/Dafny), but the experience is not as good. *In these labs, I recommend you to use the IDE VS Code.*

### 0. Before you continue Start by revising the slides of [Lecture 7](07-dafny.html) and [Lecture 8](08-dafny.html). Make sure that you do all the exercises (if you haven't done so already).

1. Lists

Download the file Lab3_exercises.dfy and do the exercises listed in the file.

2. Reading activity

Read Dafny's tutorial on Collections. Experiment with all the examples.