Final

Our final exam is a take-home exam posted May 12th at 2:00pm and due May 15th at 3:15pm. Topics as discussed in class will include:

Basic Language Definitions

• defining abstract syntax
• using inductive

defining computational evaluation

• defining values, terms and commands
• defining state and state transformation
• termination and non-termination

defining big-step evaluation relations

• defining inference rules
• inductive propositions using inductive
• including and transforming state
• defining evaluation relations for expressions
• defining evaluation relations for commands

defining small-step evaluation relations

• defining single step evaluation relations
• managing state
• defining multi-step evaluation relations
• values, stuckness, termination

program equivalence

• specifying behavioral equivalence
• optimization applications
• non-termination
• program equivalence as an equivalence

program assertions

• program state
• definition
• use and notations

Hoare triples

• specifying language constructs
• validity
• rule of consequence
• loop invariants

Language Properties

• determinism
• uniqueness
• stuckness and termination
• equivalence

Extending languages

• adding by extension
• new syntax and values
• extending the evaluation relation
• adding correctness properties