EECS 755
Software Modeling and Analysis
Index
Blog
Midterm Exam
 Midterm
 Available: March 28 at 2:30
 Due: March 29 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.
 Dowload: Midterm Exam
 Source: LaTeX

Topics:
 Specification
 Inductive types
 Nonrecursive definitions
 Fixpoint definitions
 Theorems
 Type variables and polymorphisms
 Logic
 Constructive specification
 Defining constructors
 Defining properties over constructors
 Defining correctness theorems
 Proof tactics
intros
 instaintiating 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