03. Assercions
Objectius
Els objectius d'aquest mòdul són:
- Entendre el concepte de asserció i la seva aplicació al llenguatge de programació C.
- Ser capaç de definir les precondicions i postcondicions en programes escrits en C.
Introducció
Les assercions (asserts en anglès) són aquelles condicions que un programa ha de complir en certs moments concrets. Tot i que podem definir assercions a qualsevol punt del nostre codi per assegurar que es compleixen certes restriccions, els mínims a assegurar són que les condicions inicials i finals es compleixen. Aquestes condicions inicials i finals corresponen a les precondicions i postcondicions.
Quan una asserció no es compleix, el programa s'atura i es genera un error. Això ens permet detectar punts del nostre codi en els que alguna cosa falla. Cal tenir en compte que les assercions serveixen per detectar errors del programa, no errors d'execució. Els errors del programa són errates en la codificació, i no s'haurien de donar mai, per tant cal detectar-los i corregir-los. Per altre costat, els errors d'execució són aquells que es poden donar degut a certes situacions que es poden donar durant la execució d'un programa (per exemple quedar-se sense memòria), i cal controlar-los i reaccionar correctament a ells, però no són errors del programa.
És important tenir en compte aquesta distinció, ja que les assercions només funcionaran quan compilem en mode Test o Debug. Quan l'aplicació es compila i s'executa en mode Release les assercions no funcionen. Això es deu a que existeix una constant anomenada NDEBUG (no debug) que si està definida fa que les assercions es desactivin. Per defecte, quan compilem el nostre codi en mode Release aquesta constant es troba definida.
En aquest mòdul veurem el funcionament bàsic de les assercions, com podem incloure-les a la documentació i alguns exemples típics.
Assercions en C
Les assercions en C es controlen mitjançant l'acció assert, definida al fitxer de capçaleres assert.h. Per tant, caldrà incloure aquest fitxer per poder-les utilitzar. L'acció assert espera que se li passi una expressió com a paràmetre, que ha de ser certa. En cas que no ho sigui, la execució del programa finalitza i es mostra un error indicant el lloc on hi ha l'asserció que no s'ha complert.
Si voleu desactivar les assercions ho podeu fer (sempre i quant estigueu segurs que el vostre codi és correcte) declarant aquesta constant amb la següent línia de codi:
Una bona pràctica és indicar quines assercions es contemplen en un mètode donat. Això ho podem fer afegint la informació amb comentaris a la definició del mètode en el fitxer de capçaleres. Fixeu-vos en els exemples com s'ha documentat cada mètode en la seva implementació amb llenguatge C. Tingueu en compte que en aquests casos no utilitzem fitxers de capçalera, per tant s'han posat directament en la implementació.
Exemples
A continuació es mostren alguns exemples típics de l'ús de les assercions. Es mostra les precondicions i la seva traducció a asserts:
Exemple 03_01: control d'índexs
Un cas típic en el qual les assercions ens poden ajudar és a l'hora de verificar que els índexs estan en el rang correcte. Donada la definició d'una taula d'enters, fixeu-vos com s'ha definit les precondicions per a una funció getVal que ens retorna el valor a la posició indicada de la taula.
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(table.numElements >= 0);
assert(table.numElements <= MAX_ELEMENTS);
assert(pos >= 0);
assert(pos < table.numElements);
return table.elements[pos];
}
Exemple 03_02: paràmetres per referència
Un altre cas típic de l'ús de les assercions és quan rebem paràmetres per referència (ja sigui de sortida o d'entrada/sortida). Cal tenir en compte que aquests paràmetres són punters i, com a tals, pot donar-se el cas de que tinguin un valor NULL. Fixeu-vos en el següent exemple, en el qual rebem dos enters i retornem la suma d'aquests enters en un paràmetre de sortida.
{ 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;
}
Fixeu-vos que en aquest cas, com en llenguatge algorísmic el paràmetre c no és un punter, el que fem és indicar a la precondició que el valor que té assignat ha de pertànyer al tipus enter, o sigui, ser un enter vàlid. En el cas que el paràmetre fos una taula o un tipus estructurat, hauríem de fer el mateix, però el tipus canviaria. Per exemple, en cas que tinguéssim un mètode que prengués una taula de tipus tIntTable com a paràmetre d'entrada/sortida i en retorna la suma de tots els valors, la precondició seria:
{ Pre: table=TABLE ʌ TABLE.numElements>=0 ʌ TABLE.numElements<=MAX_ELEMENTS ʌ TABLE ∈ tIntTable }
Exemple 03_03: recursivitat
En aquest últim exemple veurem com aplicar les assercions a una funció recursiva. Recordem que una funció recursiva és aquella que es crida a sí mateixa. Un exemple típic és el càlcul del factorial. El factorial de n, o sigui, n! es pot calcular de la següent forma:
n! = n*(n-1)! = n*(n-1)*(n-2)! = n*(n-1)* ... *1
Podem definir aquesta funció de la següent 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);
}
}
Fixeu-vos que el que estem fent és assegurar que la variable de control de la recursivitat comença en un estat vàlid. En cas que ens passessin un valor negatiu de n, aquesta funció es cridaria de forma indefinida, fins que es quedés sense memòria i fes fallar l'aplicació.
Resum
En aquest mòdul hem vist con traduir les precondicions a llenguatge C, aplicant-les als nostres programes. En el cas de les postcondicions, el tractament seria exactament el mateix. També hem vist usos típics de les assercions en diferents exemples.