Backward refinement has the same goals as forward refinement, and is set up the same. However it has a different set of rules, but the same set of cases (preconditions must correspond etc.). Apparently the rules are ‘much uglier’.

It’s a bit like how it sounds, the rules describe the relation concrete to abstract. For example in forward refinement every abstract initial state needed a concrete initial state, but the reverse doesn’t apply – a concrete initial state doesn’t need to relate to an abstract initial state.

There’s an example broken into three different pieces in ‘RefinementExample’:

• dictionary is a specification and design
• dictionary_as_a_pair_of_lists is the link between specification and design

Stepwise Refinement

I think the hash_table_development code is related to this. It’s very confusing though.