Tilman
67 lines
3.3 KiB
PHP
67 lines
3.3 KiB
PHP
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
|
|
<html>
|
|
<head>
|
|
<meta http-equiv="content-type" content="text/html; charset=ISO-8859-1">
|
|
<link rel="stylesheet" type="text/css" media="all" href="stylesheet.css">
|
|
<title>Verifikation und Validation</title>
|
|
</head>
|
|
<body>
|
|
<span id="menu"><a href="index.php">zurück zur Liste</a></span>
|
|
|
|
<div id="buttons">
|
|
<form action="edit.php" method="POST">
|
|
<input type="hidden" name="filename" value="<?php echo $_SERVER['SCRIPT_FILENAME']?>">
|
|
<p>
|
|
<input type="submit" value="Seite bearbeiten">
|
|
</p>
|
|
</form>
|
|
</div>
|
|
|
|
<h1>Verifikation und Validation</h1>
|
|
|
|
<b>Verifikation:</b> es wird bewiesen, dass die Spezifikation korrekt ist. Daraus folt die <b>partielle</b> Korrektheit eines Programm(abschnitt)s. Wird noch das Terminieren des Programm(abschnitt)s für jede Eingabe bewiesen, ist dieses/r <b>total</b> korrekt.<br> <br>
|
|
|
|
Um ein Programm zu verifizieren, zerlegt man es in seine Einzelschritte und beweist für jeden einzeln die partielle Korrektheit. Dafür gibt es einige Formeln (<b>Hoare Kalkül</b>):<br><br>
|
|
<font size="+1"><font face="Times New Roman">{P}</font></font> Vorbedingung<br>
|
|
<font size="+1"><font face="Times New Roman">{Q}</font></font> Nachbedingung<br>
|
|
<font size="+1"><font face="Times New Roman">S</font></font> Sequenz (der Teil des Programms, den man beweisen will.<br><br>
|
|
Zuweisungsaxiom: <font size="+1"><font face="Times New Roman">{P}x = e{P[e/x]}</font></font><br>
|
|
Alles was vorher für e galt, gilt nachher für x. Beispiel: <code>x = 5</code> (alles was für die 5 "gilt", gilt jetzt auch für x, z.B. dass man sie zu einer anderen Zahl addieren kann oder dass sie ungerade ist.)<br><br>
|
|
|
|
<table >
|
|
<tr>
|
|
<td align="right">Zuweisungsaxiom:</td>
|
|
<td><img src="zuweisung.gif" width="146" height="33" border="0" alt=""></td>
|
|
<td></td>
|
|
</tr>
|
|
<tr>
|
|
<td align="right">Sequenzregel:</td>
|
|
<td><img src="sequenz.gif" width="228" height="57" border="0" alt=""></td>
|
|
<td>Wenn man von P mittels S<sub>1</sub> zu R kommt, und von R mittels S<sub>2</sub> zu Q, so kommt man von P über die Ausführung von S<sub>1</sub> und s<sub>2</sub> zu Q.</td>
|
|
</tr>
|
|
<tr>
|
|
<td align="right">Bedingte Anweisung:</td>
|
|
<td><img src="bedingung.gif" width="329" height="60" border="0" alt=""></td>
|
|
<td>Wenn P und die Bedinung B erfüllt sind und man über S<sub>1</sub> zu Q gelangt, und wenn P erfüllt ist und B nicht und man über S<sub>2</sub> zu Q gelangt, so gilt {P} if (B) then S<sub>1</sub> else S<sub>2</sub> {Q}.
|
|
</tr>
|
|
<tr>
|
|
<td align="right">Schleife:</td>
|
|
<td><img src="while.gif" width="273" height="55" border="0" alt=""></td>
|
|
<td>Es wird eine geeignete Schleifeninvariante benötigt. Gilt diese und B ist erfüllt und ist die Invariante nach Durchlauf der Schleife unverändert und ist B nicht mehr erfüllt, ist die Schleife partiell korrekt. Für die totale Korrektheit muss noch die Termnierung bewiesen werden (siehe ALP II Skript)</td>
|
|
</tr>
|
|
</table>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<br><br><b>Validation:</b> es wird überprüft, ob der Algorithmus das bestehende Problem löst, also ob er tut, was er soll. Es gibt dafür keine formale Schreibweise.
|
|
<h2>Fragen</h2>
|
|
|
|
<h2>Anmerkungen</h2>
|
|
|
|
<h2>Links</h2>
|
|
|
|
</body>
|
|
</html> |