Programos funkcijų ir veiksmų aprašas.

Aprašymas to, ką programa daro arba turi daryti.
Gali būti neformali (nusakomoji) arba formali. Neformali skirta žmogui, kad jis žinotų, kokius rezultatus turi duoti programa ir iš to suprastų, kaip programuoti. Formali užrašoma šiam tikslui skirta specifikavimo kalba ir skirta kompiuteriui, kad jis galėtų patikrinti (verifikuoti) žmogaus parengtą programą arba pagal specifikaciją sintezuoti programą.
Yra įvairių specifikavimo kalbų ir metodų. Jie kol kas dar nėra tobuli ir programos dar mažai sintezuojamos arba verifikuojamos.

Formalizuotas objekto savybių, charakteristikų ir funkcijų aprašymas, dažniausiai pateikiamas dokumento forma.
Specifikacijos reikalingos kuriant naujas sistemas, programinę įrangą ir pan. Joms sudarytos įvairių metakalbų ir specializuotų žymenų sistemos.

Formalus programos teisingumo patikrinimas įrodant, kad programa yra teisinga.
Programa laikoma teisinga, jeigu ji daro tai, ko reikia, kas apibrėžta jos specifikacijoje. Tam, kad būtų galima formaliai (kompiuteriu) patikrinti programos teisingumą, reikia, kad ir jos specifikacija būtų formali. Parašyti formalią specifikaciją yra sudėtingas uždavinys. Verifikavimo programos taip pat sudėtingos. Todėl verifikuojamos tik labai atsakingos programos.
Programos taip pat tikrinamos testavimu. Testuoti paprasčiau. Tačiau testavimu tik randamos klaidos, bet neįrodoma, kad jų nėra. Verifikavimu įrodoma, kad klaidų nebėra.