program (Syntaks og semantik)

Program (Syntaks og semantik), Et programmeringssprogs syntaks er den korrekte notation af de enkelte bestanddele i et program, skrevet i vedkommende sprog, og semantikken er meningen med de forskellige syntaktiske konstruktioner. For at beskrive et sprogs syntaks og semantik må man benytte sig af et metasprog, dvs. et sprog, der kan beskrive et andet sprog. Det er vigtigt, at metasproget er så nøjagtigt og utvetydigt som overhovedet muligt, ellers risikerer man, at oversættere, der er beregnet for samme sprog, men udviklet af forskellige personer og måske til forskellige computere, er inkompatible og indeholder forskelle, der gør det vanskeligt at flytte programmer fra én computer til en anden. Ved fremkomsten af sproget Algol i 1960 benyttede man et formelt metasprog til syntaksbeskrivelse, backus-naur-form (BNF), der senere har været forbillede for syntaksbeskrivelse af programmeringssprog (se John W. Backus). Et andet og beslægtet metasprog er syntaksdiagrammer, der er grafiske og derfor velegnede til at skabe overblik for en menneskelig læser. Begge metasprog har en sådan grad af fuldkommenhed, at der ikke kan være tvivl om, hvilke sprogkonstruktioner der er legale, og hvilke der ikke er det.

Formel beskrivelse af semantikken for et programmeringssprog har derimod vist sig at være et vanskeligere problem. Man falder ofte tilbage på anvendelsen af naturligt sprog, oftest engelsk, når semantikken i et programmeringssprog skal defineres. Ulempen er, at almindelig prosa er tvetydig, så forskellige læsere ofte får afvigende opfattelser af, hvordan en tekst skal forstås. Der findes dog forslag til formelle metasprog også på semantikkens område. Én mulighed er at bruge prædikatslogik som metasprog og anvende logiske slutningsregler til at udlede virkningen af sætninger i det programmeringssprog, hvis semantik skal beskrives. Meningen med en sætning eller en gruppe af sætninger beskrives ved at opstille regler for, hvordan et logisk udsagn, der gælder, før sætningen bliver udført, kan transformeres til et andet logisk udsagn, der gælder efter udførelse af sætningen. Metoden bruges mest til verificering af programmer og til ræsonnementer over virkningen af konkrete programmer.