About: Hoare logic     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : yago:PsychologicalFeature100023100, within Data Space : dbpedia.org associated with source document(s)

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 Tony Hoare, and subsequently refined by Hoare and other researchers. The original ideas were seeded by the work of Robert W. Floyd, who had published a similar system for flowcharts.

AttributesValues
rdf:type
rdfs:label
  • Hoare logic
  • Hoare-Kalkül
  • Lógica de Hoare
  • Logique de Hoare
  • Logica di Hoare
  • ホーア論理
  • Hoarelogica
  • Logika Hoare’a
  • Lógica de Hoare
  • Логика Хоара
  • 霍尔逻辑
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 Tony Hoare, and subsequently refined by Hoare and other researchers. The original ideas were seeded by the work of Robert W. Floyd, who had published a similar system for flowcharts.
  • Hoarelogica is een formele logica die in de informatica wordt gebruikt om over programma's te redeneren. Ze is vernoemd naar de bedenker van de basis van het mechanisme, Tony Hoare.
  • 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)とは、公理的意味論の立場でプログラムの正当性について厳密に推論するために第一階述語論理を拡張した形式論理の言語を言う。 プログラムの正しさを証明するためのロバート・フロイドによる流れ図に関する方法を基に、計算機科学者のアントニー・ホーアによって提案された。
  • Lógica de Hoare(também conhecida como lógica de Floyd–Hoare ou regras de Hoare) é um sistema formal com um conjunto de regras lógicas para um raciocínio rigoroso sobre a corretude na computação. Proposta em 1969 pelo cientista da computação e lógico britânico C. A. R. Hoare, e subsequêncialmente aprimorada por Hoare e outros pesquisadores. A idéia original havia sido idealizada pelo trabalho de Robert Floyd, que publicou um sistema similar para fluxogramas.
  • 霍爾邏輯(英语:Hoare Logic),又稱弗洛伊德-霍爾邏輯(Floyd–Hoare logic),是英国计算机科学家東尼·霍爾开发的形式系统,这个系统的用途是为了使用严格的数理逻辑推理來替计算机程序的正确性提供一组逻辑规则。 這個想法起源於罗伯特·弗洛伊德於較早的研究,他为流程图提供了类似的系统。東尼·霍爾於1969年首次發表,随后为其他研究者所精制。
  • Логика Хоара (англ. Hoare logic, также Floyd—Hoare logic, или Hoare rules) — формальная система с набором логических правил, предназначенных для доказательства корректности компьютерных программ. Была предложена в 1969 году английским учёным в области информатики и математической логики Хоаром, позже развита самим Хоаром и другими исследователями. Первоначальная идея была предложена в работе Флойда, который опубликовал похожую систему в применении к блок-схемам (англ. flowchart).
  • Der Hoare-Kalkül (auch Hoare-Logik) 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 verfeinert. Der Hoare-Kalkül wurde 1969 in einem Artikel mit dem Titel An axiomatic basis for computer programming veröffentlicht. Alternativ kann auch der wp-Kalkül benutzt werden, bei dem im Gegensatz zum Hoare-Kalkül eine Rückwärtsanalyse stattfindet.
  • 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. 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. Elle est fondée sur la syntaxe en ce sens que la correction d'un programme est décrite et démontrée par induction (récurrence) sur la structure du programme : à chaque règle syntaxique de construction d'un programme correspond une règle de la logique de Hoare. Elle a deux utilisations : fournir un outil de vérification formelle des programmes sans les exécuter (analyse statique), décrire rigoureusement la sémantique des langages de programma
  • 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. 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 wartości zmiennej y. jeśli {P1}C{P2} oraz {P2}D{P3}, to {P1}C; D{P3}.
sameAs
dct:subject
Wikipage page ID
Wikipage revision ID
Link from a Wikipage to another Wikipage
Link from a Wikipage to an external page
foaf:isPrimaryTopicOf
prov:wasDerivedFrom
has 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 Tony Hoare, and subsequently refined by Hoare and other researchers. The original ideas were seeded by the work of Robert W. Floyd, who had published a similar system for flowcharts.
Faceted Search & Find service v1.17_git39 as of Aug 09 2019


Alternative Linked Data Documents: PivotViewer | iSPARQL | ODE     Content Formats:       RDF       ODATA       Microdata      About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
OpenLink Virtuoso version 07.20.3235 as of Jun 25 2020, on Linux (x86_64-generic-linux-glibc25), Single-Server Edition (61 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2020 OpenLink Software