## A Method of Program Refinement |

### What people are saying - Write a review

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

### Contents

Predicative ProgrammingA Survey | 31 |

A ThreeValued Logic for Refinement | 55 |

A Method of Refinement | 69 |

Copyright | |

5 other sections not shown

### Common terms and phrases

A A B A D B a x y allows assume assumption chapter close this window complete conditional statement construct context current position cursor CursorCurrent(cursor delete denotes described dissertation EDIT operation error example expand the definition expression Fitzwilliam College function Generic-PC glyph glyph-at("line HOL theorem prover implementation initial and final initialisation introduce invariant ISAbs(l lemma line editor lineoi lineq(i+1 MacChar MacLength MacPos Marpos meaning monotonic function natural deduction nondeterministic nonterminating behaviour offset 3 length open a subwindow open a window PAINT(*line parent window partial model previous window program refinement programming language proof prove Pſ sp Qſsal recursive block refinement relation relational model requirements screen screenf('i screenOn SeeOurrent(offset semantics sequential composition simplify the focus skip sēl specification subexpression terminate three-valued logic three-valued predicates total model two-valued universal quantification variant View(screen window inference window rule window-inference interface