Table of ContentsPPT Slide Temporal Logic Problems With TL Temporal Logic of Actions Temporal Logic of Actions (2) Advantages of TLA Semantics Background for TLA (a.K.A, Hoare Proofs) Hoare Triples Specifying Progress Specifying Complete Programs Example System Specification Example (2): State Variables and Initialization Example (3): Allowed Actions N? Examples (4) Progress Condition L? Examples (5) Is That Enough? Invariants Examples (6) Invariants Examples (7) Sketch Proofs for These Claims: Summary ?????????????????¬????? |
Author: shawnh
Email: shawnh@cs.cmu.edu Home Page: http://www.cs.cmu.edu/afs/cs.cmu.edu/academic/class/15671-f97/www/index.html |