Isabelle/UTP Tutorial

This website will contain the materials for my course on Isabelle/HOL and the UTP. I will be adding to this page over the coming weeks. Please also see the Isabelle/HOL website for more information. You can also download an Isabelle cheatsheet.

Session 1: Isabelle/HOL basics

Slides | Trees example | Dates exercise | Dates solution

Session 2: Deduction, Classes, Induction and Isar

Slides | Deduction exercise | Dates exercise 2

Session 3: UTP Values, Models and Predicates

Slides | Isabelle/UTP part 1

Session 4: Creating a Basic Model

Basic model example

Simon Foster, University of York