| http://dbpedia.org/ontology/abstract
|
La logica di Hoare è un sistema formale ch … 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.a concorrenza, i puntatori e le procedure.
, La logique de Hoare, parfois appelée logiq … 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 programmation (sémantique axiomatique). La logique de Hoare a des axiomes pour toutes les instructions de base d'un langage de programmation impératif et des règles d'inférence pour les compositions d'instructions comme le si ... alors ... sinon ... ou le tant que. Hoare ajoute dans son article originel des règles pour les procédures, les sauts, les pointeurs et la concurrence.es sauts, les pointeurs et la concurrence.
, 霍爾邏輯（英語：Hoare Logic），又稱弗洛伊德-霍爾邏輯（Floyd–Hoare logic），是英国计算机科学家東尼·霍爾开发的形式系统，这个系统的用途是为了使用严格的数理逻辑推理來替计算机程序的正确性提供一组逻辑规则。 這個想法起源於罗伯特·弗洛伊德於較早的研究，他为流程图提供了类似的系统。東尼·霍爾於1969年首次發表，随后为其他研究者所精制。
, La lógica de Hoare es un sistema formal de … 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 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 o triplete “{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. base del diseño de software por contrato.
, Hoare logic (also known as Floyd–Hoare log … 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.published a similar system for flowcharts.
, Алгоритмічна логіка Гоара (також відома як … Алгоритмічна логіка Гоара (також відома як Флойда-Гоара) — це формальна система з множиною логічних правил для строгого доведення . Запропонована в 1969 британським інформатиком та логіком Тоні Гоаром, і пізніше вдосконалена ним же, та іншими дослідниками. Початкові ідеї були закладені в роботі Роберта Флойда, який опублікував подібну систему для блок-схем.опублікував подібну систему для блок-схем.
, Logika Hoare’a – formalizm matematyczny sł … 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 oznacza, że fragment kodu o ile na wejściu będzie miał stan spełniający warunek oraz zakończy swoje działanie, to na wyjściu da stan spełniający warunek Formułę nazywamy , a formułę nazywamy . Przykład:do instrukcji przypisania możemy dopisać następujące warunki wstępne i końcowe: co oznacza, że przy dowolnym stanie przed wykonaniem instrukcji, po wykonaniu instrukcji będziemy mieli stan, w którym zmiennej jest przypisana wartość 5. prawdą będzie również formuła bo operacja przypisania na zmienną nie zmieni wartości zmiennej też będzie prawdą, ponieważ operacja przypisania na zmienną wartości tej zmiennej zwiększonej o 1, przy założeniu, że przed wykonaniem tej instrukcji zmienna ma wartość 15 da nam wynik, w którym zmienna będzie miała wartość 16. W przypadku logiki Hoare’a dozwolone jest m.in. następujące rozumowanie: jeśli oraz to Pozwala nam to rozbijać złożone fragmentu kodu na instrukcje elementarne, dla których weryfikacja poprawności zapisu jest łatwa.weryfikacja poprawności zapisu jest łatwa.
, 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.
, Логика Хоара (англ. Hoare logic, также Flo … Логика Хоара (англ. Hoare logic, также Floyd—Hoare logic, или Hoare rules) — формальная система с набором логических правил, предназначенных для доказательства корректности компьютерных программ. Была предложена в 1969 году английским учёным в области информатики и математической логики Хоаром, позже развита самим Хоаром и другими исследователями. Первоначальная идея была предложена в работе Флойда, который опубликовал похожую систему в применении к блок-схемам (англ. flowchart).рименении к блок-схемам (англ. flowchart).
, Der Hoare-Kalkül (auch Hoare-Logik) ist ei … 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. 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. Im Gegensatz zum floydschen Verfahren, bei dem Ausführungspfade interpretiert werden, arbeitet der Hoare-Kalkül mit dem Quellcode. Alternativ kann auch der wp-Kalkül benutzt werden, bei dem im Gegensatz zum Hoare-Kalkül eine Rückwärtsanalyse stattfindet.-Kalkül eine Rückwärtsanalyse stattfindet.
, ホーア論理（ホーアろんり、英: Hoare logic）とは、公理的意味論の立場でプログラムの正当性について厳密に推論するために第一階述語論理を拡張した形式論理の言語を言う。 プログラムの正しさを証明するためのロバート・フロイドによる流れ図に関する方法を基に、計算機科学者のアントニー・ホーアによって提案された。
, Lógica de Hoare (também conhecida como lóg … 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 subsequencialmente 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.licou um sistema similar para fluxogramas.
|
| http://dbpedia.org/ontology/wikiPageExternalLink
|
http://j-algo.binaervarianz.de/index.php%3Flanguage=en +
, https://web.archive.org/web/20071117054808/http:/www.key-project.org/download/hoare/ +
, http://www.cs.queensu.ca/home/specsoft/ +
|
| http://dbpedia.org/ontology/wikiPageID
|
182708
|
| http://dbpedia.org/ontology/wikiPageLength
|
22234
|
| http://dbpedia.org/ontology/wikiPageRevisionID
|
1124506026
|
| http://dbpedia.org/ontology/wikiPageWikiLink
|
http://dbpedia.org/resource/Minimal_element +
, http://dbpedia.org/resource/Loop_invariant +
, http://dbpedia.org/resource/Predicate_transformer_semantics +
, http://dbpedia.org/resource/Inference_rule +
, http://dbpedia.org/resource/Design_by_contract +
, http://dbpedia.org/resource/Positive_real_numbers +
, http://dbpedia.org/resource/Formal_system +
, http://dbpedia.org/resource/Flowchart +
, http://dbpedia.org/resource/Postcondition +
, http://dbpedia.org/resource/Procedure_%28computer_science%29 +
, http://dbpedia.org/resource/Precondition +
, http://dbpedia.org/resource/Axiom +
, http://dbpedia.org/resource/Assertion_%28software_development%29 +
, http://dbpedia.org/resource/Termination_analysis +
, http://dbpedia.org/resource/Partial_correctness +
, http://dbpedia.org/resource/Dynamic_logic_%28modal_logic%29 +
, http://dbpedia.org/resource/Tony_Hoare +
, http://dbpedia.org/resource/Program_transformation +
, http://dbpedia.org/resource/Category:1969_in_computing +
, http://dbpedia.org/resource/KeY +
, http://dbpedia.org/resource/Static_program_analysis +
, http://dbpedia.org/resource/Well-founded_relation +
, http://dbpedia.org/resource/Jump_%28computer_science%29 +
, http://dbpedia.org/resource/Substitution_%28logic%29 +
, http://dbpedia.org/resource/Mathematical_logic +
, http://dbpedia.org/resource/Chain_%28order_theory%29 +
, http://dbpedia.org/resource/NOP_%28code%29 +
, http://dbpedia.org/resource/Imperative_programming +
, http://dbpedia.org/resource/Pointer_%28computer_programming%29 +
, http://dbpedia.org/resource/Predicate_logic +
, http://dbpedia.org/resource/Category:Program_logic +
, http://dbpedia.org/resource/Formal_verification +
, http://dbpedia.org/resource/Free_variables_and_bound_variables +
, http://dbpedia.org/resource/Concurrency_%28computer_science%29 +
, http://dbpedia.org/resource/Correctness_of_computer_programs +
, http://dbpedia.org/resource/Integer +
, http://dbpedia.org/resource/Robert_W._Floyd +
, http://dbpedia.org/resource/Category:Static_program_analysis +
, http://dbpedia.org/resource/Aliasing_%28computing%29 +
, http://dbpedia.org/resource/Termination_proof +
, http://dbpedia.org/resource/Total_correctness +
, http://dbpedia.org/resource/Denotational_semantics +
, http://dbpedia.org/resource/Assertion_%28computing%29 +
, http://dbpedia.org/resource/Loop_variant +
|
| http://dbpedia.org/property/wikiPageUsesTemplate
|
http://dbpedia.org/resource/Template:Quote +
, http://dbpedia.org/resource/Template:Mono +
, http://dbpedia.org/resource/Template:ISBN +
, http://dbpedia.org/resource/Template:Reflist +
, http://dbpedia.org/resource/Template:Authority_control +
, http://dbpedia.org/resource/Template:Mvar +
, http://dbpedia.org/resource/Template:Columns-list +
, http://dbpedia.org/resource/Template:Short_description +
|
| http://purl.org/dc/terms/subject
|
http://dbpedia.org/resource/Category:Static_program_analysis +
, http://dbpedia.org/resource/Category:1969_in_computing +
, http://dbpedia.org/resource/Category:Program_logic +
|
| http://purl.org/linguistics/gold/hypernym
|
http://dbpedia.org/resource/System +
|
| http://www.w3.org/ns/prov#wasDerivedFrom
|
http://en.wikipedia.org/wiki/Hoare_logic?oldid=1124506026&ns=0 +
|
| http://xmlns.com/foaf/0.1/isPrimaryTopicOf
|
http://en.wikipedia.org/wiki/Hoare_logic +
|
| owl:sameAs |
http://nl.dbpedia.org/resource/Hoarelogica +
, http://sk.dbpedia.org/resource/Hoareova_logika +
, http://rdf.freebase.com/ns/m.018z8r +
, http://ru.dbpedia.org/resource/%D0%9B%D0%BE%D0%B3%D0%B8%D0%BA%D0%B0_%D0%A5%D0%BE%D0%B0%D1%80%D0%B0 +
, http://it.dbpedia.org/resource/Logica_di_Hoare +
, https://global.dbpedia.org/id/PARV +
, http://fr.dbpedia.org/resource/Logique_de_Hoare +
, http://es.dbpedia.org/resource/L%C3%B3gica_de_Hoare +
, http://dbpedia.org/resource/Hoare_logic +
, http://uk.dbpedia.org/resource/%D0%9B%D0%BE%D0%B3%D1%96%D0%BA%D0%B0_%D0%93%D0%BE%D0%B0%D1%80%D0%B0 +
, http://pl.dbpedia.org/resource/Logika_Hoare%E2%80%99a +
, http://vi.dbpedia.org/resource/Lu%E1%BA%ADn_l%C3%BD_Hoare +
, http://pt.dbpedia.org/resource/L%C3%B3gica_de_Hoare +
, http://www.wikidata.org/entity/Q1375924 +
, http://de.dbpedia.org/resource/Hoare-Kalk%C3%BCl +
, http://d-nb.info/gnd/4343105-7 +
, http://ja.dbpedia.org/resource/%E3%83%9B%E3%83%BC%E3%82%A2%E8%AB%96%E7%90%86 +
, http://zh.dbpedia.org/resource/%E9%9C%8D%E5%B0%94%E9%80%BB%E8%BE%91 +
, http://yago-knowledge.org/resource/Hoare_logic +
|
| rdf:type |
http://dbpedia.org/class/yago/Cognition100023271 +
, http://dbpedia.org/class/yago/WikicatFormalMethods +
, http://dbpedia.org/class/yago/PsychologicalFeature100023100 +
, http://dbpedia.org/class/yago/Abstraction100002137 +
, http://dbpedia.org/class/yago/Ability105616246 +
, http://dbpedia.org/class/yago/Method105660268 +
, http://dbpedia.org/class/yago/Know-how105616786 +
|
| rdfs:comment |
Logika Hoare’a – formalizm matematyczny sł … 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 oznacza, że fragment kodu o ile na wejściu będzie miał stan spełniający warunek oraz zakończy swoje działanie, to na wyjściu da stan spełniający warunek Formułę nazywamy , a formułę nazywamy . Przykład:do instrukcji przypisania możemy dopisać następujące warunki wstępne i końcowe: prawdą będzie również formuła bo operacja przypisania na zmienną nie zmieni wartości zmiennej jeśli oraz tonie zmieni wartości zmiennej jeśli oraz to
, ホーア論理（ホーアろんり、英: Hoare logic）とは、公理的意味論の立場でプログラムの正当性について厳密に推論するために第一階述語論理を拡張した形式論理の言語を言う。 プログラムの正しさを証明するためのロバート・フロイドによる流れ図に関する方法を基に、計算機科学者のアントニー・ホーアによって提案された。
, Der Hoare-Kalkül (auch Hoare-Logik) ist ei … 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.-Kalkül eine Rückwärtsanalyse stattfindet.
, La logique de Hoare, parfois appelée logiq … 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 programmant la sémantique des langages de programma
, Алгоритмічна логіка Гоара (також відома як … Алгоритмічна логіка Гоара (також відома як Флойда-Гоара) — це формальна система з множиною логічних правил для строгого доведення . Запропонована в 1969 британським інформатиком та логіком Тоні Гоаром, і пізніше вдосконалена ним же, та іншими дослідниками. Початкові ідеї були закладені в роботі Роберта Флойда, який опублікував подібну систему для блок-схем.опублікував подібну систему для блок-схем.
, 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 lógica de Hoare es un sistema formal de … 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 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. base del diseño de software por contrato.
, Hoare logic (also known as Floyd–Hoare log … 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.published a similar system for flowcharts.
, Логика Хоара (англ. Hoare logic, также Flo … Логика Хоара (англ. Hoare logic, также Floyd—Hoare logic, или Hoare rules) — формальная система с набором логических правил, предназначенных для доказательства корректности компьютерных программ. Была предложена в 1969 году английским учёным в области информатики и математической логики Хоаром, позже развита самим Хоаром и другими исследователями. Первоначальная идея была предложена в работе Флойда, который опубликовал похожую систему в применении к блок-схемам (англ. flowchart).рименении к блок-схемам (англ. flowchart).
, 霍爾邏輯（英語：Hoare Logic），又稱弗洛伊德-霍爾邏輯（Floyd–Hoare logic），是英国计算机科学家東尼·霍爾开发的形式系统，这个系统的用途是为了使用严格的数理逻辑推理來替计算机程序的正确性提供一组逻辑规则。 這個想法起源於罗伯特·弗洛伊德於較早的研究，他为流程图提供了类似的系统。東尼·霍爾於1969年首次發表，随后为其他研究者所精制。
, Lógica de Hoare (também conhecida como lóg … 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 subsequencialmente 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.licou um sistema similar para fluxogramas.
, La logica di Hoare è un sistema formale ch … 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.a concorrenza, i puntatori e le procedure.
|
| rdfs:label |
Hoare logic
, ホーア論理
, Lógica de Hoare
, Logique de Hoare
, Логика Хоара
, Logika Hoare’a
, Логіка Гоара
, Logica di Hoare
, Hoarelogica
, 霍尔逻辑
, Hoare-Kalkül
|
