En programació informàtica, una postcondició és una condició o predicat que sempre ha de ser cert just després de l'execució d'alguna secció de codi o després d'una operació en una especificació formal. Les postcondicions de vegades es proven mitjançant assercions dins del mateix codi. Sovint, les postcondicions simplement s'inclouen a la documentació de la secció de codi afectada.
Per exemple: el resultat d'un factorial sempre és un enter i més gran o igual que 1. Per tant, un programa que calcula el factorial d'un nombre d'entrada tindria postcondicions que el resultat després del càlcul sigui un enter i que sigui més gran o igual que 1. Un altre exemple: un programa que calcula l'arrel quadrada d'un nombre d'entrada podria tenir les postcondicions que el resultat sigui un nombre i que el seu quadrat sigui igual a l'entrada.
Postcondicions en la programació orientada a objectes
En alguns enfocaments de disseny de programari, les postcondicions, juntament amb les precondicions i els invariants de classe, són components del mètode de construcció de programari (disseny per contracte).
La postcondició per a qualsevol rutina és una declaració de les propietats que es garanteixen un cop finalitzada l'execució de la rutina. Pel que fa al contracte de la rutina, la postcondició ofereix la garantia als possibles invocadors que, en els casos en què la rutina es crida en un estat en què es compleix la seva precondició, les propietats declarades per la postcondició estan assegurades.
Exemple d'Eiffel El següent exemple, escrit en Eiffel, estableix el valor d'un atribut de classe hour basat en un argument proporcionat pel qui truca, a_hour. La postcondició segueix la paraula clau ensure. En aquest exemple, la postcondició garanteix, en els casos en què la precondició es compleix (és a dir, quan a_hour representa una hora vàlida del dia), que després de l'execució de set_hour, l'atribut de classe hour tindrà el mateix valor que a_hour. L'etiqueta " hour_set: " descriu aquesta clàusula de postcondició i serveix per identificar-la en cas d'una violació de la postcondició en temps d'execució. set_hour (a_hour: INTEGER) -- Set `hour' to `a_hour' require valid_argument: 0 <= a_hour and a_hour <= 23 do hour := a_hour ensure hour_set: hour = a_hour end
Postcondicions i herència En presència d'herència, les rutines heretades per les classes descendents (subclasses) ho fan amb els seus contractes, és a dir, les seves precondicions i postcondicions, en vigor. Això significa que qualsevol implementació o redefinició de rutines heretades també s'ha d'escriure per complir amb els seus contractes heretats. Les postcondicions es poden modificar en rutines redefinides, però només es poden reforçar. És a dir, la rutina redefinida pot augmentar els beneficis que proporciona al client, però no disminuir aquests beneficis.
Referències
Categoria:Programari