EECS 755
Software Modeling and Analysis
Index
Blog
Final Exam
 Final
 Available: May 6 at 2:30
 Due: May 9 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: Final 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
inversion
and subst
(basics)
 tacticals (
try
, ;
, etc)
 Inductive Propositions
 Defining properties
 Defining relations
 Use in proofs
 Program Equivalence
 Defining equivalence properties
 Verification styles
 Defining language semantics
 Hoare Logic
 Program State
 Assertions
 Hoare Triples
 Hoare Logic (very basic)