James Course - Hoare Logic

Question 1

What it means for a program to be wrong?

Answer 1

A program is wrong if the reasoning for why it should be correct is flawed.

Question 2

When we talk about programs, we speak at one of three levels. What are these three levels?

Answer 2

Level 1: Runtime. The runtime level deals with specific values and a specific environment from a single execution of the program. A lot of debugging is done at Level 1.

Level 2: Code. At the level of code, we think about what the current implementation could do when given arbitrary inputs and an arbitrary environment. Behaviors that cannot happen are not considered, even if it requires global reasoning to rule them out. A lot of implementation work is done at Level 2.

Level 3: Design/Logic: At the level of logic, we consider the abstract specification of each unit of a program. When using other units, we only consider the guarantees made by the spec, and assume they may be replaced at any time with a different implementation. Many programs which are correct when viewed at Level 2 are not correct when viewed at Level 3, because they rely on behavior which is not guaranteed to hold in all future versions. Most software design is done at Level 3.

Question 3

Isn’t our goal to deliver working software to customers, and so Level 2 correctness is all that’s important?

Answer 3

No, our goal is to be able to continue to deliver working software far into the future. Level 3 is all about how modular are the interactions between the components of your software, and that’s important if you care at all about having different versions of those components, like, say, if you wanted to rewrite one of them tomorrow.

Question 4

What is the lesson we can learn from the SimCity use after free error?

Answer 4

This is why it’s important to make your APIs conform as strictly to the spec as possible, at least in Debug mode.
This all could have been avoided if DOS’s free were to deliberately zero-out the memory.
Hyrum’s Law

Question 5

Reminder: The most important parts of our craft deal not with code, but with the logic underneath

Answer 5

Software Design only exists at the level of logic.

Question 6

List Level 2 elements

Answer 6

The object of study of Level 2 is the code. Any statement that can be phrased in terms of the code, but not a specific trace or state, is a Level 2 statement.

The corresponding manner of reasoning is first-order logic. This means we can write down formulas that say “for all inputs X, does this property hold?” or “does there exist an input Y, such that this function crashes?” What we can’t do is quantify over other functions.

Question 7

List Level 3 elements

Answer 7

The object of study of Level 3 is the specification. There are many, many ways of writing specifications, but a popular one is the Hoare triple: preconditions and postconditions.

At Level 3, we can ask questions about all possible implementations of malloc, like “does this program have a memory error?”

The corresponding manner of reasoning is higher-order logic. Higher-order logic is like first-order logic, but we can now quantify over functions.

Question 8

Can you retrieve design information from the code?

Answer 8

The information of a program’s design is largely not present in its code. There are many designs that correspond to the exact same code, and so recovering all the design information is actually impossible.

Question 9

Why self documenting code is not possible?

Answer 9

Because the information of a program’s design is largely not present in its code. There are many designs that correspond to the exact same code.

Question 10

Why TDD is not a substitute for design?

Answer 10

Test too much and be too specific. Is it part of the design that postProfileUpdateToServer must call appState.saveCurrentState twice, and it chooses to do so once by calling logger.logUpdateEvent?

The code should not follow the tests, nor the tests the code. They should both follow the design.

Question 11

Why TDD is not a substitute for design?

Answer 11

Test too much and be too specific. Is it part of the design that postProfileUpdateToServer must call appState.saveCurrentState twice, and it chooses to do so once by calling logger.logUpdateEvent?

The code should not follow the tests, nor the tests the code. They should both follow the design.

Question 12

What is the purpose of a documentation?

Answer 12

The purpose of documentation is not just to describe how the system works today, but also how it will work in the future and across many versions

Question 13

What are the benefits of a spec in Joel eyes?

Answer 13

When you design your product in a human language, it only takes a few minutes to try thinking about several possibilities, revising, and improving your design.

Giant reason number two is to save time communicating. When you write a spec, you only have to communicate how the program is supposed to work once. Everybody on the team can just read the spec.

Question 14

What does “code knowledge” means

Answer 14

Code A knows about code B when B is referenced in the proof of correctness of A.

Question 15

What smell do you identify when you search for some behavior very deep in the code?

Answer 15

When you have to read a ton of things to make sure a thing can happen or not you are probably searching for unstable guarantees, that is, implementation guarantees, instead of design guarantees. You shouldn’t have to dig deep, use the specification.

Question 16

What new way of thinking about function calling Level 3 give us?

Answer 16

Don’t think about one function calling another. Think about one function calling all future versions of that function.

Question 17

What are assertions in Hoare Logic?

Answer 17

Logical facts that must be true at a certain point in the program. We typically write assertions in curly braces.

Question 18

How Hoare triples can reflect complexity in a program?

Answer 18

Even though each line is simple, the assertions grow in complexity, reflecting how the current state of the program grows in complexity.

Question 19

How Hoare tiples show when we can forget something?

Answer 19

{true}
x  =  1 0 ;
{x>1}
y  =  4 2 ;
{x>1 ,   y>1}
z  =  x  +  y ;
{z>1}

we can “forget” about x and y, and about the exact value of z.

Question 20

How many pieces are necessary in a Hoare triple?

Answer 20

We only need two, the third can be inferred.
Given a statement and a precondition we can find the strongest postcondition.
Given a statement and a postcondition we can find the weakest precondition.
So, for a given precondition, there is a canonical postcondition, and vice versa.
We can also mechanically transform the precondition and postcondition into code.

Question 21

A Hoare triple is composed of:

Answer 21

precondition, command, and postcondition
{P}S{Q}
A Hoare triple {P} S {Q} should be read “if P is true, then, after S executes, Q will be true”.

Question 22

What are inference rules?

Answer 22

An inference rule says what premises we need to deduce something.
If the premises of the rule hold, then one can deduce
that the conclusions hold.

Question 23

What is a derivation tree?

Answer 23

Is a sequence of applications of inference rules in a tree layout. The derivation tree is a proof for that program.

Question 24

What is the inference rule for assignment?

Answer 24

————————– assign

{[E/x]P} x := E {P}

Question 25

What is the sequence inference rule?

Answer 25

{P} S {Q} {Q} T {R}
—————————- sequence
{P} S ; T {R}

This inference rule show us how to append/sequence programs.

Question 26

What is the consequence inference rule?

Answer 26

P′ ⇒ P {P} S {Q} Q ⇒ Q′
————————————- consequence
{P′} S {Q′}

Consequence rule show to us how to strenghten preconditions or how to weaken postconditions.

When we express Hoare logic as assertions between each line of a program, the consequence rule lets us modify an assertion using purely logical reasoning,
without any intervening code.

Question 27

When a program has modularity?

Answer 27

Suppose a program consists of two subprograms, A followed by B. If the strongest postcondition of A is stronger than the weakest precondition of B, the program has modularity, because it is possible to change A without changing B.

Question 28

What is the while inference rule?

Answer 28

{P ∧ B} S {P}
————————————– while
{P} while B do S {¬B ∧ P}

P is the loop invariant

Question 29

What is the if inference rule?

Answer 29

{P} S {R} {Q} T {R}
———————————————————— if
{(B⇒P) ∧ (¬B⇒Q)} if B then S else T {R}

Note that the if rule doubles the size of the precondition, so that a chain of them can cause exponential blowup in complexity. This corresponds to how a chain of if statements can have exponentially many paths. Being able to forget which path was taken using the consequence rule is paramount to making programs with conditionals tractable to reason about.