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
  • Non-recursive 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)