Testing and Verification

I’d like to discuss some remarks regarding Chapter 7: Testing and Verification:


  1. After Remark 7.2.3, it is stated that
  • Failures do not inform us about the cause of the error (See Paragraph)
  • Unit tests help because they consider only one module and therefore make finding the bug’s cause easier.(See Paragraph)

However, error (aka bug) is defined as the cause of the failure. (See Error Def.) In the mentined quotes, error also seems as symptom. Otherwise, what should “cause of an error” mean?


  1. In Subsection 7.3.1: The Oracle Problem was mentioned that

In such cases, a typical specification is (true,true). Although it looks very weak, this specification at least requires that for being partially correct, the program must neither get stuck, nor abort, nor diverge which is sort of the minimum requirement for a properly functioning program.

Was it a typo since a partially correct program might diverges?


  1. In Example 7.3.9 a typo:
    test_linear covers the statements 1,11,12,13 but not 14.

  1. In 7.3.4 Fuzzing Just to prevent confusing, it might be better to say:

Furthermore, a very common thing is to use another (maybe simpler and maybe less efficient) implementation of a program A to fuzz test a more complicated implementation B of the same problem.


  1. In 7.4.1 Hoare Logic/Assignment_Rule, a typo:

So the Hoare triple ⊢{Q[e/x]}x=e;{Q} is true and our proof system has the first axiom.

As the axiom [Abort] was explained before [Assign], the quote implies that [Abort] was not an axiom.


  1. In Example 7.4.4, a typo:

looking back at Definition 7.4.3 we see that the precondition of the Hoare triple of an assignment is actually derived from the postcondition.

The Definition 7.4.3 is of Hoare triples for the block, Definition 7.4.1 for Assignment.


  1. In Example 7.4.7, some typos:

At the time, we count how many times we subtracted in q (not m). In the end, q is the quotient of x divided by y (not x) and x contains the remainder.


  1. In Proof of Theorem 7.4.11., I’m not sure whether it was a typo or I just didn’t understand it:

pc s Q is now defined such that e ∧ pc s Q = pc s1 Q and e ∧ pc s Q = pc s2 Q.

I think, it should be defined such that pc s Q = e ∧ pc s1 Q or pc s Q = ¬e ∧ pc s2 Q.

We have cause(failure)=error where failure=not (proper termination in a state satisfying Q).
We also have cause(error)=programming mistake.
programming mistake -> error -> failure
The failure tells us there was an error but not why there was an error (what is wrong with our program).

1 Like

Here it is meant, that parts of it are correct / fulfill certain aspects of correctness.
partially correct might be confusing with partial correctness. We will look to reformulate this paragraph.
Thank you.

Yes, you are right.
We will fix it.

Yes, [Abort] is also an axiom.

Thanks, we will fix it.

Thank you. We will fix it.

1 Like