Temporal Logic of Programs |
Contents
Introduction | 1 |
The Formal System | 45 |
Additional Propositional Variables | 51 |
Copyright | |
7 other sections not shown
Other editions - View all
Common terms and phrases
a₁ a₂ applying assumption atnext atomic formulas await B₁ B₂ Bo→mn classical logic coend computation contain Deduction Theorem definition denoted Derivation entry execution sequence expressed finite first-order first-order logic formal system formulas of F hence holds indatnext induction hypothesis induction principle infinite intermittent assertion invof K₁ Kröger L₁ L₂ language Lemma Let F logical laws loop invariant Manna and Pnueli mn=nr modal logic nr=ls O(at P-formula parallel component partial correctness precedence properties premises previous section program axioms Program Example program verification proof rules prop propositional logic propositional variables prove semantics sequential program set of formulas set of labels smallest k>i Soundness Theorem ẞ₁ ẞo statement sequence t₁ taut temporal logic temporal operators temporal structure Tense logic trans trivial true verification well-founded ordering α₁ α₂