Formele methoden

Uit Wikipedia, de vrije encyclopedie
Ga naar: navigatie, zoeken

Een Formele methode is een op wiskunde en formele logica gebaseerde methode om software en hardware systemen 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.

Specificatie[bewerken]

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 het Backus-Naur-formalisme welke het mogelijk maakt de syntaxis van een taal (de grammatica) eenduidig te noteren.

Verificatie[bewerken]

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.

Formele methoden en notaties[bewerken]

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

Bronnen, noten en/of referenties