Dev.to

Software Testing: Theory and Practice (Part 2) - Software Testing and Logical Expressions

Part 1 is here. Key Takeaways for This Article The conditions we need to check when testing functional programs can be expressed as logical formulae. Make it a habit to think about specifications and software tests in terms of logical expressions. Recap of Functional Program Testing from Part 1 In this second installment we re-explain Part 1 from a different angle, so let’s quickly review: A functional program’s specification can be described as a table mapping some inputs to outputs, and the implementation’s meaning as a table mapping all inputs to outputs. If, for every input listed in the specification, the output matches the implementation’s table, then the implementation satisfies the specification. These explanations are in fact natural-language translations of concepts originally described as logical formulae in computer-science literature. The goal of Part 2 is to let you understand those original formulae. Trying to explain logical notation without motivation can feel unsatisfying, so let’s first see why it is worth using. Why Logical Expressions? Behind specifications, implementations, semantics and software tests lies an important concept: verification of correctness. In the sources we introduced, the core of verification is always described with logical formulae. Why did the authors choose formulae instead of plain language? There are two reasons: Natural language is ambiguous; one description may admit multiple interpretations. Logical notation makes it much easier to check the validity of an argument. Consider the ambiguous sentence “I saw the man with the telescope.” — who has the telescope? When explanations allow multiple readings, different people may derive different conclusions. To avoid such tragedies we should use a language whose meaning is as precise as possible, and logical notation is a well-known candidate. Of course formulae cannot eliminate every misunderstanding: a reader may misread symbols, or fail to map them to real-world concepts. Nevertheless, they cause far fewer misinterpretations than plain language. The field that studies logical expressions is symbolic logic. Its literature covers both the meaning of formulae and formal proofs built from them — which brings us to the second advantage. With logical proofs, if you can start from known formulae and reach your claim by following the prescribed rules, your claim is proven correct. In short, plain language is ambiguous and makes validity hard to check. For critical core ideas that we do not want misread, authors use logical expressions. Both Part 1 and Part 2 of this series are examples of that approach. For each step we: Formulate an explanation as a logical expression that reduces the gap to traditional software-testing concepts. Verify that this expression follows from the literature’s formulae by a valid proof. Translate the expression into natural language. Step 2 lets the author confirm the translation’s correctness precisely 1 — a task that would be much harder had step 1 not been written as formulae. Because natural-language premises can be interpreted in multiple ways, judging the soundness of an argument written in plain text is hard. If both premises and conclusion are formulae, you only need to check that the premises hold and the proof follows the rules to be confident in the conclusion. Sidebar: Specifications as Logical Formulae Naturally, precise logical expressions can describe program specifications themselves. If implementer and verifier interpret a spec differently, they are effectively working on different programs. Successful testing then becomes unlikely, leading to re-work, extra costs and delays. Specification notation must fit the system’s domain. Different notations carry different overheads and mitigate re-work to different degrees. For domains where errors after deployment are extremely costly (aerospace, medical, rail, finance), formal logic or specialised spec languages are often worth the effort. For a small e-commerce site or a game, that cost may be overkill. Meaning of Logical Expressions Now that we know why we use formulae, let’s learn just enough notation to follow Part 2. A comprehensive treatment would fill a textbook, so we’ll cover only what we need. What Is a Logical Expression? A logical expression (or formula) is a string of symbols conforming to a fixed grammar. Examples: P ∧ Q, ∃x. ∀y. (R x y) 2. Below we introduce just the constructs needed to understand testing-related formulae. For deeper study, see an introductory logic text. Building Blocks Conjunction (logical AND) P ∧ Q (“P and Q”) is true iff both P and Q are true. Table 1: Truth table for conjunction Left Right Result T T T T F F F T F F F F Programmers can think of && / and. Implication P ⟶ Q (“if P then Q”) is false only when P is true and Q is false; otherwise true

Apr 24, 2025 - 01:42

Software Testing: Theory and Practice (Part 2) - Software Testing and Logical Expressions

