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