An Entity of Type: programming language, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

Axiomatic semantics is an approach based on mathematical logic for proving the correctness of computer programs. It is closely related to Hoare logic. Axiomatic semantics define the meaning of a command in a program by describing its effect on assertions about the program state. The assertions are logical statements—predicates with variables, where the variables define the state of the program.

Property Value
dbo:abstract
  • Αξιωματική σημασιολογία (axiomatic semantics) ονομάζεται μια προσέγγιση της απόδειξης της , η οποία βασίζεται στη μαθηματική λογική. Έχει στενή σχέση με τη . Η αξιωματική σημασιολογία ορίζει τη σημασία μιας εντολής ενός προγράμματος περιγράφοντας την επίδρασή της σε βεβαιώσεις (assertions) σχετικά με την κατάσταση του προγράμματος. Οι βεβαιώσεις είναι λογικές προτάσεις - κατηγορήματα με μεταβλητές, όπου οι μεταβλητές περιγράφουν την κατάσταση του προγράμματος. (el)
  • Die axiomatische Semantik der Informatik beschreibt die Bedeutung von Programmen durch Schlussregeln, die es erlauben, von einer gewünschten Eigenschaft der Eingabe auf Eigenschaften der Ausgabe zu schließen. Dabei abstrahiert die axiomatische Semantik weiter als die denotationelle Semantik. Es werden keine konkreten Speicher transformiert, sondern nur logische Aussagen über Speicher, genauer gesagt über Werte von Programmvariablen in ihnen. Dabei entspricht die axiomatische Semantik der Sicht des Programmierers.Sie scheint im Gegensatz zur operationellen Semantik nur für imperative Sprachen geeignet zu sein. Es existieren zwei Hauptausprägungen, der Hoare-Kalkül und der wp-Kalkül. (de)
  • Axiomatic semantics is an approach based on mathematical logic for proving the correctness of computer programs. It is closely related to Hoare logic. Axiomatic semantics define the meaning of a command in a program by describing its effect on assertions about the program state. The assertions are logical statements—predicates with variables, where the variables define the state of the program. (en)
  • Semántica axiomática es un enfoque basado en la lógica matemática para demostrar la correctitud de un algoritmo. Está estrechamente relacionado con la lógica de Hoare. La semántica axiomática define el significado de un comando dentro de un programa, mediante la descripción de su efecto sobre las aserciones acerca del estado del programa. El primer aporte significativo en esta aproximación, fue realizado por Hoare y Wirth en 1980. más precisamente para proveer la semántica del lenguaje Pascal. (es)
  • La sémantique axiomatique est une approche basée sur la logique mathématique qui sert à prouver qu'un programme informatique est correct. (fr)
  • 公理的意味論(こうりてきいみろん、Axiomatics Semantics)とは、数理論理学に基づいてプログラムの正当性を証明する手法。ホーア論理と密接に関連している。 (ja)
  • Semântica axiomática é uma abordagem de semântica formal. A semântica formal é uma das áreas de estudo de ciência da computação, preocupada em atribuir significado às construções das linguagens de programação. Nesta abordagem se especificam propriedades do efeito da execução das estruturas como asserções, que são sentenças da lógica de predicados. Estas sentenças são usualmente chamadas de axiomas, e daí o nome desta abordagem. Como as asserções se referem aos valores das variáveis dos programas, alguns aspectos da execução são ignorados. A abordagem axiomática enfatiza a possibilidade de provar propriedades de programas usando-se lógica formal, particularmente verificação formal. A abordagem faz uso de asserções, que são sentenças da lógica definidas sobre os valores das variáveis do programa. Por exemplo, em , e são asserções. é chamada de pré-condição, representando uma sentença que é verdadeira antes da execução do comando , e é chamada de póscondição, representando uma sentença que é verdadeira após a execução do comando . A abordagem axiomática foi proposta por Floyd e Hoare na década de 1960. (pt)
  • 公理语义学(Axiomatic semantics)是使用数理逻辑来证明。程序中的命令的意义描述是通过对程序状态的断言(assertion)效果。断言是逻辑语句——带变量的谓词,而这些变量定义了程序的状态。 公理语义学的一个实例是霍尔逻辑。 (zh)
  • Аксіоматична семантика — підхід до опису семантики системи за допомогоюаксіоматичних теорій: теорії множин, натуральних чисел, математичної логіки. Система описується в рамках визначених понять за допомогою аксіом та правил виводу. Як база використовується апарат математичної логіки. Використання аксіоматичної семантики дозволяє ввести поняття часткової коректності системи. Система частково коректна, якщо при задовільненні у початковому стані визначених умов (передумов) після завершення вона задовольняє відповідні умови (постумови). (uk)
