Helyesség (számítástechnika)
 |
Ez a szócikk nem tünteti fel a független forrásokat, amelyeket felhasználtak a készítése során. Emiatt nem tudjuk közvetlenül ellenőrizni, hogy a szócikkben szereplő állítások helytállóak-e. Segíts megbízható forrásokat találni az állításokhoz! Lásd még: A Wikipédia nem az első közlés helye. |
Az elméleti számítástechnikában egy algoritmus helyessége azt jelenti, hogy az algoritmus egy specifikációhoz képest helyes. A funkcionális helyesség az algoritmus bemeneti és kimeneti viselkedésére utal. (például minden bemenet esetén az elvárt kimenetet adja).
Különbség van a részleges és a teljes helyesség között. A részleges helyesség azt jelenti, hogy egy visszaadott válasz helyes lesz, míg a teljes helyesség esetén ezen túl az algoritmus be is tud fejeződni. Mivel nincs általános megoldás a leállás problémájára, a teljes helyesség nem eldönthető. A befejezés igazolása egy olyan típusú matematikai bizonyítás, amely kritikus szerepet játszik a formális ellenőrzésben, mert egy algoritmus teljes helyessége a befejeződésétől függ.
Egy példa: sikeres keresést futtatni a természetes számok között annak érdekében, hogy tudunk-e példát találni egy jelenségre, tegyük fel, egy páratlan tökéletes számra. Egészen könnyű egy részlegesen helyes programot írni erre (a prímfelbontást használva minden természetes szám valódiosztóösszeg-függvényének kiszámítására). De ha azt mondanánk, hogy ez a program teljesen helyes, akkor olyan dolgot állítanánk, ami jelenleg nem ismert a számelméletben.
Egy bizonyításnak kötelezően matematikai bizonyításnak lennie, feltételezve, hogy mind az algoritmus és mind a specifikáció formálisan meg van adva. Nem várható el, hogy egy adott program helyességének igazolása érdekében az algoritmust egy adott számítógépen valósítsuk meg, hiszen olyan határokat is figyelembe kell venni, mint a gép memóriája.
A „mély eredmény” a bizonyításelméletben, a Curry–Howard-összefüggés, azt jelenti, hogy a konstruktív logika területén a funkcionális helyesség bizonyítása összefügg egy bizonyos programmal a lambda-kalkulusban. A bizonyítás ilyen módon történő átalakítását a program kibontásának nevezik.
A Hoare-logika egy olyan formális rendszer, amely szigorúan érvel a számítógépes programok helyességével kapcsolatban. Axiomatikus technikákat használ, hogy meghatározza a programozási nyelvnek a szemantikáját, és érveljen a programok helyességével kapcsolatban „Hoare-hármas”-ként ismert kijelentéseken keresztül.
A szoftvertesztelés bármely olyan tevékenység, amelynek a célja egy program vagy rendszer tulajdonságainak vagy képességeinek az értékelése. Ezen felül az is a célja, hogy meghatározza, eléri-e az elvárt eredményeket. Habár a szoftvertesztelés elengedhetetlen a megfelelő minőség eléréséhez, és gyakran alkalmazzák a programozók és tesztelők, még mindig művészetként van kezelve, a szoftver szabályainak korlátozott ismerete miatt. A szoftvertesztelés nehézsége a szoftverek összetettségéből fakad, nem tudunk teljesen tesztelni még egy közepesen összetett programot sem. A tesztelés sokkal több, mint egyszerűen a „debugging” (hibakeresés). A célja lehet a minőség biztosítása, igazolása, érvényesítése vagy a megbízhatóság megbecslése. A tesztelés általános metrikaként is használható. A helyesség és a megbízhatóság tesztelése két fő területe a tesztelésnek. A tesztelés célja ezen felül az egyensúly megtalálása a költségvetés, idő és minőség közt.
Fordítás[szerkesztés]
Ez a szócikk részben vagy egészben a Correctness (computer science) című angol Wikipédia-szócikk ezen változatának fordításán alapul. Az eredeti cikk szerkesztőit annak laptörténete sorolja fel. Ez a jelzés csupán a megfogalmazás eredetét és a szerzői jogokat jelzi, nem szolgál a cikkben szereplő információk forrásmegjelöléseként.