EECS 755
Software Modeling and Analysis
Index
Blog
Final Exam
- Final
- Available: December 5 at 5:00
- Due: December 12 at 2:30
- Format: Download from class website, solution may be a LaTeX
generated PDF, an edited PDF, a text file, or a markdown file. Submit
via email to
palexand@ku.edu or Canvas.
- Download: here
- Source: here
-
Topics:
- Specification
- Inductive types
- Non-recursive definitions
- Fixedpoint definitions
- Theorems
- Type variables and polymorphisms
- Logic
- Proof tactics
intros - instantiating variables
induction and destruct - induction and case analysis
rewrite and apply - using equalities and properties
simpl and reflexivity - simplification and decision procedures
discriminate and injection - using constructed type values
split, right, and left - logic
- tacticals (
try, ;, etc. very basic)
- Inductive Definitions
- Defining relations
- Defining semantics
- Use in proofs
- Program Correctness
- Defining correctness properties
- Verification styles
- Defining language semantics
- Compiler Correctness
- Language abstract syntax
- Interpreters
- Correctness properties