Isabelle/UTP tutorial
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