Program Correctness
The goal of program correctness is to discover subtle bugs in a program and then prove that a program has the correct behaviour once all the bugs have been fixed.
But what is â€ścorrect behaviourâ€ť?

Correctness is a relative concept (i.e., relative to the specification).

Using proof rules for the constructs of a programming language, we prove that a program satisfies its specification.

Partial Correctness: Partial correctness means that the program fulfills its specification, or does not terminate (ex: infinite loop or recursion).
 Proof of partial correctness checks that the postcondition is true if the program terminates

Total Correctness = Partial Correctness + Termination
 Proof of total correctness shows that the loop terminates
The program below is partially correct, because it never terminates: (see Program Specification for syntax)
We use FloydHoare Logic for the Proof Theory to show Program Correctness.
Templates of Proofs
In program correctness proofs, we often work backwards from the postcondition.
 This is important, we need to start from the assertion that they give us. You cannot conjure up any assertions. Even saying assert(x +1 = x+ 1), you need to build on something from before, use
by implied using arith
orby implied using VC1
For example,
Reminder: We define $P[t/x]$ to be the formula obtained by replacing in $P$ every free occurrence of variable $x$ with $t$.
 The original expression $P$ CAN have the variable $t$, but there shouldnâ€™t be a Variable Capture (see note for example)
You have to be really careful, itâ€™s an assignment operator, so you cannot just do this (see Variable Capture):
One thing I got super confused about, and then I was doing the assignment, was like, do I need to replace everything? And the answer is no. For example:
 Basically, just think about it intuitively. You donâ€™t want to overwrite variables, which is why the conditions must be free. If you flip the assertions around, you would be overwriting the variable, so the assertion would no longer hold
 Also think of replacing
y := x
withx := y
, that would not work
 Also think of replacing
Review on Binary Relation.
We can make use of arrays in 2 ways:
 A reference to a value in an array (e.g., on RHS of an assignment or in a condition)
 You can use
by asn
 You can use
 Assignments to an element of an array (on LHS of an assignment)
 NEW, use
by array_asn
, see below
 NEW, use
You need to make use of the function rule. $(Râ‡’S)[a_{1}/x_{1},a_{2}/x_{2},â€¦,a_{n}/x_{n},f(a_{1},a_{2},â€¦,a_{n})/ret]$
Log_var_intro, this is something fairly new that I havenâ€™t seen too much, but it is worthwhile