Formele methoden

Een formele methode is een op wiskunde en formele logica gebaseerde methode om software en hardwaresystemen te specificeren en te verifiëren. Het doel van (het gebruik van) formele methoden is:

• het eenduidig en volledig specificeren van de werking van een te ontwerpen programma of algoritme, en
• het leveren van een systematisch en sluitend bewijs van de correctheid van een programma of algoritme.

Met formele methoden kan de werking van een te ontwerpen systeem of algoritme beschreven worden met behulp van wiskundige en logische notaties. Deze zijn, in tegenstelling tot beschrijvingen in spreektaal, eenduidig en methodisch verifieerbaar. Een voorbeeld hiervan is BNF, dat het mogelijk maakt de syntaxis van een taal (de grammatica) eenduidig te noteren.

De formele specificatie kan vervolgens gebruikt worden om de correctheid van de specificatie te bewijzen. Indien succesvol, is hiermee ook de correctheid van de implementatie aangetoond als deze inderdaad voldoet aan de opgestelde specificaties.

Vanwege de aard van formele methoden is het (tot op zekere hoogte) mogelijk dit proces te automatiseren.

Er zijn een aantal formele methoden en notaties beschikbaar, zoals:

• BNF
• hoarelogica
• petrinetten