SE212 - Program Correctness

• State - Values of the variables at a particular time in the execution of the program
• Postcondition - Well formulated formula about values of program variables in the state after the program has completed
• Program correctness we prove the arguments in form of:

assert(P);
C;
assert(Q);

• P is the precondition
• C is the program
• Q is the postcondition
• assert in SE212 are not executable program statements and do not affect the behavior of the program
• |= par implies partial correctness
  • C does not always have to terminate in partial correctness
  • But when it does terminate it ends in satisfying state (Q) assuming it started at satisfying state (P)
• |= tot implies total correctness
  • Total Correctness = Partial Correctness + Termination
• History variables - Variables that do not appear in the program
• assert(P [E/Var]); Var := E; assert(P);
  • Var is a variable
  • E is an expression
  • P[E/Var] is a substitution
• Loop Invariant - Assertion that the program state satisfies before and after each execution of the body of a loop