[ Course Documents ] : [ Semantics ]

Course Documents Next Keyword Index

Semantics

Handout:

PDF File (13pp., 492K)

Outline

• Static Semantics
• Dynamic Semantics
• Operational Semantics
  • Operational Semantics (cont.)
  • Operational Semantics Example
  • Evaluation of Operational Semantics
• Axiomatic Semantics
  • Weakest Preconditions
  • Program Proofs
  • An Axiom for Assignment
  • Some Inference Rules
  • A Rule for Loops
  • Loop Invariant Characteristics
    • More on Loop Invariants
    • Finding Loop Invariants
    • Finding Invariants (cont.)
    • Is I a Loop Invariant?
    • A Harder Loop Invariant Example
    • Using Loop Criterion 4
  • Evaluation of Axiomatic Semantics
• Denotational Semantics
  • Denotational vs. Operational
  • Denotational Specification Process
  • Program State
  • Example: Decimal Numbers
  • Expressions
  • Statement Basics
  • Assignment Statements
  • Sequence of Statements
    • Sequence of Statements (cont.)
    • Sequence of Statements (cont.)
    • Sequence of Statements (concl.)
  • Logical Pretest Loops
  • Logical Pretest Loops (cont.)
  • Evaluation of Denotational Semantics
• Summary