## Completeness and incompleteness theorems for Hoare-like axiom systems |

### What people are saying - Write a review

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

### Contents

A FixedPoint Characterization of Partial | 7 |

Expressihility Soundness and Completeness | 52 |

Chapter k NonRegular Control Structues | 72 |

2 other sections not shown

### Common terms and phrases

A2 Q algorithm assertion language assignment statement assume axioms Rl BA(P C. A. R. Hoare complete axiom complete proof system conditional statement coroutines deBakker and Meertens deducible defined definition of partial Dijkstra's end V}/D fixed point theorem follows free variables function fundamental invariance theorem FX(P FX(w GCS's given global variables Gorelick G075 greatest fixed point halting problem Hence Hoare-like axiom systems Ifree(V least fixed point M[begin non-active variables non-regular partial correctness PL[L point of G post condition predicate transformer fixed proc x:p procedure call procedure declarations procedure parameters procedures with procedure program identifier proof of soundness Proposition provable recursive procedures regular system rule of inference RX(Q Semantics sound and complete soundness of axiom ST x P(S stack static scope system of procedure total correctness transformer fixed point true iff weakest precondition wQ A P(wQ