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.
• Counter Example.
• Abstract Queue.
• Rodin 3.2 Download.
• Rodin User Manual
• Rodin Handbook version 2.7 HTML and PDF. Also available PDF local copy.

• Assignment 3 on Refinement and Rodin.

  Rodin machines

  • Memory
  • Queue