Axiomatic semantics is an approach based on mathematical logic to 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.

PropertyValue
dbpprop:abstract
  • Axiomatic semantics is an approach based on mathematical logic to 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.
  • 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. Siehe auch: Formale Semantik operationelle Semantik denotationelle Semantik
  • La sémantique axiomatique est une approche basée sur la logique mathématique qui sert à prouver qu'un programme informatique est correct.
  • 公理的意味論（こうりてきいみろん、Axiomatics Semantics）とは、数理論理学に基づいてプログラムの正当性を証明する手法。ホーア論理と密接に関連している。
  • 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 contruçõ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 <math>\{P\} Q \{R\}</math>, <math>P</math> e <math>R</math> são asserções. <math>P</math> é chamada de pré-condição, representando uma sentença que é verdadeira antes da execução do comando <math>Q</math>, e <math>R</math> é chamada de póscondição, representando uma sentença que é verdadeira após a execução do comando <math>Q</math>. A abordagem axiomática foi proposta por Floyd e Hoare na década de 1960. Semântica formal Ciência da computação Linguagens de programação Linguagens formais e compiladores
dbpprop:hasPhotoCollection
rdf:type
rdfs:comment
  • Axiomatic semantics is an approach based on mathematical logic to 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.
  • 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.
  • La sémantique axiomatique est une approche basée sur la logique mathématique qui sert à prouver qu'un programme informatique est correct.
  • 公理的意味論（こうりてきいみろん、Axiomatics Semantics）とは、数理論理学に基づいてプログラムの正当性を証明する手法。ホーア論理と密接に関連している。
  • 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 contruçõ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.
rdfs:label
  • Axiomatic semantics
  • Axiomatische Semantik
  • Sémantique axiomatique
  • 公理的意味論
  • Semântica axiomática
owl:sameAs
skos:subject
foaf:page
is owl:sameAs of