Marco de plantillas de prueba

Dejar${\displaystyle Op}$Sea una operación Z.${\displaystyle x_{1}\dots x_{n}}$sean todas las variables de entrada y de estado (no primadas) a las que se hace referencia en${\displaystyle Op}$, y${\displaystyle T_{1}\dots T_{n}}$sus tipos correspondientes. El espacio de entrada (EI) de${\displaystyle Op}$, escrito${\displaystyle Op_{is}}$, es el cuadro de esquema Z definido por${\displaystyle [x_{1}:T_{1}\dots x_{n}:T_{n}]}$.

Dejar${\displaystyle Op}$Sea una operación Z.${\displaystyle {\text{pre }}Op}$ser la condición previa de${\displaystyle Op}$. El espacio de entrada válido (VIS) de${\displaystyle Op}$, escrito${\displaystyle Op_{vis}}$, es el cuadro de esquema Z definido por${\displaystyle [Op_{is}|{\text{pre }}Op]}$.

Dejar${\displaystyle Op}$ser una operación Z y dejar${\displaystyle P}$sea ​​cualquier conjunción de predicados atómicos que dependan de una o más de las variables definidas en${\displaystyle Op_{vis}}$. Luego, el cuadro de esquema Z${\displaystyle [Op_{vis}|P]}$es una clase de prueba de${\displaystyle Op}$. Tenga en cuenta que este esquema es equivalente a${\displaystyle [Op_{is}|{\text{pre }}Op\land P]}$Esta observación puede generalizarse diciendo que si${\displaystyle Op_{c}}$es una clase de prueba de${\displaystyle Op}$, luego el cuadro de esquema Z definido por${\displaystyle [Op_{c}|P]}$es también una clase de prueba de${\displaystyle Op}$Según esta definición, el VIS también es una clase de prueba.

