A „helyes” programokról

 A „helyes” program fogalma alatt azt értjük, hogy a program a specifikációjának megfelelően működik.
A későbbiekben - amikor egy program helyességének bizonyításával foglalkozunk - ezt a meghatározást úgy fogalmazhatjuk át, hogy „a program nem csinálja azt, amit nem szabad”.

A programozás valós világban léteznek olyan területek, ahol nem elégséges programjaink helyességéről pusztán teszteléssel meggyőződni. Ezek általában azok a területek, ahol az emberek által készített programok szorosan kapcsolódnak az emberek biztonságához.
Mivel ezek a programok sok ember együttes munkájaként születnek meg, a magas minőségű programok elkészítéseknél használt programozási valamint formális nyelvek szintaxisa (és természetesen annak ismerete) egyáltalán nem elhanyagolható részlet. (Egy ilyen szintaxis nem csak a gépelési, de még a tervezési hibák elkövetésének kockázatát is csökkenti.)
A biztonságkritikus programozás területén gyakran használnak formális módszereket melyek által bizonyítottan helyes kódot lehet előállítani, melyeket nem szükséges tesztelni.
Ilyen például a B módszertan is.
Egy kevésbé biztonságos, de lényegesen „olcsóbb” módszer az esetleges hibák minél korábbi elkerülésére a statikus kódanalízis. Számos szoftver létezik erre a célra, és egyes fordítók is rendelkeznek ezt támogató funkciókkal.
Néhány nyelvhez definiáltak résznyelveket is, melyek szűkítik például a programok dinamikus viselkedéséből eredő, nehezen tesztelhető problémák körét.
Akiket ez a terület érdekel, terjedelmes mennyiségű szakirodalmat találhatnak a témával kapcsolatban.
Akik a téma matematikai oldalával csak később szeretnének ismerkedni, az Ada programozási nyelv és a SPARK segítségével ezekbe a területekbe is betekintést nyerhetnek.

megjegyzés:

Az Ada 2012 által, a nyelvbe bevezetett fogalmak szorosan kapcsolódnak a fent említett témákhoz…