Restart learning math • Mathematical logic (6)

Personally I don't like model based correctness checking methods, they just check every possible states in a system in brute force, without generating any insight (eg. how each statement in a program helps it to reach the overall correctness) of the system or human readable/understandable proof of the correctness, which IMO is very disgraceful.

So I think a more reasonable way is using a proof based checking method, which the book explains in chapter 4.

Hoare triples

A Hoare triple is a triple of the form

$$ (|\phi|) P (|\psi|) $$

Which means in a state where $\phi$ holds, executing $P$ will lead to a state where $\psi$ holds.

For example, if the program $P$ calculate a number whose square is less than $x$, so when input is $x$ and output is $y$, we have

$$ (|x > 0|) P (|y\times y < x|) $$

So to prove the correctness of any program P, we need to assume a $\phi$ and get a $\psi$ with $P$ in some certain ways.

However, the possible result of P executing in $\phi$ is not just $\psi$ or $\neg\psi$, it's also possible that P never terminates (if you are using a turing complete language, it is totally possible to write a dead loop), so we can distinguish partial correctness, which just assume the program will eventually terminate, and complete correctness, which needs a proof of it.

Proof calculus for partial correctness

Rules

Ref figure 4.1 of the book.

Note in "Implied" rule "AR" means arithmetic¹.

Weakest Precondition

For each $\psi'$ after a $C$, we can get a $\psi$ before $C$, which can lead to $\psi'$ after $C$ by using one of the rules.

The only difficult rule to apply here is the "Partial-while" rule. Which needs part of $\psi'$ is a "loop invariant", which holds before each iteration of the loop starts and still holds after the whole loop.

Unfortunately, finding such a loop invariant is not easy, it needs "intelligence and ingenuity".

Proof calculus for total correctness

Proof calculus for total correctness is similar to partial correctness, we just need to add a proof to show the loops will eventually terminated, this is usually done by "identify an integer expression whose value can be shown to decrease every time we execute the body of the while-statement in question, but which is always non-negative".

However it is not always possible to find such a proof, for example, I believe Collatz program terminates, but human beings haven't found a way to show it terminates.

Programming by contract

Good methodology, not feasible in most commercial softwares nowadays.

Nowadays there do exists some languages that support programming by contract, like Dafny, but they are not widely used. It's understandable, because it costs too much effort to practice. Most software just want to hit the market fast and get quick responses rather than being correct at the first place.

It might be a serious problem for program verification, few programs can be "specified" before being written, and since requirements changes rapidly, it's hard to keep the specification, the requirements and the program in sync. And all the verification work is quiet hard and requires "intelligence and ingenuity", a verification checker is sometimes annoying², even if it is, in most of times, correct.

Honestly, though I love the idea of programming by contract (and I always add as much asserts I can in my programs), I have to admit it's not a good idea for nowadays software industry, which develops in a crazy speed. We just pile up shitty code to satisfied the customer. Correctness is not the most important thing here, but profitable is.

Personally I think a gradual way of introducing verification into industrial languages might be a feasible approach. We can provide tools in language to enable the programmer to proof only the core logic of a program, and maybe with several "sorry" or "trustMe" for complex details.