# EECS 755

## Software Requirements Modeling and Analysis

Index

Blog

# Midterm Exam

As you look through these topics, keep in mind that I do not care
about the specifics of Coq commands. For example, you neednâ€™t
remember that `induction`

performs induction, but you should remember
what induction does. Similarly for all other definition and proof
rules.

I will not ask you to do proofs. However, I may ask you to look at a
proof and describe what is happening or describe a theorem that should
be proved.

- Definition Techniques
- Defining abstract syntax with
`Inductive`

- Defining functions with
`Fixpoint`

- Defining functions/relations with inference rules
- Defining inductive propositions and relations

- Proof Techniques
- Induction and cases
- Applying theorems using
`apply`

and `eapply`

- Rewriting with theorems
- Generalizing an induction hypothesis (very basic)

- Interpreter Based Semantics
- Interpreting arithmetic expressions (Like the AE language)
- Interpreting sequential languages (Like the COM language)
- Defining interpreters over abstract syntax using
`Fixpoint`

- Defining transformations among semantics (compilers, optimizers)
- Verifying transformations (compilers, optimizers)