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’:
dictionaryis a specification and design
dictionary_as_a_pair_of_listsis the link between specification and design
I think the
hash_table_development code is related to this. It’s very confusing though.