Zum Inhalt springen

Hoare-Kalkül

aus Wikipedia, der freien Enzyklopädie

Der Hoare-Kalkül (auch Hoare-Logik oder Floyd-Hoare-Kalkül) ist ein formales System, um die Korrektheit von Programmen nachzuweisen. Er wurde von dem britischen Informatiker C. A. R. Hoare entwickelt und später von ihm und anderen Wissenschaftlern verbessert. Der Hoare-Kalkül wurde 1969 in einem Artikel mit dem Titel An axiomatic basis for computer programming veröffentlicht.<ref name="Primärquelle">Charles Antony Richard Hoare: <templatestyles src="Webarchiv/styles.css" />{{#if:20160304013345 

      | {{#ifeq: 20160304013345 | *
    | Vorlage:Webarchiv/Wartung/Stern{{#if: An Axiomatic Basis for Computer Programming | {{#invoke:WLink|getEscapedTitle|An Axiomatic Basis for Computer Programming}} | {{#invoke:Webarchiv|getdomain|http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf}} }} (Archivversionen)
    | {{#iferror: {{#time: j. F Y|20160304013345}}
         | {{#if:  || }}Vorlage:Webarchiv/Wartung/DatumDer Wert des Parameters {{#if: wayback | wayback | Datum }} muss ein gültiger Zeitstempel der Form YYYYMMDDHHMMSS sein!
         | {{#if: An Axiomatic Basis for Computer Programming | {{#invoke:WLink|getEscapedTitle|An Axiomatic Basis for Computer Programming}} | {{#invoke:Webarchiv|getdomain|http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf}} }} {{#ifeq:  | [] | [ | ( }}Memento{{#if: {{#if:  | {{{archiv-bot}}} |  }} |  des Vorlage:Referrer }} vom {{#time: j. F Y|20160304013345}} im Internet Archive{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
      }}
  }}
      | {{#if:
          | {{#iferror: {{#time: j. F Y|{{{webciteID}}}}}
    | {{#switch: {{#invoke:Str|len|{{{webciteID}}}}}
       | 16= {{#if: An Axiomatic Basis for Computer Programming | {{#invoke:WLink|getEscapedTitle|An Axiomatic Basis for Computer Programming}} | {{#invoke:Webarchiv|getdomain|http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf}} }} {{#ifeq:  | [] | [ | ( }}Memento{{#if: {{#if:  | {{{archiv-bot}}} |  }} |  des Vorlage:Referrer }} vom {{#time: j. F Y| 19700101000000 + {{#expr: floor {{#expr: {{#invoke:Str|sub|{{{webciteID}}}|1|10}}/86400}} }} days}} auf WebCite{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
       | 9 = {{#if: An Axiomatic Basis for Computer Programming | {{#invoke:WLink|getEscapedTitle|An Axiomatic Basis for Computer Programming}} | {{#invoke:Webarchiv|getdomain|http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf}} }} {{#ifeq:  | [] | [ | ( }}Memento{{#if: {{#if:  | {{{archiv-bot}}} |  }} |  des Vorlage:Referrer}} vom {{#time: j. F Y| 19700101000000 + {{#expr: floor {{#expr: {{#invoke:Str|sub|{{#invoke:Expr|base62|{{{webciteID}}}}}|1|10}}/86400}} }} days}} auf WebCite{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
       | #default= Der Wert des Parameters {{#if: webciteID | webciteID | ID }} muss entweder ein Zeitstempel der Form YYYYMMDDHHMMSS oder ein Schüsselwert mit 9 Zeichen oder eine 16-stellige Zahl sein!Vorlage:Webarchiv/Wartung/webcitation{{#if:  || }}
      }}
    | c|{{{webciteID}}}}} {{#if: An Axiomatic Basis for Computer Programming | {{#invoke:WLink|getEscapedTitle|An Axiomatic Basis for Computer Programming}} | {{#invoke:Webarchiv|getdomain|http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf}} }} (Memento{{#if: {{#if:  | {{{archiv-bot}}} |  }} |  des Vorlage:Referrer}} vom {{#time: j. F Y|{{{webciteID}}}}} auf WebCite{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
  }}
          | {{#if: 
              | Vorlage:Webarchiv/Today
              | {{#if:
                      | Vorlage:Webarchiv/Generisch
                      | {{#if: An Axiomatic Basis for Computer Programming | {{#invoke:WLink|getEscapedTitle|An Axiomatic Basis for Computer Programming}} | {{#invoke:Webarchiv|getdomain|http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf}} }}  
                 }}}}}}}}{{#if:
    | Vorlage:Webarchiv/archiv-bot
  }}{{#invoke:TemplatePar|check
     |all      = url=
     |opt      = text= wayback= webciteID= archive-is= archive-today= archiv-url= archiv-datum= ()= archiv-bot= format= original=
     |cat      = Wikipedia:Vorlagenfehler/Vorlage:Webarchiv
     |errNS    = 0
     |template = Vorlage:Webarchiv
     |format   = *
     |preview  = 1
  }}{{#ifexpr: {{#if:20160304013345|1|0}}{{#if:|+1}}{{#if:|+1}}{{#if:|+1}}{{#if:|+1}} <> 1
    | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Genau einer der Parameter 'wayback', 'webciteID', 'archive-today', 'archive-is' oder 'archiv-url' muss angegeben werden.|1}}
  }}{{#if: 
    | {{#switch: {{#invoke:Webarchiv|getdomain|{{{archiv-url}}}}}
        | web.archive.org = 
          {{#if:  || }}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Im Parameter 'archiv-url' wurde URL von Internet Archive erkannt, bitte Parameter 'wayback' benutzen.|1}} 
        | webcitation.org = 
          {{#if:  || }}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Im Parameter 'archiv-url' wurde URL von WebCite erkannt, bitte Parameter 'webciteID' benutzen.|1}} 
        | archive.today |archive.is |archive.ph |archive.fo |archive.li |archive.md |archive.vn = 
          {{#if:  || }}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Im Parameter 'archiv-url' wurde URL von archive.today erkannt, bitte Parameter 'archive-today' benutzen.|1}}
      }}{{#if: 
         | {{#iferror: {{#iferror:{{#invoke:Vorlage:FormatDate|Execute}}|}}
             | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Der Wert des Parameter 'archiv-datum' ist ungültig oder hat ein ungültiges Format.|1}}
          |  }} 
         | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Der Pflichtparameter 'archiv-datum' wurde nicht angegeben.|1}}
      }}
    | {{#if: 
         | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Der Parameter 'archiv-datum' ist nur in Verbindung mit 'archiv-url' angebbar.|1}}
      }}
  }}{{#if:{{#invoke:URLutil|isHostPathResource|http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf}}
    || {{#if:  || }}
  }}{{#if: An Axiomatic Basis for Computer Programming
    | {{#if: {{#invoke:WLink|isBracketedLink|An Axiomatic Basis for Computer Programming}}
        | {{#if:  || }}
      }}
    | {{#if:  || }}Vorlage:Webarchiv/Wartung/Linktext_fehlt
  }}{{#switch: 
    |addlarchives|addlpages= {{#if:  || }}{{#if: 1 |Vorlage:Webarchiv/Wartung/Parameter}}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: enWP-Wert im Parameter 'format'.|1}}
  }}{{#ifeq: {{#invoke:Str|find|http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf%7Carchiv}} |-1
    || {{#ifeq: {{#invoke:Str|find|{{#invoke:Str|cropleft|http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf%7C4}}%7Chttp}} |-1
         || {{#switch: {{#invoke:Webarchiv|getdomain|http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf }}
              | abendblatt.de | daserste.ndr.de | inarchive.com | webcitation.org = 
              | #default = {{#if:  || }}{{#if: 1 |Vorlage:Webarchiv/Wartung/URL}}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Archiv-URL im Parameter 'url' anstatt URL der Originalquelle. Entferne den vor der Original-URL stehenden Mementobestandteil und setze den Archivierungszeitstempel in den Parameter 'wayback', 'webciteID', 'archive.today' oder 'archive-is' ein, sofern nicht bereits befüllt.|1}}
            }} 
       }}
  }} (PDF; 659 kB). In: Communications of the ACM. Bd. 12, Nr. 10, 1969, S. 576–585, doi:10.1145/363235.363259.</ref>

Der Zweck des Systems ist es, eine Menge von logischen Regeln zu liefern, die es erlauben, Aussagen über die Korrektheit von imperativen Computer-Programmen zu treffen und sich dabei der mathematischen Logik zu bedienen. Hoare knüpft an frühere Beiträge von Robert Floyd an, der ein ähnliches System für Flussdiagramme veröffentlichte.<ref name="Floyd">{{#invoke:Vorlage:Literatur|f}}</ref> Im Gegensatz zum floydschen Verfahren, bei dem Ausführungspfade interpretiert werden, arbeitet der Hoare-Kalkül mit dem Quellcode.<ref name="Software-Qualität">{{#invoke:Vorlage:Literatur|f}}</ref>

Alternativ kann auch der wp-Kalkül benutzt werden, bei dem im Gegensatz zum Hoare-Kalkül eine Rückwärtsanalyse stattfindet.

Hoare-Tripel

Das zentrale Element des Hoare-Kalküls ist das Hoare-Tripel, das beschreibt, wie ein Programmteil den Zustand einer Berechnung verändert:

<math>\{P\}\;S\;\{Q\}.</math>

Dabei sind <math>P</math> und <math>Q</math> Zusicherungen (englisch assertions), <math>S</math> ist ein Programmsegment. <math>P</math> ist die Vorbedingung (englisch precondition) und <math>Q</math> die Nachbedingung (englisch postcondition). Wenn die Vorbedingung zutrifft, gilt nach der Ausführung des Programmsegments die Nachbedingung. Zusicherungen sind Formeln der Prädikatenlogik.<ref name="Primärquelle" />

Ein Tripel kann auf folgende Weise verstanden werden: Falls <math>P</math> für den Programmzustand vor der Ausführung von <math>S</math> gilt, dann gilt <math>Q</math> danach. Falls <math>S</math> nicht terminiert, dann gibt es kein danach, also kann in diesem Fall <math>Q</math> jede beliebige Aussage sein. Tatsächlich kann man für <math>Q</math> die Aussage falsch wählen, um auszudrücken, dass <math>S</math> nicht terminiert. Man spricht hier von partieller Korrektheit. Falls <math>S</math> immer terminiert und danach <math>Q</math> wahr ist, spricht man von totaler Korrektheit. Die Terminierung muss unabhängig bewiesen werden.

Falls keine Vorbedingung existiert, schreibt man:<ref name="Software-Qualität" />

<math>\{true\}\;S\;\{Q\}.</math>

Partielle Korrektheit

Der Hoare-Kalkül besteht aus Axiomen und Ableitungsregeln für alle Konstrukte einer einfachen imperativen Programmiersprache:

Axiom der leeren Anweisung

Wenn ein Programmsegment <math>S</math> keine Variablen verändert, so ändern sich auch die Zusicherungen nicht, es gilt also Nachbedingung gleich Vorbedingung:

<math> \frac {} {\{P\} S \{P\}}</math>

Zuweisungsaxiom

Das Zuweisungsaxiom besagt, dass nach einer Zuweisung jede Aussage für die Variable gilt, welche vorher für die rechte Seite der Zuweisung galt:

<math> \frac {} {\{P[E/x]\}\ x:=E \ \{P\}}.</math>

<math>P[E/x]</math> ist die Aussage, die dadurch entsteht, dass man in <math>P</math> jedes freie Vorkommen von <math>x</math> durch <math>E</math> ersetzt.

Genau genommen ist das Zuweisungsaxiom kein einzelnes Axiom, sondern ein Schema für eine unendliche Menge von Axiomen, denn <math>x</math>, <math>E</math> und <math>P</math> können jede mögliche Form annehmen, und <math>P[E/x]</math> kann daraus konstruiert werden.

Ein Beispiel für ein durch das Zuweisungsaxiom beschriebenes Tripel ist:

<math>\{ x + 1 = 43\} \ y:=x + 1\ \{y =43 \}.</math>

Kompositions- oder Sequenzregel

Um sequentielle Programme zu analysieren, können die einzelnen Tripel nach folgender Regel verknüpft werden:

<math> \frac {\{P\}\ S\ \{R\}\ , \ \{R\}\ T\ \{Q\} } {\{P\}\ S;T\ \{Q\}} </math>

Diese Regel kann auf folgende Weise angewendet werden: Wenn die über dem Strich stehenden Aussagen bewiesen worden sind, kann die unter dem Strich stehende Aussage auch als bewiesen angesehen werden.

Betrachtet man zum Beispiel die folgenden beiden Aussagen, die aus dem Zuweisungsaxiom folgen

<math>\{ x + 1 = 43\} \ y:=x + 1\ \{y =43 \}</math>

und

<math>\{ y = 43\} \ z:=y\ \{z =43 \}</math>

kann man die folgende Aussage daraus folgern:

<math>\{ x + 1 = 43\} \ y:=x + 1; z:= y\ \{z =43 \}.</math>

Auswahlregel (if-then-else-Regel)

Es gilt folgende Regel für Auswahlkonstrukte mit 2 Auswahlmöglichkeiten:<ref name="Software-Qualität" />

<math>\frac { \{P \wedge B\}\ S\ \{Q\}\ ,\ \{P \wedge \neg B \}\ T\ \{Q\} } { \{P\}\ \mathrm{if}\ B\ \mathrm{then}\ S\ \mathrm{else}\ T\ \{Q\} }</math>

Die Regel beweist also sowohl den if-Zweig, als auch den else-Zweig. Hat eine if-Abfrage keinen else-Zweig, so verwendet man eine leicht modifizierte Version dieser Regel:

<math>\frac { \{P \wedge B\}\ S\ \{Q\}\ ,\ P \wedge \neg B \Rightarrow Q } { \{P\}\ \mathrm{if}\ B\ \mathrm{then}\ S\ \{Q\} }</math>

Iterationsregel (while-Regel)

<math>\frac { \{I \wedge B \}\ S\ \{I\} } { \{I \}\ \mathrm{while}\ B\ \mathrm{do}\ S\ \mathrm{done}\ \{I \wedge \neg B \} }</math>

Hierbei wird <math>I</math> als die Schleifeninvariante bezeichnet, die sowohl vor, während und nach Ausführung der Schleife gültig ist. Eine Invariante muss manuell ermittelt werden.

Konsequenzregel (Rule of Consequence)

<math>\frac { P \Rightarrow\ P^\prime ,\ \lbrace P^\prime \rbrace\ S\ \lbrace Q^\prime \rbrace\ ,\ Q^\prime \Rightarrow\ Q } { \lbrace P\rbrace\ S\ \lbrace Q\rbrace }</math>

Die Konsequenzregel erlaubt es, die Vorbedingung zu verstärken und die Nachbedingung abzuschwächen und so die Anwendung anderer Beweisregeln zu ermöglichen. Insbesondere kann man auch die Vor- oder Nachbedingung durch eine äquivalente logische Formel ersetzen. Beispiel:

<math>\lbrace true \rbrace\ x := 0 \ \lbrace x \geq 0\rbrace\ </math> ist partiell korrekt, denn
<math>\frac { true \Rightarrow 0 = 0, \lbrace 0 = 0 \rbrace \ x := 0 \ \lbrace x = 0 \rbrace , \ x = 0 \Rightarrow x \geq 0 } { \lbrace true \rbrace \ x := 0\ \lbrace x \geq 0 \rbrace }.</math>

Totale Korrektheit

Wie oben erläutert eignet sich der beschriebene Kalkül nur für den Beweis der partiellen Korrektheit. Zum Beweis der totalen Korrektheit muss die while-Regel durch eine Schleifenvariante erweitert werden. Dabei handelt es sich um eine Funktion oder eine Variable <math>t</math>, die eine Zahl mit einem Anfangswert <math>z</math> darstellt. Es muss nun nachgewiesen werden, dass <math>t</math> in jedem Schleifendurchlauf verringert wird, und dass die Schleife ab einem bestimmten, verringerten Wert terminiert.<ref name="Floyd" />

Iterationsregel für totale Korrektheit

<math>\frac { \{I \wedge B ~\wedge ~t = z \}\ S\ \{I ~\wedge ~t < z \},~I \Rightarrow t \geq 0} { \{I \}\ \mathrm{while}\ B\ \mathrm{do}\ S\ \mathrm{done}\ \{I \wedge \neg B \} }</math>

Hierbei ist <math>t</math> ein Term, <math>I</math> die Schleifeninvariante – also das, was in jedem Schleifendurchlauf gilt – und <math>z</math> eine Variable, die in <math>B</math>, <math>t</math>, <math>S</math> und <math>I</math> nicht frei vorkommt. Sie dient dazu, den Wert des Terms vor der Schleife mit dem nach der Schleife zu vergleichen. Die Bedingung <math>I \Rightarrow t \geq 0</math> stellt sicher, dass <math>t</math> nicht negativ wird. Die Idee hinter der Regel ist, dass, wenn <math>t</math> mit jedem Schleifendurchlauf abnimmt, aber nie kleiner als Null wird, die Schleife irgendwann enden muss. <math>t</math> muss dabei aus einer fundierten Menge sein.

Bewertung

Mit dem Hoare-Kalkül und einer formalen Spezifikation ist es möglich, ein Programm oder Teile eines Programms auf Korrektheit zu prüfen. Er liefert damit eines der wenigen Verfahren, die tatsächlich Korrektheit nachweisen und nicht nur Anwesenheit von Fehlern feststellen können. Allerdings müssen die Ergebnisse einer Analyse mit dem Hoare-Kalkül mit Vorsicht genossen werden:

  • Ist die Spezifikation fehlerhaft, können zwar die Ergebnisse der Analyse korrekt sein, allerdings gegenüber einer falschen Spezifikation.
  • Mit dem Hoare-Kalkül werden keine Fehler gefunden, die durch Fehler in der Spezifikation der Programmiersprache selbst oder durch einen fehlerhaften Compiler entstehen.<ref name="Software-Qualität" />
  • Der Hoare-Kalkül stößt bei großen Softwaresystemen, speziell mit globalen Variablen und Rekursion schnell an seine Grenzen.<ref>{{#invoke:Vorlage:Literatur|f}}</ref>
  • Zur Verifikation müssen Axiome der Computerarithmetik benutzt werden, die Besonderheiten, wie die Beschränktheit der mit Integer-Typen repräsentierbaren ganzen Zahlen und die Ungenauigkeit von Gleitkommazahlen, berücksichtigen.<ref name="Software-Qualität" />

Literatur

  • Hoare: An axiomatic basis for computer programming, Communications of the ACM, Band 12, 1969, S. 576–580
  • Robert D. Tennent: Specifying Software. A Hands-on Introduction. Cambridge University Press, Cambridge u. a. 2002, ISBN 0-521-00401-2 (ein aktuelles Lehrbuch mit einer Einführung in die Hoare-Logik), Beschreibung und „Errors and Corrections“.
  • Krzysztof R. Apt, Ernst-Rüdiger Olderog: Fifty years of Hoare’s logic. In: Formal Aspects of Computing, Band 31, Nr. 6, Dezember 2019, S. 751–807. doi:10.1007/s00165-019-00501-3.

Weblinks

  • Programmverifikation mit zahlreichen Beispielen und Übungsaufgaben
  • Das Project Bali hat Regeln nach Art des Hoare-Kalküls für ein Subset von Java aufgestellt, zur Benutzung mit dem Theorembeweiser Isabelle
  • <templatestyles src="Webarchiv/styles.css" />{{#if:20120131115328
      | {{#ifeq: 20120131115328 | *
    | Vorlage:Webarchiv/Wartung/Stern{{#if: Hoare Tutorial | {{#invoke:WLink|getEscapedTitle|Hoare Tutorial}} | {{#invoke:Webarchiv|getdomain|http://wwwswt.informatik.uni-rostock.de/deutsch/Mitarbeiter/michael/lehre/pt_2001/Hoare_akt_008.pdf}} }} (Archivversionen)
    | {{#iferror: {{#time: j. F Y|20120131115328}}
         | {{#if:  || }}Vorlage:Webarchiv/Wartung/DatumDer Wert des Parameters {{#if: wayback | wayback | Datum }} muss ein gültiger Zeitstempel der Form YYYYMMDDHHMMSS sein!
         | {{#if: Hoare Tutorial | {{#invoke:WLink|getEscapedTitle|Hoare Tutorial}} | {{#invoke:Webarchiv|getdomain|http://wwwswt.informatik.uni-rostock.de/deutsch/Mitarbeiter/michael/lehre/pt_2001/Hoare_akt_008.pdf}} }} {{#ifeq:  | [] | [ | ( }}Memento{{#if: {{#if:  | {{{archiv-bot}}} |  }} |  des Vorlage:Referrer }} vom {{#time: j. F Y|20120131115328}} im Internet Archive{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
      }}
  }}
      | {{#if:
          | {{#iferror: {{#time: j. F Y|{{{webciteID}}}}}
    | {{#switch: {{#invoke:Str|len|{{{webciteID}}}}}
       | 16= {{#if: Hoare Tutorial | {{#invoke:WLink|getEscapedTitle|Hoare Tutorial}} | {{#invoke:Webarchiv|getdomain|http://wwwswt.informatik.uni-rostock.de/deutsch/Mitarbeiter/michael/lehre/pt_2001/Hoare_akt_008.pdf}} }} {{#ifeq:  | [] | [ | ( }}Memento{{#if: {{#if:  | {{{archiv-bot}}} |  }} |  des Vorlage:Referrer }} vom {{#time: j. F Y| 19700101000000 + {{#expr: floor {{#expr: {{#invoke:Str|sub|{{{webciteID}}}|1|10}}/86400}} }} days}} auf WebCite{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
       | 9 = {{#if: Hoare Tutorial | {{#invoke:WLink|getEscapedTitle|Hoare Tutorial}} | {{#invoke:Webarchiv|getdomain|http://wwwswt.informatik.uni-rostock.de/deutsch/Mitarbeiter/michael/lehre/pt_2001/Hoare_akt_008.pdf}} }} {{#ifeq:  | [] | [ | ( }}Memento{{#if: {{#if:  | {{{archiv-bot}}} |  }} |  des Vorlage:Referrer}} vom {{#time: j. F Y| 19700101000000 + {{#expr: floor {{#expr: {{#invoke:Str|sub|{{#invoke:Expr|base62|{{{webciteID}}}}}|1|10}}/86400}} }} days}} auf WebCite{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
       | #default= Der Wert des Parameters {{#if: webciteID | webciteID | ID }} muss entweder ein Zeitstempel der Form YYYYMMDDHHMMSS oder ein Schüsselwert mit 9 Zeichen oder eine 16-stellige Zahl sein!Vorlage:Webarchiv/Wartung/webcitation{{#if:  || }}
      }}
    | c|{{{webciteID}}}}} {{#if: Hoare Tutorial | {{#invoke:WLink|getEscapedTitle|Hoare Tutorial}} | {{#invoke:Webarchiv|getdomain|http://wwwswt.informatik.uni-rostock.de/deutsch/Mitarbeiter/michael/lehre/pt_2001/Hoare_akt_008.pdf}} }} (Memento{{#if: {{#if:  | {{{archiv-bot}}} |  }} |  des Vorlage:Referrer}} vom {{#time: j. F Y|{{{webciteID}}}}} auf WebCite{{#if:  | ;  }}{{#ifeq:  | [] | ] | ) }}
  }}
          | {{#if: 
              | Vorlage:Webarchiv/Today
              | {{#if:
                      | Vorlage:Webarchiv/Generisch
                      | {{#if: Hoare Tutorial | {{#invoke:WLink|getEscapedTitle|Hoare Tutorial}} | {{#invoke:Webarchiv|getdomain|http://wwwswt.informatik.uni-rostock.de/deutsch/Mitarbeiter/michael/lehre/pt_2001/Hoare_akt_008.pdf}} }}  
                 }}}}}}}}{{#if:
    | Vorlage:Webarchiv/archiv-bot
  }}{{#invoke:TemplatePar|check
     |all      = url=
     |opt      = text= wayback= webciteID= archive-is= archive-today= archiv-url= archiv-datum= ()= archiv-bot= format= original=
     |cat      = Wikipedia:Vorlagenfehler/Vorlage:Webarchiv
     |errNS    = 0
     |template = Vorlage:Webarchiv
     |format   = *
     |preview  = 1
  }}{{#ifexpr: {{#if:20120131115328|1|0}}{{#if:|+1}}{{#if:|+1}}{{#if:|+1}}{{#if:|+1}} <> 1
    | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Genau einer der Parameter 'wayback', 'webciteID', 'archive-today', 'archive-is' oder 'archiv-url' muss angegeben werden.|1}}
  }}{{#if: 
    | {{#switch: {{#invoke:Webarchiv|getdomain|{{{archiv-url}}}}}
        | web.archive.org = 
          {{#if:  || }}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Im Parameter 'archiv-url' wurde URL von Internet Archive erkannt, bitte Parameter 'wayback' benutzen.|1}} 
        | webcitation.org = 
          {{#if:  || }}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Im Parameter 'archiv-url' wurde URL von WebCite erkannt, bitte Parameter 'webciteID' benutzen.|1}} 
        | archive.today |archive.is |archive.ph |archive.fo |archive.li |archive.md |archive.vn = 
          {{#if:  || }}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Im Parameter 'archiv-url' wurde URL von archive.today erkannt, bitte Parameter 'archive-today' benutzen.|1}}
      }}{{#if: 
         | {{#iferror: {{#iferror:{{#invoke:Vorlage:FormatDate|Execute}}|}}
             | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Der Wert des Parameter 'archiv-datum' ist ungültig oder hat ein ungültiges Format.|1}}
          |  }} 
         | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Der Pflichtparameter 'archiv-datum' wurde nicht angegeben.|1}}
      }}
    | {{#if: 
         | {{#if:  || }}Vorlage:Webarchiv/Wartung/Parameter{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Der Parameter 'archiv-datum' ist nur in Verbindung mit 'archiv-url' angebbar.|1}}
      }}
  }}{{#if:{{#invoke:URLutil|isHostPathResource|http://wwwswt.informatik.uni-rostock.de/deutsch/Mitarbeiter/michael/lehre/pt_2001/Hoare_akt_008.pdf}}
    || {{#if:  || }}
  }}{{#if: Hoare Tutorial
    | {{#if: {{#invoke:WLink|isBracketedLink|Hoare Tutorial}}
        | {{#if:  || }}
      }}
    | {{#if:  || }}Vorlage:Webarchiv/Wartung/Linktext_fehlt
  }}{{#switch: 
    |addlarchives|addlpages= {{#if:  || }}{{#if: 1 |Vorlage:Webarchiv/Wartung/Parameter}}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: enWP-Wert im Parameter 'format'.|1}}
  }}{{#ifeq: {{#invoke:Str|find|http://wwwswt.informatik.uni-rostock.de/deutsch/Mitarbeiter/michael/lehre/pt_2001/Hoare_akt_008.pdf%7Carchiv}} |-1
    || {{#ifeq: {{#invoke:Str|find|{{#invoke:Str|cropleft|http://wwwswt.informatik.uni-rostock.de/deutsch/Mitarbeiter/michael/lehre/pt_2001/Hoare_akt_008.pdf%7C4}}%7Chttp}} |-1
         || {{#switch: {{#invoke:Webarchiv|getdomain|http://wwwswt.informatik.uni-rostock.de/deutsch/Mitarbeiter/michael/lehre/pt_2001/Hoare_akt_008.pdf }}
              | abendblatt.de | daserste.ndr.de | inarchive.com | webcitation.org = 
              | #default = {{#if:  || }}{{#if: 1 |Vorlage:Webarchiv/Wartung/URL}}{{#invoke:TemplUtl|failure| Fehler bei Vorlage:Webarchiv: Archiv-URL im Parameter 'url' anstatt URL der Originalquelle. Entferne den vor der Original-URL stehenden Mementobestandteil und setze den Archivierungszeitstempel in den Parameter 'wayback', 'webciteID', 'archive.today' oder 'archive-is' ein, sofern nicht bereits befüllt.|1}}
            }} 
       }}
  }} Ein Tutorial, das den Umgang mit dem Hoare-Kalkül zur Programmverifikation erklärt (PDF; 493 kB)
  • j-Algo-Modul Hoare Kalkül Ein Visualisierung des Hoare-Kalküls im Rahmen des Algorithmenvisualisierungsprogramms j-Algo
  • KeY-Hoare ist ein halbautomatisches Verifikationssystem, das auf dem KeY-Theorem-Prover aufbaut. Es führt den Hoare-Kalkül für einfache Schleifen durch.

Einzelnachweise

<references />

{{#ifeq: s | p | | {{#if: 4343105-7 | |

}} }}Vorlage:Hinweisbaustein{{#ifeq: s | p | | {{#if: 4343105-7 | |

}} }}{{#ifeq:||{{#if: | [[Kategorie:Wikipedia:GND fehlt {{#invoke:Str|left|{{{GNDCheck}}}|7}}]] }}{{#if: | {{#if: | | }} }} }}{{#if: | {{#ifeq: 0 | 2 | | }} }}{{#if: | {{#ifeq: 0 | 2 | | }} }}{{#ifeq: s | p | {{#if: 4343105-7 | | {{#if: {{#statements:P227}} | | }} }} }}{{#ifeq: s | p | {{#if: 4343105-7 | {{#if: {{#invoke:Wikidata|pageId}} | {{#if: {{#statements:P227}} | | }} }} }} }}{{#ifeq: s | p | {{#if: | | {{#if: {{#statements:P244}} | | }} }} }}{{#ifeq: s | p | {{#if: | {{#if: {{#invoke:Wikidata|pageId}} | {{#if: {{#statements:P244}} | | }} }} }} }}{{#ifeq: s | p | {{#if: | | {{#if: {{#statements:P214}} | | }} }} }}{{#ifeq: s | p | {{#if: | {{#if: {{#invoke:Wikidata|pageId}} | {{#if: {{#statements:P214}} | | }} }} }} }}Vorlage:Wikidata-Registrierung

Abgerufen von „https://wiki-de.moshellshocker.dns64.de/index.php?title=Hoare-Kalkül&oldid=320415“