# Final Exam Coverage

## Logistics

• Apr 29, 8AM-10AM, SB 111
• You are permitted 2 letter-sized, double-sided pages of notes to use on the exam (no sharing notes)
• No electronics!
• The exam will NOT be cumulative!
• The exam will be ~30-40% objective (MC), and 60-70% written problems.

## Topics

1. Semantics

• Basic definitions: what is it? why do we care?
• Math
• ematical rigor!
• Primary approaches:
• Operational {big-step, small-step}
• Denotational (but we didn’t cover this one)
• Axiomatic
• Rules of inference
• Terms: premises, side-conditions, conclusion, axioms, etc.
• Proof trees & Derivation strategies
2. Grammars

• Why do we have them?
• Formal specification of valid syntactic objects (for later semantic analysis)
• Chomsky hierarchy
• Regular, Context-free, Context-sensitive grammars/languages
• Backus-Naur Form (BNF) -- used for specifying grammars
• IMP language (described in BNF)
3. Big-step Semantics

• e ⇓ v : e evaluates to v (in one big step)
• ⇓ is a relation over syntactic objects, environments, and possible results
• Equivalence to eval function (interpreter)
• Big-step rules for IMP
• Proof trees concerning IMP programs using ⇓
• Concerning the result of evaluating expressions/statements
• Concerning the equivalence of different programs
• Why is this important?
4. λ Calculus

• Syntax & Semantics
• Study precedence rules
• e.g., “λx.x λz.y z” fully parenthesized is  “λx.(x (λz.(y z)))”
• Free variables & Variable capture
• ɑ-conversion, β-reduction, η-reduction
• Normal form
• Evaluation strategies: applicative-order vs. normal-order
• Equivalence to: eager/strict eval vs. lazy eval
• Equivalence to: call-by-value vs. call-by-name
• Data representation
• Booleans
• Church numerals
5. Axiomatic Semantics

• Hoare triples, e.g., {P} C {Q}
• Partial correctness
• Language of assertions
• IMP-language axiomatic semantic rules
• Rule of Consequence
• We can strengthen a valid Hoare triple’s preconditions and weaken its postconditions, and it will still hold
• Strong vs. Weak assertions (relative)
• Loop invariants used to prove the correctness/goal of loops

## Written Problems

1. Big-step Semantics

• Come up with rule(s) of inference to describe a new IMP language construct (similar to the for loop in the assignment)
• Come up with a proof tree for some ⇓ assertion
• I will provide all the IMP rules
2. λ Calculus

• Given λ-calculus expressions, draw ASTs, identify free/bound variables
• Given λ-calculus expressions, show reductions to get to normal form (or indicate that normal form is not reachable)
3. Axiomatic Semantics

• Given an IMP program, derive the weakest precondition (given a postcondition that holds)
• Come up with a loop invariant and loop goal for a looping program, and show that P → Q after the loop condition becomes false.