dbo:wikiPageID
  • 518199 (xsd:integer)
dbo:wikiPageLength
  • 1488 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1063360890 (xsd:integer)
dbo:wikiPageWikiLink
dbp:wikiPageUsesTemplate
dcterms:subject
gold:hypernym
rdf:type
rdfs:comment
  • Αξιωματική σημασιολογία (axiomatic semantics) ονομάζεται μια προσέγγιση της απόδειξης της , η οποία βασίζεται στη μαθηματική λογική. Έχει στενή σχέση με τη . Η αξιωματική σημασιολογία ορίζει τη σημασία μιας εντολής ενός προγράμματος περιγράφοντας την επίδρασή της σε βεβαιώσεις (assertions) σχετικά με την κατάσταση του προγράμματος. Οι βεβαιώσεις είναι λογικές προτάσεις - κατηγορήματα με μεταβλητές, όπου οι μεταβλητές περιγράφουν την κατάσταση του προγράμματος. (el)
  • Axiomatic semantics is an approach based on mathematical logic for proving the correctness of computer programs. It is closely related to Hoare logic. Axiomatic semantics define the meaning of a command in a program by describing its effect on assertions about the program state. The assertions are logical statements—predicates with variables, where the variables define the state of the program. (en)
  • Semántica axiomática es un enfoque basado en la lógica matemática para demostrar la correctitud de un algoritmo. Está estrechamente relacionado con la lógica de Hoare. La semántica axiomática define el significado de un comando dentro de un programa, mediante la descripción de su efecto sobre las aserciones acerca del estado del programa. El primer aporte significativo en esta aproximación, fue realizado por Hoare y Wirth en 1980. más precisamente para proveer la semántica del lenguaje Pascal. (es)
  • La sémantique axiomatique est une approche basée sur la logique mathématique qui sert à prouver qu'un programme informatique est correct. (fr)
  • 公理的意味論(こうりてきいみろん、Axiomatics Semantics)とは、数理論理学に基づいてプログラムの正当性を証明する手法。ホーア論理と密接に関連している。 (ja)
  • 公理语义学(Axiomatic semantics)是使用数理逻辑来证明。程序中的命令的意义描述是通过对程序状态的断言(assertion)效果。断言是逻辑语句——带变量的谓词,而这些变量定义了程序的状态。 公理语义学的一个实例是霍尔逻辑。 (zh)
  • Аксіоматична семантика — підхід до опису семантики системи за допомогоюаксіоматичних теорій: теорії множин, натуральних чисел, математичної логіки. Система описується в рамках визначених понять за допомогою аксіом та правил виводу. Як база використовується апарат математичної логіки. Використання аксіоматичної семантики дозволяє ввести поняття часткової коректності системи. Система частково коректна, якщо при задовільненні у початковому стані визначених умов (передумов) після завершення вона задовольняє відповідні умови (постумови). (uk)
  • Die axiomatische Semantik der Informatik beschreibt die Bedeutung von Programmen durch Schlussregeln, die es erlauben, von einer gewünschten Eigenschaft der Eingabe auf Eigenschaften der Ausgabe zu schließen. Dabei abstrahiert die axiomatische Semantik weiter als die denotationelle Semantik. Es werden keine konkreten Speicher transformiert, sondern nur logische Aussagen über Speicher, genauer gesagt über Werte von Programmvariablen in ihnen. Es existieren zwei Hauptausprägungen, der Hoare-Kalkül und der wp-Kalkül. (de)
  • Semântica axiomática é uma abordagem de semântica formal. A semântica formal é uma das áreas de estudo de ciência da computação, preocupada em atribuir significado às construções das linguagens de programação. Nesta abordagem se especificam propriedades do efeito da execução das estruturas como asserções, que são sentenças da lógica de predicados. Estas sentenças são usualmente chamadas de axiomas, e daí o nome desta abordagem. Como as asserções se referem aos valores das variáveis dos programas, alguns aspectos da execução são ignorados. (pt)
rdfs:label
  • Axiomatic semantics (en)
  • Axiomatische Semantik (de)
  • Αξιωματική σημασιολογία (el)
  • Semántica axiomática (es)
  • Sémantique axiomatique (fr)
  • 公理的意味論 (ja)
  • Semântica axiomática (pt)
  • 公理语义学 (zh)
  • Аксіоматична семантика (uk)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageWikiLink of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License