## A Method of Program Refinement |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Window Inference | 11 |

Predicative ProgrammingA Survey | 31 |

A ThreeValued Logic for Refinement | 55 |

Copyright | |

6 other sections not shown

### Common terms and phrases

abort array assume assumption but_last(fst chapter char2glyph lineQ("i close this window complete conditional statement construct context current position cursor delete denotes described dissertation EDIT operation error example expand the definition expression following window function Generic-PC glyph glyph-at line GoodScreen(screen imperative programming language implementation initial and final initialisation interpretation introduce IsAbs(l labelled block lemma length line editor line'Qi lineQ(i MaxChar MaxLength MaxPos meaning MinMove("offset monotonic function natural deduction nondeterministic nonterminating behaviour offset open a subwindow open a window parent window partial model previous window program refinement program variables programming language proof prove recursive block recursive call refinement method refinement relation relational model requirements result screen screen'Qn semantics sequential composition simplify the focus skip subexpression theorem prover three-valued logic three-valued predicates tool total model transformational reasoning two-valued UneQi universal quantification variant verification window and return window inference system window rule window-inference interface