Atomic propositions and equivalence classes offer a practical solution for making testing manageable when dealing with large or infinite input domains. While these concepts are widely used in formal verification—such as in Exhaustive Model-Based Equivalence Class Testing by W. Huang and J. Peleska, 2013, from which we’ll borrow the formal definition of equivalence classes—they are extremely useful in everyday testing tasks.
In this two-part post, we explore how atomic propositions and equivalence classes help us select “representative values” when input spaces are large. These representative values group inputs that behave equivalently, enabling thorough system testing without needing to cover every possible input within each group. Given that atomic propositions and equivalence classes are commonly used in formal verification, we also delve into the formal mathematical notation that defines these concepts.
Let’s start by defining what atomic propositions are, how they relate to equivalence classes, and why they always go hand-in-hand.
Atomic propositions and equivalence classes
Atomic propositions and equivalence classes are closely related concepts. Atomic propositions are logical statements that evaluate to either true or false based on the current state of the system. Equivalence classes, on the other hand, are partitions of the input space where all inputs in the same class are expected to produce the same system behavior.
Atomic propositions
“Atomic propositions are logical statements that evaluate to either true or false, based on the current state of the system.”
Each atomic proposition describes a condition on the system’s variables, which make up the state of the system, such as a specific range or threshold. For example, in an industrial heating system, an atomic proposition could define a condition where a temperature value is greater than 100°C. Such atomic propositions are used to define equivalence classes: inputs that make the proposition true belong to one class, while inputs that make the proposition false belong to another.
For instance, if we have an atomic proposition like:
Then, the corresponding equivalence classes are:
- Class 1: Inputs where is true (temperature is greater than 100°C).
- Class 2: Inputs where is false (temperature is less than or equal to 100°C).
By using multiple atomic propositions, we can create a more granular partition of the input space. For example, consider the atomic propositions:
These atomic propositions define four equivalence classes:
- Class 1: is true and is true
- Class 2: is true and is false
- Class 3: is false and is true
- Class 4: is false and is false
Each equivalence class represents a distinct combination of true/false values for the atomic propositions, effectively reducing the input space to a set of classes where system behavior is expected to be equivalent.
Equivalence classes
Equivalence classes defined by atomic propositions partition the input space into groups where inputs are expected to behave similarly. By testing combinations of representative inputs from each class, we can reduce the number of combinations that need to be checked, assuming equivalent behavior for all inputs within the same class. This approach is especially useful when it’s not feasible to check all possible combinations due to the large or infinite cardinality (the number of unique values) of inputs.
“Therefore, equivalence classes allow for the reduction of the number of combinations that need to be checked.”
To illustrate how we can use atomic propositions and equivalence classes, we’ll again use a memory function as our system under test, which we explored in the Combinatorial Testing: Writing Behavior Model post.
However, before we start applying atomic propositions and equivalence classes to a real system under test, let’s take a more formal approach and define these concepts more precisely using the formal mathematical notation commonly found in scientific papers related to formal methods.
Definition of atomic propositions ()
Let be atomic propositions that describe various properties of the system. The set is the collection of all these atomic propositions:
In Python, we can represent this definition as follows:
1 | # 'set' is a collection of unordered unique elements |
Remember that an atomic proposition is a logical statement that evaluates to either true or false. For example:
Each is an atomic proposition that evaluates to true or false based on the values of the system’s variables in a particular state . Thus, for any , we have:
where:
- is the current state of the system,
- are the variables of the system,
- is a logical condition on these variables that defines .
In Python, each atomic proposition can be thought of as a function that returns either a True
or False
boolean value:
1 | # Define atomic proposition p_i as a function of system state s(v1), s(v2), ..., s(vn) |
Now, let’s break the set of atomic propositions into separate components based on input variables, model (internal) variables, and output variables, and redefine as follows:
where:
- is the set of atomic propositions that relate to input variables.
- is the set of atomic propositions that relate to model (internal) variables.
- is the set of atomic propositions that relate to output variables.
In Python, can be represented as a list that includes all atomic propositions, which we can split into three separate lists for input, model, and output variables, respectively:
1 | # Define the lists for AP_I, AP_M, and AP_O |
Since we are performing black box testing, this decomposition of is very convenient. We can define atomic propositions related only to (input) and (output), as we may not have access to the internals of the implementation to know the (model) variables.
Definition of Equivalence classes
We can informally define equivalent classes as a group of inputs that produce equivalent system behavior. A formal definition can be taken from the paper Exhaustive Model-Based Equivalence Class Testing by W. Huang and J. Peleska, 2013, where input equivalence class partitions (IECP) are defined as follows:
Where:
- : The domain of input variables.
- : An atomic proposition evaluated with the input variable substituted for . This means that the proposition is evaluated based on the current value of the input variable.
- : A subset of the atomic propositions from , the set of atomic propositions related to input variables.
- : Logical AND operator that requires all atomic propositions in to be true.
- : Negation of atomic proposition , meaning the proposition is false.
- : Removes empty sets, ensuring that we don’t include cases where no states match.
The expression means that is a subset of , but we consider all possible subsets , therefore represents elements from the powerset of .
To clarify:
- The expression means that is any subset of .
- Given that we are considering all possible values of , we are essentially looking at the powerset , which includes all subsets of , including the empty set and itself.
Thus, when you’re iterating over all possible subsets , you’re effectively iterating over the powerset .
In Python, we can calculate a powerset as follows:
1 | # Define the original set (as a list, set, or tuple) |
We can simplify the definition and remove so that we can only focus on the equivalence classes without specifying values for the input variables. Removing , we get a simplified expression:
Where:
- : An atomic proposition evaluated based on the values of input variables .
- : Negation of atomic proposition , meaning the proposition is false.
Simplified is just a Cartesian product
Even though the simplified version of still looks intimidating,
it is equivalent to a Cartesian product of all possible true and false values for each atomic proposition in the set . Each atomic proposition can either be true, represented as
or false, represented as
The set of all possible combinations of these truth values is effectively the Cartesian product of the two possible states for each atomic proposition:
This Cartesian product represents all possible subsets , where for each subset , the propositions in are true, and those not in are false. By evaluating the truth of the propositions for all possible subsets , we generate all possible truth value assignments across the set of atomic propositions.
The memory function
Let’s use a simple memory function as an example to demonstrate the application of atomic propositions and equivalence classes in a practical context. This memory function will allow us to see how these concepts work together in organizing and testing input scenarios based on expected behaviors.
In Python, we’ll define the memory
function as follows:
1 | def memory(addr, value=0, mode="r", default=0, mem_={}): |
Atomic propositions for input variables () of the memory function
Defining atomic propositions for a real-world black-box tested software system is not easy. A tester must be able to break down the system’s inputs into the simplest, indivisible conditions that affect the system’s behavior (the output or the internal state). The focus must always be on behavior-causing differences. If the system has internal states, like our memory function, then differences in behavior must be considered for each state.
“Focus on behavior-causing differences.”
An iterative approach works best. Start with high-level atomic propositions and refine them as needed, keeping the focus on behavior-causing differences.
High-level atomic propositions
If you don’t know where to start, it always helps to start with simple propositions that state the validity of each input variable. After all, we do expect that each input must have some valid value and we do expect that valid input should cause differences in system behavior as compared to invalid input.
Therefore, we can define the following high-level atomic propositions for each input variable (addr
, value
, mode
, default
):
- : `addr` is valid
- : `value` is valid
- : `mode` is valid
- : `default` is valid
Having a set of our four simple high-level atomic propositions in hand, we can use them to define the equivalence classes that correspond to these propositions using the definition . There are classes where is the number of propositions. In our case, we have propositions, which gives us classes.
Class | ||||
Class 1 | ||||
Class 2 | ||||
Class 3 | ||||
Class 4 | ||||
... | ||||
Class 16 |
Note that (logical AND
) operation is implied between all the columns. For example, Class 2, means that addr
is valid, value
is valid, mode
is valid, but default
value is invalid.
You can also recognize that equivalence classes are generated similar to how you count in binary and the invalid input is automatically considered by negation of each proposition. This means defining a proposition like would be redundant because logically means that and would be just .
In Python, we can calculate this simply by using the Cartesian product (testflows.combinatorics.product
or itertools.product
) function as follows:
1 | list(product(['p1','¬p1'],['p2','¬p2'],['p3','¬p3'],['p4','¬p4'])) |
1 | [('p1', 'p2', 'p3', 'p4'), |
If you don’t remember how a Cartesian product works, recall that a Cartesian product can be represented using nested for-loops as follows:
1 | for p1 in ['p1','¬p1']: |
In a TestSketch which supports the either() function, the same Cartesian product can be naturally defined as possibilities as follows:
1 |
|
Defining the meaning of each proposition and its negation
Having defined the first four high-level propositions and the equivalent classes derived from them, we need to give meaning to what it actually means for a given input to be valid or invalid. For this, we need to look at each input individually, as what it means to be valid or invalid for one input does not apply to another. We’ll define an input to be invalid when the memory function raises an exception; otherwise, we’ll consider any value that does not lead to an exception to be valid. Therefore, now we just need to think if there are any values for each input that would cause the memory function to raise an exception.
After a quick examination of the memory function implementation, we can conclude the following:
The
addr
is valid when the value is hashable and invalid when it is not hashable. This is because theaddr
is used as a key in a dictionary, and Python dictionary keys must be hashable.The
value
is valid for any value, and therefore there are no invalid values for it.The
mode
is valid when the value is iterable and invalid when it is not. This is because themode
is used with thein
operator, which only works for iterable objects.The
default
is valid for any value, and therefore there are no invalid values for it.
Filtering out invalid classes
Given that both value
and default
inputs don’t have invalid values, we reduce the equivalent classes to just four. This is because value
and default
propositions must always be true, and only propositions for addr
and mode
can vary.
Class | ||||
Class 1 | ||||
Class 2 | ||||
Class 3 | ||||
Class 4 |
Refining atomic propositions
We’ve started with high-level input validity propositions and after analysis of what valid and invalid values can be for each input, we’ve narrowed down our equivalence classes to just four. However, as intuition tells us, this is not enough to test the memory function. This is because we need to think about if all values that fall into the valid or invalid class for a given variable would lead to the same behavior, or if some values would cause the behavior to be different.
Let’s start with the mode
and add additional atomic propositions that would cause differences in behavior. When mode
is invalid, the only behavior that we expect is an exception, so we don’t need to add an additional proposition to differentiate behavior when mode
is invalid. However, this is not the case when mode
is valid. When the mode
is valid, the behavior of the system will depend on the presence or absence of each mode flag r
, w
, and e
. Therefore, we need to add additional propositions
to account for difference in the behavior when these flags are set. This gives us
three new propositions:
- : `r` in `mode`
- : `w` in `mode`
- : `e` in `mode`
Next, let’s think about the addr
. If addr
is invalid, meaning the value is non-hashable, we expect the behavior to be the same - an exception will be raised. Now, what about when addr
is valid? Can we say that for any valid value of addr
the behavior is the same? The answer is obviously, no. It is a memory function after all, so the behavior of the system depends on the actual value of the addr
. Therefore, we need to add an additional proposition to cover this.
- : `addr` is set to valid value `A`
The same logic will apply for the value
argument. The invalid case does not even apply; however, for valid values we expect that the behavior of the system will be different for different values. Therefore, again we need to add an additional proposition to cover it.
- : `value` is set to valid value `V`
Note that we only want to fix a value for addr
and value
inputs when these values are valid. We don’t care about fixing any values for the invalid cases for these variables.
The last one is the default
. The invalid case again does not apply, but even for the valid case, we expect the system to behave the same irrespective of the actual value set for the default
. Therefore, we don’t need to add any additional propositions related to the default
.
It is clear from the above that choosing the right propositions requires a tester to think about the system at the right abstraction level. Not too high and not too low, but just enough to cover the important cases that lead to different behaviors.
The previously stated quote is critical to defining atomic propositions for real-world systems at hand.
“Focus on behavior-causing differences” - specific variations in inputs that lead a software system to exhibit different behaviors.
Also, note that we are maintaining the right level of abstraction by saying that for addr
and value
the actual value matters, but we don’t care what it actually is. Instead, we do care when the value will be different to the one we select, which is covered by the negation of those propositions.
For the memory function, the full set of atomic propositions now sits at nine and is the following:
- : `addr` is valid
- : `addr` is set to valid value `A`
- : `value` is valid
- : `value` is set to valid value `V`
- : `mode` is valid
- : `r` in `mode`
- : `w` in `mode`
- : `e` in `mode`
- : `default` is valid
We can scratch our heads now and ask if we’ve defined enough propositions? What does it mean to be enough? Well, enough is simply the smallest set of propositions that cover all possible differences in system’s behavior. Remember that the negations of these propositions are included by default.
Equivalence classes from refined propositions
Having our nine refined propositions ready, we can now build our equivalence classes. If we consider each proposition to be independent, then we would have classes. However, some propositions are dependent, and we need to take that into account.
Let’s start with and , which are propositions related to the addr
. When (address is invalid), the is a don’t care. Therefore, for and , we only have possible combinations.
Description | ||
---|---|---|
addr is valid and is A | ||
addr is valid and is B (not A) | ||
addr is invalid and value doesn't matter |
For the two propositions related to the value
, and , we know that we don’t need to consider ,
as value can’t be invalid. Therefore, we only have possible combinations.
Description | ||
---|---|---|
value is valid and is V | ||
value is valid and is W (not V) |
Next, let’s look at propositions for the mode
. The mode is covered by propositions , , , and . Here, we note that when , the mode is invalid, and the other propositions , , and are don’t care. Therefore, we have possible combinations .
Description | ||||
---|---|---|---|---|
mode is valid and 'rwe' flags are set | ||||
mode is valid and 'rw' flags are set | ||||
... | ||||
mode is valid and no flags are set | ||||
mode is invalid and flags don't care |
Lastly, we only have one proposition for default
, which is . Given that the default value can only be valid, there is only possible combination.
Description | |
---|---|
default value is valid and exact value doesn't matter |
Therefore, the total number of equivalent classes that we need to consider is:
giving us only classes that we need to consider for comprehensive test coverage of the memory function. This is much less than , if we did not consider interdependency between propositions and when valid or invalid propositions actually applied.
Table of equivalence classes
Here are all the classes and the description for each:
Table: Equivalent Classes
Class | Description | |||||||||
---|---|---|---|---|---|---|---|---|---|---|
1 | False | N/A | True | True | False | N/A | N/A | N/A | True | addr invalid; value set to V; mode invalid; default is valid |
2 | False | N/A | True | False | False | N/A | N/A | N/A | True | addr invalid; value not V; mode invalid; default is valid |
3 | False | N/A | True | True | True | False | False | False | True | addr invalid; value set to V; mode valid; no flags; default is valid |
4 | False | N/A | True | False | True | False | False | False | True | addr invalid; value not V; mode valid; no flags; default is valid |
5 | False | N/A | True | True | True | False | False | True | True | addr invalid; value set to V; mode 'e'; erases memory; default is valid |
6 | False | N/A | True | False | True | False | False | True | True | addr invalid; value not V; mode 'e'; erases memory; default is valid |
7 | False | N/A | True | True | True | False | True | False | True | addr invalid; value set to V; mode 'w'; writes value; default is valid |
8 | False | N/A | True | False | True | False | True | False | True | addr invalid; value not V; mode 'w'; writes value; default is valid |
9 | False | N/A | True | True | True | False | True | True | True | addr invalid; value set to V; mode 'w' & 'e'; erases memory; writes value; default is valid |
10 | False | N/A | True | False | True | False | True | True | True | addr invalid; value not V; mode 'w' & 'e'; erases memory; writes value; default is valid |
11 | False | N/A | True | True | True | True | False | False | True | addr invalid; value set to V; mode 'r'; attempts to read; default is valid |
12 | False | N/A | True | False | True | True | False | False | True | addr invalid; value not V; mode 'r'; attempts to read; default is valid |
13 | False | N/A | True | True | True | True | False | True | True | addr invalid; value set to V; mode 'r' & 'e'; attempts to read; erases memory; default is valid |
14 | False | N/A | True | False | True | True | False | True | True | addr invalid; value not V; mode 'r' & 'e'; attempts to read; erases memory; default is valid |
15 | False | N/A | True | True | True | True | True | False | True | addr invalid; value set to V; mode 'r' & 'w'; attempts to read; writes value; default is valid |
16 | False | N/A | True | False | True | True | True | False | True | addr invalid; value not V; mode 'r' & 'w'; attempts to read; writes value; default is valid |
17 | False | N/A | True | True | True | True | True | True | True | addr invalid; value set to V; mode all flags; reads; erases memory; writes value; default is valid |
18 | False | N/A | True | False | True | True | True | True | True | addr invalid; value not V; mode all flags; reads; erases memory; writes value; default is valid |
19 | True | False | True | True | False | N/A | N/A | N/A | True | addr valid; not A; value set to V; mode invalid; default is valid |
20 | True | False | True | False | False | N/A | N/A | N/A | True | addr valid; not A; value not V; mode invalid; default is valid |
21 | True | False | True | True | True | False | False | False | True | addr valid; not A; mode valid; no flags; default is valid |
22 | True | False | True | False | True | False | False | False | True | addr valid; not A; value not V; mode valid; no flags; default is valid |
23 | True | False | True | True | True | False | False | True | True | addr valid; not A; mode 'e'; erases memory; default is valid |
24 | True | False | True | False | True | False | False | True | True | addr valid; not A; value not V; mode 'e'; erases memory; default is valid |
25 | True | False | True | True | True | False | True | False | True | addr valid; not A; mode 'w'; writes value; default is valid |
26 | True | False | True | False | True | False | True | False | True | addr valid; not A; value not V; mode 'w'; writes value; default is valid |
27 | True | False | True | True | True | False | True | True | True | addr valid; not A; mode 'w' & 'e'; erases memory; writes value; default is valid |
28 | True | False | True | False | True | False | True | True | True | addr valid; not A; value not V; mode 'w' & 'e'; erases memory; writes value; default is valid |
29 | True | False | True | True | True | True | False | False | True | addr valid; not A; mode 'r'; reads from addr; returns value or default |
30 | True | False | True | False | True | True | False | False | True | addr valid; not A; value not V; mode 'r'; reads from addr; returns value or default |
31 | True | False | True | True | True | True | False | True | True | addr valid; not A; mode 'r' & 'e'; reads; erases memory; returns value or default |
32 | True | False | True | False | True | True | False | True | True | addr valid; not A; value not V; mode 'r' & 'e'; reads; erases memory; returns value or default |
33 | True | False | True | True | True | True | True | False | True | addr valid; not A; mode 'r' & 'w'; reads; writes value; returns value or default |
34 | True | False | True | False | True | True | True | False | True | addr valid; not A; value not V; mode 'r' & 'w'; reads; writes value; returns value or default |
35 | True | False | True | True | True | True | True | True | True | addr valid; not A; mode all flags; reads; erases memory; writes value; returns value or default |
36 | True | False | True | False | True | True | True | True | True | addr valid; not A; value not V; mode all flags; reads; erases memory; writes value; returns value or default |
37 | True | True | True | True | False | N/A | N/A | N/A | True | addr valid; A; mode invalid; default is valid |
38 | True | True | True | False | False | N/A | N/A | N/A | True | addr valid; A; value not V; mode invalid; default is valid |
39 | True | True | True | True | True | False | False | False | True | addr valid; A; mode valid; no flags; default is valid |
40 | True | True | True | False | True | False | False | False | True | addr valid; A; value not V; mode valid; no flags; default is valid |
41 | True | True | True | True | True | False | False | True | True | addr valid; A; mode 'e'; erases memory; default is valid |
42 | True | True | True | False | True | False | False | True | True | addr valid; A; value not V; mode 'e'; erases memory; default is valid |
43 | True | True | True | True | True | False | True | False | True | addr valid; A; mode 'w'; writes value; default is valid |
44 | True | True | True | False | True | False | True | False | True | addr valid; A; value not V; mode 'w'; writes value; default is valid |
45 | True | True | True | True | True | False | True | True | True | addr valid; A; mode 'w' & 'e'; erases memory; writes value; default is valid |
46 | True | True | True | False | True | False | True | True | True | addr valid; A; value not V; mode 'w' & 'e'; erases memory; writes value; default is valid |
47 | True | True | True | True | True | True | False | False | True | addr valid; A; mode 'r'; reads from addr; returns value |
48 | True | True | True | False | True | True | False | False | True | addr valid; A; value not V; mode 'r'; reads from addr; returns value |
49 | True | True | True | True | True | True | False | True | True | addr valid; A; mode 'r' & 'e'; reads; erases memory; returns value |
50 | True | True | True | False | True | True | False | True | True | addr valid; A; value not V; mode 'r' & 'e'; reads; erases memory; returns value |
51 | True | True | True | True | True | True | True | False | True | addr valid; A; mode 'r' & 'w'; reads; writes value; returns value |
52 | True | True | True | False | True | True | True | False | True | addr valid; A; value not V; mode 'r' & 'w'; reads; writes value; returns value |
53 | True | True | True | True | True | True | True | True | True | addr valid; A; mode all flags; reads; erases memory; writes value; returns value |
54 | True | True | True | False | True | True | True | True | True | addr valid; A; value not V; mode all flags; reads; erases memory; writes value; returns value |
Conclusion
In this first part, we’ve introduced formal definitions for atomic propositions and equivalence classes, applying them to a memory function as a practical example. By analyzing each input variable and refining our initial set of propositions, we reduced the potential input space to a manageable set of equivalence classes. Through this process, we illustrated how to focus on behavior-causing differences in inputs, ensuring comprehensive test coverage without redundancy.
Next, in Part 2, we’ll explore how to take internal states into account, select specific input values, and use a combinatorial sketch to cover all equivalence classes effectively.