Refinement and Rodin

• Slides on ADTs and refinement.
• Paper by Hoare et al, Data Refinement Refined, Oxford Univ Technical Report, 1985.
• Slides on Rodin and refinement.
• Rodin 3.9 Download.
• Rodin User Manual
• Rodin Handbook version 2.8 HTML and PDF. Also available PDF local copy.

• Rodin machines done in class
  • Two Byte Counter
  • Queue

• Assignment 3 on Refinement and Rodin. Due on Fri 6th Mar 2026.
  Partial Rodin machine: Virtual Memory.