lectures.alex.balgavy.eu

Lecture notes from university.
git clone git://git.alex.balgavy.eu/lectures.alex.balgavy.eu.git
Log | Files | Refs | Submodules

program-correctness.md (661B)

      1 +++
      2 title = 'Program correctness'
      3 +++
      4 ## Program correctness
      5 Prove that a program meets its specification.
      6 
      7 Correctness specification: formal description of how program is supposed to behave
      8 
      9 Program is correct: its executions satisfy the specification
     10 
     11 ### Verification - Hoare approach
     12 Prove statements of form `{precondition} program {postcondition}`
     13 - pre/postcondition are formulas
     14 - program is a while-program
     15 - we have proof rules for showing {φ} α {ψ}
     16 
     17 Partial correctness: if program starts satisfying φ, and if it halts, then when it halts ψ is satisfied
     18 
     19 Total correctness: partially correct, and terminates whenever started while satisfying φ