Perkontrakta programado

Perkontrakta programado estas paradigmo kiu permesas fari komputilajn programojn pli sekuraj dank'al aldono de reguloj.

Plej kutime la reguloj estas aldonataj sur la signaturo de funkcio aŭ proceduro. Temas pri:

• prekondiĉoj : indikas ke la parametroj kaj la ĉirkaŭaĵo devas respekti regulojn antaŭ ol oni vokas la funkcion
• postkondiĉoj : indikas ke la funkcio garantias ke la regulo estos vera post la alvoko de la funkcio
• nevarianto : indikas ke io estas ĉiam vera, do antaŭ kaj post la voko de la funkcio.

Ekzemple, se oni volas skribi funkcion por kalkuli logaritmon oni povus diri ke

• prekondiĉo estas, ke la parametro estas pli granda ol 0
• postkondiĉo povus esti ekzemple ke Eksponenta funkcio aplikata al la rezulto redonas la parametron.

La tradukilo decidas, kion oni faras de tiuj kondiĉoj:

• kelkaj kapablas kontroli evidentajn kondiĉojn dum tradukado (ekzemple se vi skribas x = -1; y = log(x), evidentiĝas ke la prekondiĉo ne estas vera)
• plimulto da tradukiloj simple aldonas kontrolon en la komenco kaj fino de la funkcio, kiuj kontrolas dum la programo funkcias, kaj se kondiĉo ne veras, interrompas la programon (sed kiam la programado estas finita oni demandas al tradukilo forviŝi la testojn por ke la programo laboru pli rapide).

Eiffel estas el la plej unuaj programlingvoj kiuj denaske permesas perkontraktan programadon. Tamen ekzistas ankaŭ bibliotekoj permesante programi per kontrakto kun plej kutimaj programlingvoj, ekzemple en Java. Programlingvoj kiel C kaj Java nun proponas la funkcion assert kun la sama celo, sed tio ne estas tute simila: assert povas aperi ie ajn en la funkcio. Tute male, kontraktoj estas deklarataj je la komenco de la funkcio, ili estas parto de ĝia signaturo kaj dank'al tio estas bonaj indikiloj por programistoj kiuj poste uzas la funkcion, por kompreni kiel uzi ĝin.