Software kan nooit de bedoeling van een algoritme achterhalen en kan dan ook niet zien of een (complex) algoritme correct is of niet.
Dat is waar. Echter waar het hier om gaat is om van een stukje code te bewijzen dat het aan bepaalde eigenschappen voldoet. Heel in het kort komt het op neer dat je een aantal pre-condities opstelt en een invariant. Vervolgens begin je bij de onderste regel van je code en werk je naar boven. Elke regel die je afwerkt levert een stuk formule in logica op.
Klinkt makkelijk, maar slechts enkele regels code leveren al 2 A4'tjes aan formule op. Helemaal bovenaan je code gekomen hou je 1 logica formule over. Nu moet je vanaf je precondities en invariant de implicatie bewijzen naar deze formule.
Er zijn voor CS mensen 3 problemen met deze methode:
1) Het opstellen van de invariant is vaak niet te doen. Bij tentamens over dit onderwerp is deze meestal dan ook gegeven.
2) Het is een
ENORM tijdrovend werk om die uiteindelijke formule op te stellen. Als je 1 dingetje in je code verander mag je weer overnieuw beginnen.
3) Het is meestal niet te doen om de uiteindelijke implicatie 'even' te bewijzen. Vaak levert alleen al dit bewijs weer minstens 1 A4'tje aan bewijs stappen op.
Het gevolg is dus dat bijna geen enkele developper dit leuk vindt. Bij Informatica is dit bv een van de meest gehate vakken. De enigste die het leuk vinden zijn van die mensen die eigenlijk wiskunde hadden willen studeren maar van hun familie Informatica moesten doen omdat daar meer toekomst in zat volgens die familie. (uitzonderingen daargelaten natuurlijk)
Als nu een tool stap 2) kan automatiseren, dan helpt dat al enorm. Hoewel ik absoluut geen expert ben in dit onderwerp geloof ik dat stap 3) ook in veek gevallen geautomatiseerd kan worden. Dan blijft alleen stap 1) over.
Formele testen komen dan veel eerder binnen het bereik van echte developpers. Het inhuren van een wiskundige voor dit soort werk blijft echter (IMHO) aan te raden.