03. Aserciones
Objetivos
Los objetivos de este módulo son:
- Entender el concepto de aserción y su aplicación al lenguaje de programación C.
- Ser capaz de definir las precondiciones y postcondiciones en programas escritos en C.
Introducción
Las aserciones (assert en inglés) son aquellas condiciones que un programa debe cumplir en ciertos momentos concretos. Aunque podemos definir aserciones en cualquier punto de nuestro código para asegurar que se cumplen ciertas restricciones, los mínimos a asegurar son que las condiciones iniciales y finales se cumplen. Estas condiciones iniciales y finales corresponden a las precondiciones y postcondiciones.
Cuando una aserción no se cumple, el programa se detiene y se genera un error. Esto nos permite detectar puntos de nuestro código en los que algo falla. Hay que tener en cuenta que las aserciones sirven para detectar errores del programa, no errores de ejecución. Los errores del programa son errores en la codificación, y no deberían darse nunca, por lo tanto hay que detectarlos y corregirlos. Por el contrario, los errores de ejecución son aquellos que se pueden dar debido a ciertas situaciones que se pueden dar durante la ejecución de un programa (por ejemplo quedarse sin memoria), y hay que controlarlos y reaccionar correctamente a ellos, pero no son errores del programa.
Es importante tener en cuenta esta distinción, ya que las aserciones sólo funcionarán cuando compilamos en modo Test o Debug. Cuando la aplicación se compila y se ejecuta en modo Release las aserciones no funcionan. Esto se debe a que existe una constante llamada NDEBUG (no debug) que si está definida hace que las aserciones se desactiven. Por defecto, cuando compilamos nuestro código en modo Release esta constante se encuentra definida.
En este módulo veremos el funcionamiento básico de las aserciones, como podemos incluirlas en la documentación y algunos ejemplos típicos.
Aserciones en C
Las aserciones en C se controlan mediante la acción assert, definida en el fichero de cabeceras assert.h. Por lo tanto, será necesario incluir este archivo para poder utilizarlas. La acción assert espera que se le pase una expresión como parámetro, que debe ser cierta. En caso de que no lo sea, la ejecución del programa finaliza y se muestra un error indicando el lugar donde está la aserción de que no se ha cumplido.
Si queremos desactivar las aserciones se puede hacer (siempre y cuando estemos seguros de que nuestro código es correcto) declarando esta constante con la siguiente línea de código:
Una buena práctica es indicar qué aserciones se contemplan en un método dado. Esto lo podemos hacer añadiendo la información con comentarios a la definición del método en el fichero de cabeceras. Fijaros en los ejemplos cómo se ha documentado cada método en su implementación en lenguaje C. Tened en cuenta que en estos casos no utilizamos ficheros de cabecera, por lo tanto se han puesto directamente en la implementación.
Ejemplos
A continuación se muestran algunos ejemplos típicos del uso de las aserciones. Se muestra las precondiciones y su traducción a asserts:
Ejemplo 03_01: control de índices
Un caso típico en el que las aserciones nos pueden ayudar es a la hora de verificar que los índices están en el rango correcto. Dada la definición de una tabla de enteros, fijaros como se ha definido las precondiciones para una función getVal que nos devuelve el valor en la posición indicada de la tabla.
const
MAX_ELEMENTS: integer = 30;
end const
type
tIntTable = record
elements: vector[MAX_ELEMENTS] of integer;
numElements: integer;
end record
end type
var
table: tIntTable;
end var
{ Pre: table=TABLE ʌ TABLE.numElements>=0 ʌ TABLE.numElements<=MAX_ELEMENTS ʌ pos=POS ʌ POS>0 ʌ POS<=TABLE.numElements }
function getVal(table: tIntTable, pos: integer): integer
return table.elements[pos];
end function
#define MAX_ELEMENTS 30
typedef struct {
int elements[MAX_ ELEMENTS];
int numElements
} tIntTable;
tIntTable table;
/* getVal: Returns the value in the given position of the table
* - table: Table containing the values
* - pos: Position to be retrieved
* return: The integer value in the position pos
* Assertions:
* 'pos' is a positive values and lower than the number of elements of the table
*/
int getVal(tIntTable table, int pos) {
assert(pos >= 0);
assert(pos < table.numElements);
return table.elements[pos];
}
Ejemplo 03_02: parámetros por referencia
Otro caso típico del uso de las aserciones es cuando recibimos parámetros por referencia (ya sea de salida o de entrada/salida). Hay que tener en cuenta que estos parámetros son punteros, y como tales, puede darse el caso de que tengan un valor NULL. Fijaros en el siguiente ejemplo, en el que recibimos dos enteros y devolvemos la suma de estos enteros en un parámetro de salida.
{ Pre: a=A ʌ b=B ʌ c=C ʌ C ∈ Z }
action sumVals(in a: integer, in b: integer, out c: integer)
c := a+b;
end action
/* sumVals: Sum two integer values
* - a: Integer value
* - b: Integer value
* - c: Result of the addition of a and b
* Assertions:
* 'c' is a not NULL pointer
*/
void sumVals(int a, int b, int *c) {
assert(c != NULL);
*c=a+b;
}
Tened en cuenta que en este caso, como en lenguaje algorítmico el parámetro c no es un puntero, lo que hacemos es indicar en la precondición de que el valor que tiene asignado debe pertenecer al tipo entero, o sea, ser un entero válido. En caso de que el parámetro fuera una tabla o un tipo estructurado, deberíamos hacer lo mismo, pero el tipo cambiaría. Por ejemplo, en caso de que tuviéramos un método que tomara una tabla de tipo tIntTable como parámetro de entrada/salida y devolviera la suma de todos los valores, la precondición sería:
{ Pre: table=TABLE ʌ TABLE.numElements>=0 ʌ TABLE.numElements<=MAX_ELEMENTS ʌ TABLE ∈ tIntTable }
Ejemplo 03_03: recursividad
En este último ejemplo veremos cómo aplicar las aserciones a una función recursiva. Recordemos que una función recursiva es aquella que se llama a sí misma. Un ejemplo típico es el cálculo del factorial. El factorial de n, o sea, n! se puede calcular de la siguiente forma:
n! = n*(n-1)! = n*(n-1)*(n-2)! = n*(n-1)* ... *1
Podemos definir esta función de la siguiente forma:
{ Pre: n=N ʌ N>0 }
function fact(n: integer): integer
if n=1 then
return 1;
else
return n * fact(n-1);
end if
end function
/* fact: Calculate the factorial of n
* - n: Integer value
* return: The factorial of n
* Assertions:
* 'n' is a positive value
*/
int fact(int n) {
assert(n > 0);
if (n == 1) {
return 1;
} else {
return n * fact(n-1);
}
}
Fijaros en que lo que estamos haciendo es asegurar que la variable de control de la recursividad comienza en un estado válido. En caso de que nos pasaran un valor negativo de n, esta función se llamaría de forma indefinida, hasta que se quedara sin memoria y fallara la aplicación.
Resumen
En este módulo hemos visto con traducir las precondiciones a lenguaje C, aplicándolas a nuestros programas. En el caso de las postcondiciones, el tratamiento sería exactamente el mismo. También hemos visto usos típicos de las aserciones en diferentes ejemplos.