Formale Beweise der Korrektheit

Wie ich schon berichtet habe, werde ich all meine Software auf ein neues Framework stellen, das ich selber programmiere. Bei dem Framework bin ich schon recht weit und es vereinfacht die Programmierung bisher schon extrem, obwohl es noch nicht fertig ist. Und das schönste: Der Code ist auf diese Art und Weise nahezu komplett wiederverwendbar dank der neuen Struktur. Details kommen wie versprochen später, muss erst mal selber ne kleine Doku schreiben, damit ich nichts vergess.

Sicher ist jetzt aber, dass ich nicht nur auf 100% Objektorientierung setze, sondern auch die formale Korrektheit jeder Klasse sicherstellen will. Hab mir deshalb extra mal Test-Frameworks aus der PHP-Szene angeschaut. Bekannt dürfte sicher PHPUnit sein. Da ich aber sowieso in PHP5 arbeite, kommt das PHPUnit2-Framework eher in Betracht. Als ich jedoch etwas beim “Forschen” war, bin ich noch auf Simple_Test gestoßen, welches auch nicht schlecht aussieht. PHPUnit2 hat aber sicher die bessere Dokumentation, weshalb wohl die Entscheidung hierzu gefallen ist.

Bin mal gespannt, wie aufwendig es sein wird, die Beweise immer durchzuführen. Aber so bin ich wenigstens auf der sichereren Seite und kann mit ruhigem Gewissen Änderungen durchführen. Denn wenn ich die Änderung abschließe, ist die Korrektheit bewiesen. Dann können nur noch nicht vorgesehene Probleme eintreten. Auch Seiteneffekte werden so auf jeden Fall sichtbar, die man evtl. nicht berücksichtigt hat (oder die gar nicht Absicht waren).

Da ich im neuen System aber auch mehr auf JavaScript setze (für AJAX, aber natürlich nur optional), muss für JavaScript natürlich auch eine Test-Umgebung her. Hierfür gibt es J3Unit. Hab ich mir aber bisher nicht genauer angeschaut, sieht aber sehr vielversprechend aus.

Schreibe einen Kommentar

Deine E-Mail-Adresse wird nicht veröffentlicht. Erforderliche Felder sind mit * markiert.