Si${\displaystyle Op_{c}}$es una clase de prueba de${\displaystyle Op}$, entonces el predicado${\displaystyle P}$en${\displaystyle Op_{c'}==[Op_{c}|P]}$Se dice que es el predicado característico de${\displaystyle Op_{c'}}$o${\displaystyle Op_{c'}}$se caracteriza por${\displaystyle P}$.

Las clases de prueba también se denominan objetivos de prueba, plantillas de prueba, especificaciones de prueba y condiciones de prueba.

En el contexto de la TTF, una táctica de prueba ^{[ 1 ]} es un medio para particionar cualquier clase de prueba de cualquier operación. Sin embargo, algunas de las tácticas de prueba utilizadas en la práctica no siempre generan una partición de algunas clases de prueba.

Algunas de las tácticas de prueba propuestas originalmente para el TTF son las siguientes:

• Forma Normal Disyuntiva (FND). Al aplicar esta táctica, la operación se escribe en Forma Normal Disyuntiva y la clase de prueba se divide en tantas clases de prueba como términos tenga el predicado de la operación resultante. El predicado que se agrega a cada nueva clase de prueba es la precondición de uno de los términos del predicado de la operación.
• Particiones estándar (PE). Esta táctica utiliza una partición predefinida de algún operador matemático. ^{[ 1 ]} Por ejemplo, la siguiente es una buena partición para expresiones de la forma${\displaystyle S\spadesuit T}$dónde${\displaystyle \spadesuit }$es uno de${\displaystyle \cup }$,${\displaystyle \cap }$y${\displaystyle \setminus }$(véase Teoría de conjuntos ).

  ${\displaystyle {\begin{array}{l|l}S=\emptyset ,T=\emptyset &S\neq \emptyset ,T\neq \emptyset ,S\subset T\\\hline S=\emptyset ,T\neq \emptyset &S\neq \emptyset ,T\neq \emptyset ,T\subset S\\\hline S\neq \emptyset ,T=\emptyset &S\neq \emptyset ,T\neq \emptyset ,T=S\\\hline S\neq \emptyset ,T\neq \emptyset ,S\cap T=\emptyset &S\neq \emptyset ,T\neq \emptyset ,S\cap T\neq \emptyset ,\lnot (S\subseteq T),\lnot (T\subseteq S),S\neq T\end{array}}}$

  Como puede observarse, las particiones estándar pueden variar en función de la cantidad de pruebas que el ingeniero desee realizar.

• Propagación de subdominios (SDP). Esta táctica se aplica a expresiones que contienen:
  1. Dos o más operadores matemáticos para los que ya existen particiones estándar definidas, o
  2. Operadores matemáticos que se definen en términos de otros operadores matemáticos.

  En cualquiera de estos casos, las particiones estándar de los operadores que aparecen en la expresión o en la definición de una compleja se combinan para producir una partición para la expresión. Si la táctica se aplica al segundo caso, la partición resultante puede considerarse como la partición estándar para ese operador. Stocks y Carrington ilustran esta situación con${\displaystyle R\oplus G=({\text{dom }}G\ntriangleleft R)\cup G}$, dónde${\displaystyle \ntriangleleft }$significa anti-restricción de dominio , al proporcionar particiones estándar para${\displaystyle \ntriangleleft }$y${\displaystyle \cup }$y propagándolos para calcular una partición para${\displaystyle \oplus }$.

• Mutación de especificación (SM). El primer paso de esta táctica consiste en generar una versión modificada de la operación Z. Una versión modificada de una operación Z es similar en concepto a una versión modificada de un programa , es decir, es una versión modificada de la operación. El ingeniero introduce la modificación con la intención de descubrir un error en la implementación. La versión modificada debe ser la especificación que el ingeniero supone que el programador ha implementado. A continuación, el ingeniero debe calcular el subconjunto del VIS que produce resultados diferentes en ambas especificaciones. El predicado de este conjunto se utiliza para derivar una nueva clase de prueba.

Otras tácticas de prueba que también se pueden utilizar son las siguientes:

• En la Extensión de Conjuntos (ISE). Se aplica a predicados de la forma${\displaystyle expr\in \{expr_{1},\dots ,expr_{n}\}}$. En este caso, genera n clases de prueba tales que un predicado de la forma${\displaystyle expr=expr_{i}}$se añade a cada uno de ellos.
• Conjunto de pruebas obligatorio (MTS). Esta táctica asocia un conjunto de valores constantes a una variable VIS y genera tantas clases de prueba como elementos haya en el conjunto. Cada clase de prueba se caracteriza por un predicado de la forma${\displaystyle var=val}$donde var es el nombre de la variable y val es uno de los valores del conjunto.
• Intervalos enteros (IS). Esta táctica se aplica únicamente a las variables de VIS de tipo${\displaystyle \mathbb {Z} }$(o su "subtipo")${\displaystyle \mathbb {N} }$). Consiste en asociar un rango a una variable y derivar clases de prueba comparando la variable con los límites del rango de alguna manera. Más formalmente, sea n una variable de tipo${\displaystyle \mathbb {Z} }$y dejar${\displaystyle [i,j]}$sea ​​el rango asociado. Luego, la táctica genera las clases de prueba caracterizadas por los siguientes predicados:${\displaystyle n<i}$,${\displaystyle n=i}$,${\displaystyle i<n\land n<j}$,${\displaystyle n=j}$,${\displaystyle n>j}$. La táctica se generaliza fácilmente a una lista de números enteros .
• Tipo suma (ST). Esta táctica genera tantas clases de prueba como elementos se pueden construir en un tipo suma aplicando todos los constructores del tipo. En otras palabras, si un modelo define el tipo COLOUR  ::= red | blue | green y alguna operación usa c de tipo COLOUR , entonces al aplicar esta táctica cada clase de prueba se dividirá en tres nuevas clases de prueba: una en la que c es igual a red , otra en la que c es igual a blue y la tercera en la que c es igual a green .
• Subconjunto propio de extensión de conjunto (PSSE). Esta táctica utiliza el mismo concepto de ISE, pero aplicado a inclusiones de conjuntos. PSSE ayuda a probar operaciones que incluyen predicados como${\displaystyle expr\subset \{expr_{1},\dots ,expr_{n}\}}$Cuando se aplica PSSE, genera${\displaystyle 2^{n}-1}$clases de prueba donde un predicado de la forma${\displaystyle expr=A_{i}}$con${\displaystyle i\in [1,2^{n}-1]}$y${\displaystyle A_{i}\in \mathbb {P} \{expr_{1},\dots ,expr_{n}\}\setminus \{\{expr_{1},\dots ,expr_{n}\}\}}$, se añade a cada clase.${\displaystyle \{expr_{1},\dots ,expr_{n}\}}$está excluido de${\displaystyle \mathbb {P} \{expr_{1},\dots ,expr_{n}\}}$porque expr es un subconjunto propio de${\displaystyle \{expr_{1},\dots ,expr_{n}\}}$.
• Cardinalidad de conjunto (SC). Esta táctica se aplica a variables de tipo conjunto. El usuario selecciona una de dichas variables (${\displaystyle v}$) y un número entero positivo (${\displaystyle n}$). La táctica genera una especificación de prueba caracterizada por${\displaystyle |v|=m}$para cada${\displaystyle m\in [0,n]}$.

La aplicación de una táctica de prueba al VIS genera algunas clases de prueba. Si algunas de estas clases de prueba se subdividen aplicando una o más tácticas de prueba, se obtiene un nuevo conjunto de clases de prueba. Este proceso puede continuar aplicando tácticas de prueba a las clases de prueba generadas hasta el momento. Evidentemente, el resultado de este proceso puede representarse como un árbol con el VIS como nodo raíz, las clases de prueba generadas por la primera táctica de prueba como sus hijos, y así sucesivamente. Además, Stocks y Carrington proponen utilizar la notación Z para construir el árbol, como se muestra a continuación.

${\displaystyle {\begin{aligned}VIS&==[IS|P]\\TCL_{T_{1}}^{1}&==[VIS|P_{T_{1}}^{1}]\\&\dots \\TCL_{T_{1}}^{n}&==[VIS|P_{T_{1}}^{n}]\\TCL_{T_{2}}^{1}&==[TCL_{T_{1}}^{i}|P_{T_{2}}^{1}]\\&\dots \\TCL_{T_{2}}^{m}&==[TCL_{T_{1}}^{i}|P_{T_{2}}^{m}]\\&\dots \\TCL_{T_{3}}^{1}&==[TCL_{T_{2}}^{j}|P_{T_{3}}^{1}]\\&\dots \\TCL_{T_{3}}^{k}&==[TCL_{T_{2}}^{j}|P_{T_{3}}^{k}]\\&\dots \\&\dots \\&\dots \end{aligned}}}$

Las tácticas de prueba en TTF tienden a generar clases de prueba insatisfactorias. Estas clases deben eliminarse del árbol de pruebas porque representan combinaciones imposibles de valores de entrada; es decir, no se puede derivar ningún caso de prueba abstracto a partir de ellas.

Un caso de prueba abstracto es un elemento que pertenece a una clase de prueba . El TTF indica que los casos de prueba abstractos deben derivarse solo de las hojas del árbol de pruebas . Los casos de prueba abstractos también pueden escribirse como cajas de esquema Z.${\displaystyle Op}$sea ​​alguna operación, dejemos${\displaystyle Op_{vis}}$ser el VIS de${\displaystyle Op}$, dejar${\displaystyle x_{1}:T_{1}\dots x_{n}:T_{n}}$sean todas las variables declaradas en${\displaystyle Op_{vis}}$, dejar${\displaystyle Op_{c}}$ser una clase de prueba (hoja) del árbol de prueba asociado a${\displaystyle Op}$, dejar${\displaystyle P_{1}\dots P_{m}}$sean los predicados característicos de cada clase de prueba de${\displaystyle Op_{c}}$arriba a${\displaystyle Op_{vis}}$(siguiendo los bordes desde el hijo hasta el padre ), y dejar${\displaystyle v_{1}:T_{1}\dots v_{n}:T_{n}}$ser${\displaystyle n}$valores constantes que satisfacen${\displaystyle P_{1}\land \dots \land P_{m}}$. Luego, un caso de prueba abstracto de${\displaystyle Op_{c}}$es el cuadro de esquema Z definido por${\displaystyle [Op_{c}|x_{1}=v_{1}\land \dots \land x_{n}=v_{n}]}$.