Part 1 is here.

Key Takeaways for This Article

The conditions we need to check when testing functional programs can be expressed as logical formulae.
Make it a habit to think about specifications and software tests in terms of logical expressions.

Recap of Functional Program Testing from Part 1

In this second installment we re-explain Part 1 from a different angle, so let’s quickly review:

A functional program’s specification can be described as a table mapping some inputs to outputs, and the implementation’s meaning as a table mapping all inputs to outputs.
If, for every input listed in the specification, the output matches the implementation’s table, then the implementation satisfies the specification.

These explanations are in fact natural-language translations of concepts originally described as logical formulae in computer-science literature.

The goal of Part 2 is to let you understand those original formulae.

Trying to explain logical notation without motivation can feel unsatisfying, so let’s first see why it is worth using.

Why Logical Expressions?

Behind specifications, implementations, semantics and software tests lies an important concept: verification of correctness.

In the sources we introduced, the core of verification is always described with logical formulae.

Why did the authors choose formulae instead of plain language?

There are two reasons:

Natural language is ambiguous; one description may admit multiple interpretations.
Logical notation makes it much easier to check the validity of an argument.

Consider the ambiguous sentence “I saw the man with the telescope.” — who has the telescope?

When explanations allow multiple readings, different people may derive different conclusions.

To avoid such tragedies we should use a language whose meaning is as precise as possible, and logical notation is a well-known candidate.

Of course formulae cannot eliminate every misunderstanding: a reader may misread symbols, or fail to map them to real-world concepts. Nevertheless, they cause far fewer misinterpretations than plain language.

The field that studies logical expressions is symbolic logic. Its literature covers both the meaning of formulae and formal proofs built from them — which brings us to the second advantage.

With logical proofs, if you can start from known formulae and reach your claim by following the prescribed rules, your claim is proven correct.

In short, plain language is ambiguous and makes validity hard to check. For critical core ideas that we do not want misread, authors use logical expressions.

Both Part 1 and Part 2 of this series are examples of that approach. For each step we:

Formulate an explanation as a logical expression that reduces the gap to traditional software-testing concepts.
Verify that this expression follows from the literature’s formulae by a valid proof.
Translate the expression into natural language.

Step 2 lets the author confirm the translation’s correctness precisely ¹ — a task that would be much harder had step 1 not been written as formulae.

Because natural-language premises can be interpreted in multiple ways, judging the soundness of an argument written in plain text is hard. If both premises and conclusion are formulae, you only need to check that the premises hold and the proof follows the rules to be confident in the conclusion.

Sidebar: Specifications as Logical Formulae

Naturally, precise logical expressions can describe program specifications themselves.

If implementer and verifier interpret a spec differently, they are effectively working on different programs. Successful testing then becomes unlikely, leading to re-work, extra costs and delays.

Specification notation must fit the system’s domain. Different notations carry different overheads and mitigate re-work to different degrees.

For domains where errors after deployment are extremely costly (aerospace, medical, rail, finance), formal logic or specialised spec languages are often worth the effort. For a small e-commerce site or a game, that cost may be overkill.

Meaning of Logical Expressions

Now that we know why we use formulae, let’s learn just enough notation to follow Part 2. A comprehensive treatment would fill a textbook, so we’ll cover only what we need.

What Is a Logical Expression?

A logical expression (or formula) is a string of symbols conforming to a fixed grammar.

Examples: P ∧ Q, ∃x. ∀y. (R x y) ².

Below we introduce just the constructs needed to understand testing-related formulae. For deeper study, see an introductory logic text.

Building Blocks

Conjunction (logical AND)

P ∧ Q (“P and Q”) is true iff both P and Q are true.

Table 1: Truth table for conjunction

Left	Right	Result
T	T	T
T	F	F
F	T	F
F	F	F

Programmers can think of && / and.

Implication

P ⟶ Q (“if P then Q”) is false only when P is true and Q is false; otherwise true ³.

