Final Exam Coverage
Logistics
 Apr 29, 8AM10AM, SB 111
 You are permitted 2 lettersized, doublesided pages of notes to use on the exam (no sharing notes)
 No electronics!
 The exam will NOT be cumulative!
 The exam will be ~3040% objective (MC), and 6070% written problems.
Topics

Semantics
 Basic definitions: what is it? why do we care?
 Primary approaches:
 Operational {bigstep, smallstep}
 Denotational (but we didn’t cover this one)
 Axiomatic
 Rules of inference
 Terms: premises, sideconditions, conclusion, axioms, etc.
 Proof trees & Derivation strategies

Grammars
 Why do we have them?
 Formal specification of valid syntactic objects (for later semantic analysis)
 Chomsky hierarchy
 Regular, Contextfree, Contextsensitive grammars/languages
 BackusNaur Form (BNF)  used for specifying grammars
 IMP language (described in BNF)

Bigstep 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)
 Bigstep rules for IMP
 Proof trees concerning IMP programs using ⇓
 Concerning the result of evaluating expressions/statements
 Concerning the equivalence of different programs

λ Calculus
 Syntax & Semantics
 Study precedence rules
 e.g., “λx.x λz.y z” fully parenthesized is
“λx.(x (λz.(y z)))”
 ASTs (draw and read)
 Free variables & Variable capture
 ɑconversion, βreduction, ηreduction
 Normal form
 Evaluation strategies: applicativeorder vs. normalorder
 Equivalence to: eager/strict eval vs. lazy eval
 Equivalence to: callbyvalue vs. callbyname
 Data representation

Axiomatic Semantics
 Hoare triples, e.g., {P} C {Q}
 Language of assertions
 IMPlanguage 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

Bigstep 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

λ 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)

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.