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

- After Remark 7.2.3, it is stated that

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?

- 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 divergewhich is sort of the minimum requirement for a properly functioning program.

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

- In Example 7.3.9 a typo:

`test_linear`

covers the statements 1,11,12,13 but not 14.

- 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 Bof the same problem.

- 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

firstaxiom.

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

- 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

derivedfrom the postcondition.

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

- In Example 7.4.7, some typos:

At the time, we count how many times we subtracted in

q(notm). In the end, q is the quotient of x divided byy(notx) and x contains the remainder.

- 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`

.