| dbpprop:abstract
|
- Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers . The original ideas were seeded by the work of Robert Floyd, who had published a similar system for flowcharts.
- Der Hoare-Kalkül (auch Hoare-Logik) ist ein Formales System, entwickelt von dem britischen Informatiker C. A. R. Hoare und später verfeinert von Hoare und anderen Wissenschaftlern. Er wurde 1969 in einem Artikel mit dem Titel An axiomatic basis for computer programming veröffentlicht. 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. 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 nennt man <math>P</math> und <math>Q</math> Zusicherungen (englisch assertions). <math>S</math> ist ein Programmsegment. <math>P</math> heißt die Vorbedingung (englisch precondition), <math>Q</math> heißt die Nachbedingung (englisch postcondition). Zusicherungen sind Formeln der Prädikatenlogik. 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 false 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.
- La lógica de Hoare es un sistema formal desarrollado por C.A.R. Hoare — y posteriormente refinado por otros investigadores — que proporciona a una serie de reglas de inferencia para razonar sobre la corrección de programas imperativos con el rigor de la lógica matemática. Esta lógica fue publicada por Hoare en 1969 donde mencionó las contribuciones de Robert Floyd, que había publicado un sistema similar para los diagramas de flujo. La principal característica de esta lógica es la terna “{Q} S {R}”, donde Q y R son predicados lógicos que deben cumplirse para que el programa S funcione. Es decir, que si el programa S comienza en un estado válido en Q, entonces el programa termina y lo hace en un estado válido para R. Este método de precondición(Q) - postcondición(R) es la base del diseño de software por contrato.
- La logique de Hoare, parfois appelée logique de Floyd-Hoare, est une méthode formelle définie par le chercheur en informatique britannique Tony Hoare dans un article de 1969 intitulé An axiomatic basis for computer programming. La méthode de Hoare met en place un formalisme logique permettant de raisonner sur la correction des programmes informatiques. Hoare s'est inspiré du travail sur les méthodes formelles dans les organigrammes de Robert Floyd, qui lui n'avait pas eu connaissance des travaux d'Alan Turing sur le sujet. La logique de Hoare décrit les évolutions possibles de l'état d'un programme informatique. Les évolutions sont modélisées par des règles et l'état d'un programme est symbolisé par un triplet <math>\{P\}\;C\;\{Q\},</math> où P et Q sont des prédicats et C est une commande (une action sur le programme). La condition P est appelée la précondition et Q la postcondition. La logique de Hoare a des axiomes et des règles d'inférence pour toutes les instructions de base d'un langage de programmation impératif. Hoare rajoute dans son papier originel des règles pour les procédures, les sauts, les pointeurs et la concurrence.
- La Logica di Hoare è un sistema formale che rientra tra le semantiche assiomatiche pubblicato per la prima volta nel 1969 da C. A. R. Hoare che si prefigge, definendo un insieme iniziale di assiomi e di regole su di essi, di valutare la correttezza di programmi utilizzando il rigore dei formalismi matematici. La logica è stata sviluppata per essere utilizzata con un semplice linguaggio di programmazione imperativo ed ha subito sviluppi ulteriori per merito dello stesso Hoare e di altri ricercatori per la gestione di casistiche particolari quali la concorrenza, i puntatori e le procedure.
- ホーア論理（Hoare Logic、別名 Floyd–Hoare Logic）は、アントニー・ホーアが開発した形式体系。ホーアの1969年の論文 "An axiomatic basis for computer programming" で発表された。この体系の目的は、数理論理学の厳密さでプログラムの正当性を論じるための論理的規則群を提供することにある。 ホーアは、フローチャートに関して同様の体系を発表したロバート・フロイドからの影響を認めている。 ホーア論理の中心となる部分は Hoare Triple である。Hoare Triple はコードの実行による状態変化を表すものである。Hoare Triple の形式は以下の通りである。 \{P\}\;C\;\{Q\}</math> ここで、P と Q は「表明(assertion)」であり、C は「コマンド」である。P は「事前状態」、Qは「事後状態」でもある。表明（状態）は述語論理の式で表される。 ホーア論理には、単純な命令型言語の全構成要素についての公理と推論規則が備わっている。当初の論文にあったそれら規則に加えて、ホーアや他の研究者は様々な言語要素に関する規則を開発した。並行性に関する規則、プロシージャに関する規則、分岐に関する規則、ポインタに関する規則などがある。
- Hoarelogica is een rekenmethode in de informatica die gebruikt wordt ter afleiding van programma's. Ze is vernoemd naar de bedenker van de basis van het mechanisme, Tony Hoare.
- logika Hoare'a - formalizm matematyczny służący do opisu poprawności algorytmów. Wprowadzony został przez brytyjskiego naukowca Charlesa A. R. Hoare'a w roku 1969. Napis {P}C{Q} oznacza, że fragment kodu C o ile na wejściu będzie miał stan spełniający warunek P, oraz zakończy swoje działanie, to na wyjściu da stan spełniający warunek Q. Formułę P nazywamy warunkiem wstępnym, a formułę Q nazywamy warunkiem końcowym. Przykład: do instrukcji przypisania x:=5 możemy dopisać następujące warunki wstępne i końcowe: {true}x:=5{x=5} co oznacza, że przy dowolnym stanie przed wykonaniem instrukcji, po wykonaniu instrukcji będziemy mieli stan, w którym zmiennej x jest przypisana wartość 5. prawdą będzie również formuła {x=6, y=100}x:=5{x=5, y=100} bo operacja przypisania na zmienną x nie zmieni oczywiście wartości zmiennej y. {x=15}x:=x+1{x=16} też będzie prawdą, ponieważ operacja przypisania na zmienną x wartości tej zmiennej zwiększonej o 1, przy założeniu, że przed wykonaniem tej instrukcji zmienna x ma wartość 15 da nam wynik, w którym zmienna x będzie miała wartość 16. W przypadku logiki Hoare'a dozwolone jest m. in. następujące rozumowanie: jeśli {P1}C{P2} oraz {P2}D{P3}, to {P1}C; D{P3}. Pozwala nam to rozbijać złożone fragmentu kodu na instrukcje elementarne, dla których weryfikacja poprawności zapisu {P}C{Q} jest łatwa.
- Hoare 逻辑(也叫做Floyd–Hoare 逻辑)是英国计算机科学家 C. A. R. Hoare 开发的形式系统，随后为 Hoare 和其他研究者所精制。它发表于 Hoare 1969年的论文"计算机程序的公理基础"中。这个系统的用途是为了使用严格的数理逻辑推理计算机程序的正确性提供一组逻辑规则。 Hoare 认可罗伯特·弗洛伊德的早期贡献，他为流程图提供了类似的系统。 Hoare 逻辑的中心特征是Hoare 三元组。这种三元组描述一段代码的执行如何改变计算的状态。Hoare 三元组有如下形式 \{P\}\;C\;\{Q\}</math> 这里的 P 和 Q 是断言而 C 是命令。P 叫做前条件而 Q 叫做后条件。断言是谓词逻辑的公式。这个三元组在直觉上读做: 只要 P 在 C 执行前的状态下成立，则在执行之后 Q 也成立。注意如果 C 不终止，也就没有"之后"了，所以 Q 在根本上可以是任何语句。实际上，你可以选择 Q 为假来表达 C 不终止。 这叫做"部分正确(partial correctness)"的。如果 C 终止并且在终止时 Q 是真，则表达式就是"全部正确(total correctness)"的。终止必须被单独证明。 Hoare 逻辑为简单的命令式编程语言的所有构造提供了公理和推理规则。除了给 Hoare 论文中的简单语言的规则，其他语言构造的规则也已经被 Hoare 和很多其他研究者开发出来了。包括并发、过程、goto语句，和指针。
|
| rdfs:comment
|
- Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers . The original ideas were seeded by the work of Robert Floyd, who had published a similar system for flowcharts.
- Der Hoare-Kalkül (auch Hoare-Logik) ist ein Formales System, entwickelt von dem britischen Informatiker C. A. R. Hoare und später verfeinert von Hoare und anderen Wissenschaftlern. Er wurde 1969 in einem Artikel mit dem Titel An axiomatic basis for computer programming veröffentlicht.
- La lógica de Hoare es un sistema formal desarrollado por C.A.R. Hoare — y posteriormente refinado por otros investigadores — que proporciona a una serie de reglas de inferencia para razonar sobre la corrección de programas imperativos con el rigor de la lógica matemática. Esta lógica fue publicada por Hoare en 1969 donde mencionó las contribuciones de Robert Floyd, que había publicado un sistema similar para los diagramas de flujo.
- La logique de Hoare, parfois appelée logique de Floyd-Hoare, est une méthode formelle définie par le chercheur en informatique britannique Tony Hoare dans un article de 1969 intitulé An axiomatic basis for computer programming. La méthode de Hoare met en place un formalisme logique permettant de raisonner sur la correction des programmes informatiques.
- La Logica di Hoare è un sistema formale che rientra tra le semantiche assiomatiche pubblicato per la prima volta nel 1969 da C. A. R. Hoare che si prefigge, definendo un insieme iniziale di assiomi e di regole su di essi, di valutare la correttezza di programmi utilizzando il rigore dei formalismi matematici.
- Hoarelogica is een rekenmethode in de informatica die gebruikt wordt ter afleiding van programma's. Ze is vernoemd naar de bedenker van de basis van het mechanisme, Tony Hoare.
- logika Hoare'a - formalizm matematyczny służący do opisu poprawności algorytmów. Wprowadzony został przez brytyjskiego naukowca Charlesa A. R. Hoare'a w roku 1969. Napis {P}C{Q} oznacza, że fragment kodu C o ile na wejściu będzie miał stan spełniający warunek P, oraz zakończy swoje działanie, to na wyjściu da stan spełniający warunek Q. Formułę P nazywamy warunkiem wstępnym, a formułę Q nazywamy warunkiem końcowym.
- Hoare 逻辑(也叫做Floyd–Hoare 逻辑)是英国计算机科学家 C. A. R.
|
![[RDF Data]](/statics/sw-cube.png)
