## Program Construction and Verification |

### What people are saying - Write a review

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

### Contents

Preface | 9 |

THE PROPOSITIONAL CALCULUS | 14 |

THE PREDICATE CALCULUS | 53 |

Copyright | |

6 other sections not shown

### Common terms and phrases

a[fc algorithm alphabetic order and-E argument arithmetic array segment aſi aſij aſk assignment axiom Assume begin binary binary heap bubblesort cards Cartesian product chapter color(i compute conditional correctness conditional statements consequence rule consider cyclic codes defined degree(q(x denote Dijkstra disk elements equivalent example executed Exercises F F F F T F false formal gold casket guarantee termination heapsort idempotent Induction step inductive reasoning inscription integer invariant property knave length logical mathematical induction middle deck n+(n node number of occurrences odd(m odd(p odd(x path polynomial postcondition predicate prefix premise prevent evil problem proof rules propositional calculus prove range splitting remainder right decks rule of sequential rules of inference satisfying sequence sequential composition simplifies solution specification statement strong induction Superman Suppose termination condition true square truth table valid variables Variant verification conditions wb(S weakest precondition wo(S wp(S

### References to this book

Logic in Computer Science: Modelling and Reasoning about Systems Michael Huth,Mark Ryan No preview available - 2004 |

Algebraic Semantics of Imperative Programs Joseph A. Goguen,Joseph Goguen,Grant Malcolm Limited preview - 1996 |