Decorated Programs

• Doing proofs in Hoare Logic can feel overly verbose
• Decorating programs is a way to informally write down a Hoare Logic proof
  • The idea is to insert assertions between every construct that makes the program. For example:

Decorated Programs: Skip and Assignment

Decorated Programs: Sequential Composition and While loops

Decorated Programs: Conditionals and Consequence rules

Example: A decorated program

Verify the following program by decorating it:

Invariants

• To reason about loops, we need to identify loop invariants, which might be difficult!
• For example, $\scriptsize j\ge 1$ is an invariant of the loop: $$\scriptsize i:=1;\,j:=1;\,\whileloop{i\lt n}{j:=j{+}i;\,i:=i{+}1}$$ but we cannot prove $$\scriptsize \ht{j\ge 1 \,\wedge\, i\lt n}{j:=j{+}i;\,i:=i{+}1}{j\ge 1}$$
• We need to strengthen the invariant: $\scriptsize j\ge 1 \,\wedge\, i\ge 1$

Forward Reasoning

• Suppose we initially know (or assume) that $w > 0$

// w > 0
x := 17;
// w > 0 and x = 17
y := 42;
// w > 0 and x = 17 and y = 42
z := w + x + y
// w > 0 and x = 17 and y = 42 and z > 59

• Then we can deduce a few facts about the resulting state (e.g. $z > 59$)

Backward Reasoning

• Suppose we want $z < 0$ at the end

// w + 17 + 42 < 0
x := 17;
// w + x + 42 < 0
y := 42;
// w + x + y < 0
z := w + x + y
// z < 0

• Then the initial state must satisfy $w < -59$

Side Note: Forward Assignment

• Note that the Assignment Axiom that we introduce works backwards: $$ \izero{Asgn}{\ht{\subst{Q}{x}{E}}{x:=E}{Q}} $$
• This naturally raises the question: how could we formulate a forward version of this axiom?

Side Note: Forward Assignment

• Based on our examples, perhaps the following can be used? $$ \izero{AgFw}{\ht{P}{x:=E}{P \,\wedge\, x=E}} $$
• Example: $\scriptsize\ht{w > 0}{x:=17}{w>0 \wedge x=17}$
• No! Example: $\scriptsize\ht{w > 0}{x:=x+1}{w>0 \wedge x=x+1}$

Side Note: Forward Assignment

• What about the following rule? $$ \izero{AgFw}{\ht{P}{x:=E}{\subst{P}{x}{E}}} $$
• No! Example: $\scriptsize\ht{x=0}{x:=1}{1=0}$
• It's easy to check that if we use $\subst{P}{E}{x}$, similar problems arise.

Side Note: Forward Assignment

• We can use the following rule, due to Floyd: $$ \izero{AgFw}{\ht{P}{x:=E}{\exists v \cdot x=\subst{E}{x}{v} \wedge \subst{P}{x}{v}}} $$
• Example: $\scriptsize\ht{x=0}{x:=1}{\exists v \cdot x=1 \wedge v=0}$
• Backward and forward rules are equivalent, but it is more difficult to use the forward rule (we have to find the variable $v$).

Side Note: Forward Assignment

• The previous discussion shows that it is easy to have wrong intuitions about the assignment axiom.
• This shows the importance of having a rigorous means of establishing the validity of axioms and rules.
• We can define a formal semantics for our language and then prove that the axioms and rules are sound.

Forward vs Backward Reasoning

• Forward Reasoning is more intuitive for most people
  • Helps in understanding what follows from initial assumptions
  • Useful for ensuring that an invariant is mantained
  • However, it might introduce irrelevant facts
• Backward Reasoning is usually more helpful
  • Helps in understanding what should happen
  • Crucial in Program Derivation!