En programació informàtica, una precondició és una condició o predicat que sempre ha de ser cert just abans de l'execució d'alguna secció de codi o abans d'una operació en una especificació formal.
Si es viola una precondició, l'efecte de la secció de codi esdevé indefinit i, per tant, pot o no dur a terme la seva tasca prevista. Les precondicions que falten, són insuficients o no s'han demostrat formalment (o tenen un intent de demostració incorrecte), o no es comproven estàticament o dinàmicament, poden donar lloc a problemes de seguretat, especialment en llenguatges no segurs que no tenen un tipatge fort.
Sovint, les precondicions simplement s'inclouen a la documentació de la secció de codi afectada. De vegades, les precondicions es proven mitjançant guàrdies o assercions dins del mateix codi, i alguns llenguatges tenen construccions sintàctiques específiques per fer-ho.
Exemple La funció factorial només es defineix quan el seu paràmetre és un enter major o igual que zero. Per tant, una implementació de la funció factorial tindria una precondició que el seu paràmetre sigui un enter i que el paràmetre sigui major o igual que zero. Alternativament, es pot utilitzar el sistema de tipus del llenguatge per especificar que el paràmetre de la funció factorial és un nombre natural (enter sense signe), que es pot verificar formalment automàticament mitjançant un verificador de tipus de compilador.
A més, quan els tipus numèrics tenen un rang limitat (com passa a la majoria de llenguatges de programació), la precondició també ha d'especificar el valor màxim que pot tenir el paràmetre si no es vol que es produeixi un desbordament. (per exemple, si una implementació de factorial retorna el resultat en un enter sense signe de 64 bits, el paràmetre ha de ser inferior a 21 perquè factorial(21) és més gran que l'enter sense signe màxim que es pot emmagatzemar en 64 bits). Quan el llenguatge admet subtipus de rang (per exemple, Ada), aquestes restriccions poden ser verificades automàticament pel sistema de tipus. Les restriccions més complexes es poden verificar formalment de manera interactiva amb un assistent de prova.
En la programació orientada a objectes Les precondicions en el desenvolupament de programari orientat a objectes són una part essencial del disseny per contracte. El disseny per contracte també inclou nocions de postcondició i invariant de classe.
La precondició per a qualsevol rutina defineix qualsevol restricció sobre l'estat de l'objecte que sigui necessària per a una execució correcta. Des del punt de vista del desenvolupador del programa, això constitueix la part del contracte que correspon a qui crida la rutina. Qui crida, doncs, està obligat a assegurar-se que la precondició es compleix abans de cridar la rutina. La recompensa per l'esforç de qui crida s'expressa en la postcondició de la rutina anomenada.
Exemple d'Eiffel La rutina de l'exemple següent, escrita en Eiffel, pren com a argument un enter que ha de ser un valor vàlid per a una hora del dia, és a dir, de 0 a 23, ambdós inclosos. La precondició segueix la paraula clau require. Especifica que l'argument ha de ser més gran o igual que zero i més petit o igual que 23. L'etiqueta " valid_argument: " descriu aquesta clàusula de precondició i serveix per identificar-la en cas de violació d'una precondició 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
Precondicions i herència En presència d'herència, les rutines heretades per les classes descendents (subclasses) ho fan amb les seves precondicions en vigor. Això significa que qualsevol implementació o redefinició de rutines heretades també s'ha d'escriure per complir amb el seu contracte heretat. Les precondicions es poden modificar en rutines redefinides, però només es poden debilitar. És a dir, la rutina redefinida pot disminuir l'obligació del client, però no augmentar-la.
Referències
Categoria:Programari