Structured Programming, Hoare Logic, etc.

Structured Programming

In a generic imperative programming language, structured programming restricts the allowed statements to three things:

• Sequences of statements
• A while-loop
• An If-statement

Although not explicitly included, functions/routines are included as allowable statements.

It can be extended to include an If-else statement. We get for-loops and a switch statement as syntactic sugar.

We also have a number of possible commands (assign a value to a variable, function calls, etc.)

• Steve Jost's Structured Programming, IT 236 notes
• C2 Wiki Page

Hoare Logic

We can formally prove the correctness of a structured program using Hoare logic. (This can be enforced using contracts.)

• Kasper Svendsen's Slides on Hoare Logic and Model Checking, Cambridge
• C2 Wiki Page on Hoare Triples

Separation Logic

When we include pointers, allocating memory, and freeing memory into the Hoare logic, we get separation logic.

Though this is only one approach to modify Hoare logic to incorporate heap memory.

• Separation Logic

Garbage Collection

A huge open research problem is to formally prove the correctness of a garbage collector using Hoare logic (or more precisely, some generalization of Hoare logic).

• Tyler Hannan, Chester Holtz, Jonathan Liao, "Comparative Analysis of Classic Garbage-Collection Algorithms for a Lisp-like Language". arXiv:1505.00017, 13 pages
• Knuth, Art of Computer Programming, vol 1, section 2.3.5 and section 2.5
• C2 Wiki page