Table 2: Truth table for implication

Left	Right	Result
T	T	T
T	F	F
F	T	T
F	F	T

A chain P ⟶ Q ⟶ R parses as P ⟶ (Q ⟶ R); everything but the rightmost is premise, the last is conclusion.

Predicate

A predicate returns a truth value. P x denotes P applied to x.

E.g. white x is true iff x is white.

Existential quantifier `∃`

∃x. (P x) (“there exists an x such that P x”) is true iff some x makes P x true ⁴.

For instance, ∃x. white_crow x is true because white crows exist.

Universal quantifier `∀`

∀x. (P x) (“for all x, P x”) is true iff P x is true for every x ⁴.

∀x. (crow x ⟶ black x) is false because there are white crows.

Combining ∀ with implication narrows the domain:

∀x. ((crow x) ⟶ (black x)) reads “for all x that are crows, x is black.”

A chain ∀x. ((P x) ⟶ (Q x) ⟶ (R x)) means: for every x, if all premises hold, then R x holds.

That concludes our crash course. We are ready to express testing concepts as formulae!

Logical Formulae for Software-Testing Concepts

An essential notion behind testing is total correctness.

Software testing can be viewed as sampling inputs to find cases where total correctness is false (defects). Part 1 explained specification/implementation in those terms.

Here we use formulae to define total correctness (and its components). We assume functional programs (one deterministic output per input).

What Is Total Correctness?

A program is totally correct iff it both terminates and returns an output listed in the spec for every input that the spec declares valid.

Thus total correctness = termination + partial correctness.

Termination: the program never loops forever on any valid input.

Partial correctness: assuming it does terminate, the output matches the spec.

To state this precisely we introduce:

Pre-condition pre i: whether input i appears in the spec’s table.
Post-condition post i o: whether the pair (i,o) appears in that table.

The Denotation Function

The denotation function denote prog i returns the output of program prog on input i if it terminates; otherwise undefined. Thus denote is a partial function.

With this we can state total correctness precisely.

Formula for Total Correctness

TC pre post prog (“Total Correctness”) means:

For every input satisfying pre, executing prog terminates and the result satisfies post.

Define:

TC pre post prog ≡ (T pre prog) ∧ (PC pre post prog)

where T is termination, PC partial correctness.

Termination Predicate `T`

T pre prog ≡ ∀i. (pre i ⟶ ∃o. (denote prog i = o))

True iff for every valid input i there exists some output o (i.e. prog terminates).

Partial Correctness Predicate `PC`

PC pre post prog ≡ ∀i. ∀o. (pre i ⟶ (denote prog i = o) ⟶ post i o)

True iff for every valid input i, if prog terminates with o, then post i o holds.

Both predicates together yield total correctness.

Translating to Testing

A defect is an input that makes total-correctness false, i.e. violates termination or partial correctness.

Testing samples finite inputs I₁,…,Iₙ approximating the universal quantifiers. For termination:

(pre I₁ ⟶ ∃o. denote prog I₁ = o) ∧
(pre I₂ ⟶ ∃o. denote prog I₂ = o) ∧ … ∧
(pre Iₙ ⟶ ∃o. denote prog Iₙ = o)

Similarly for partial correctness with expected outputs O₁,…,Oₙ.

A good test suite approximates the true quantified formula well with few cases.

Conclusion

By reading these formulae we gain a sharper understanding of software testing, and we can construct convincing formal arguments about correctness.

Here, “confirm” means checking that replacing the literature’s definitions with those used in this series causes no problems; i.e. that the two versions of total correctness are equivalent for the same program and specification (pair of pre- and post-conditions). The book Semantics with Applications defines correctness using operational semantics (fixing an evaluation order), whereas Part 1 did so with denotational semantics (viewing programs as mathematical functions). ↩
Notation follows Isabelle syntax: https://isabelle.in.tum.de. ↩
Some texts write ⇒ instead of ⟶. ↩
Parentheses are redundant; we keep them for readability. ↩