Backward Refinement

These are lecture notes from my Computer Science course. For learning about formal specifications of systems, I recommend Software Abstractions: Logic, Language, and Analysis.

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.

This entry was posted in fss, lecture. Bookmark the permalink.