What people are saying - Write a review
We haven't found any reviews in the usual places.
A FixedPoint Characterization of Partial
Expressihility Soundness and Completeness
Chapter k NonRegular Control Structues
2 other sections not shown
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