Hoare Logic (cont'd(

12 Outubro 2022, 16:30 • Antónia Lopes

• Deductive Software Verification II
• Proof System (cont'd):
  • Soundness and Completeness 
  • Formal theory
    • Consistency (syntactically soundness)
    • Syntatic Completeness 
  • Examples of first-order theories
    • Theory of equality
    • Theory of Presburger arithmetic
    • Theory of Peano arithmetic
  • The syntatic incompleteness of arithmetic

• Hoare logic (cont'd):
• Proving termination
• Soundness and completeness
• Pros & Cons