Predicate transformer semantics (original) (raw)
述語変換意味論（じゅつごへんかんいみろん、Predicate Transformer Semantics）は、エドガー・ダイクストラによるホーア論理の拡張であり、その後も他の研究者が改良を加えたものである。最初に登場したのはダイクストラの論文 "Guarded commands, nondeterminacy and formal derivation of programs" であった。
| Property | Value |
|---|---|
| dbo:abstract | La semàntica de transformació de predicats és una extensió de la lògica de Floyd-Hoare ideada per Edsger Dijkstra i divulgada i perfeccionada per altres investigadors. Aquesta extensió va presentar-la Dijkstra en l'article "Comandaments guardats, no-determinisme i derivació formal de programes". Consisteix en un mètode per a definir la semàntica d'un llenguatge de programació imperativa amb l'assignació a cada comandament del corresponent transformador de predicats. Un transformador de predicats és una funció total entre dos predicats del conjunt d'estats d'un programa. El transformador de predicats canònic de la programació imperativa seqüencial és el conegut com "weakest precondition" (precondició més feble), , en què S denota una seqüència de comandaments i R un predicat anomenat "postcondició". El resultat de l'aplicació és la "precondició més feble" perquè S acabe de manera que R siga cert. N'és un exemple la definició de la sentència d'assignació: D'aquesta operació resulta un predicat que és una còpia de R però amb el valor E assignat a la variable x. Un exemple d'un càlcul vàlid d'un wp per a una assignació de variables senceres x e y és: Això significa que perquè la "postcondició" x > 10 siga certa després de l'assignació, la "precondició" y > 15 ha de ser certa abans de l'assignació. Això també és la "precondició més feble", mentre és la restricció "més feble" que cal aplicar al valor de y perquè x > 10 siga cert després de l'assignació. Dijkstra també va definir construccions d'aquest tipus per a les estructures alternativa (if) i repetitiva (do), així com un operador de composició utilitzant wp. Les construccions alternativa i repetitiva usen comandaments guardats per a influir en l'execució. Per les regles imposades per ell en la definició de wp, totes dues construccions permeten execucions no deterministes si els guardians dels comandaments no són disjunts. A diferència d'altres formalismes semàntics, la semàntica de transformació de predicats no fou resultat de la recerca en centres de computació. Fou creada amb la intenció de facilitar als programadors una metodologia de creació de programes "correctament construïts" basada en un "estil matemàtic". Tot i que és el més comú per la seua rellevància en la programació seqüencial, la "precondició més feble" no és l'únic transformador de predicats que hi ha. Per exemple, Leslie Lamport ha proposat win i sin com a transformadors de predicats per fer servir en la programació concurrent. (ca) Der wp-Kalkül ist ein Kalkül in der Informatik zur Verifikation eines imperativen Programmcodes. Die Abkürzung wp steht für weakest precondition, auf deutsch schwächste Vorbedingung. Bei der Verifikation geht es nicht darum, die Funktion mit einer bestimmten Menge an Eingabedaten auf korrekte Ergebnisse zu testen, sondern darum, eine allgemeingültige Aussage über das korrekte Ablaufen des Programms zu erhalten. Die Überprüfung der Korrektheit geschieht durch Rückwärtsanalyse des Programmcodes. Ausgehend von der Nachbedingung wird geprüft, ob diese durch die Vorbedingung und den Programmcode garantiert wird. Alternativ kann auch der Hoare-Kalkül benutzt werden, bei dem im Gegensatz zum wp-Kalkül eine Vorwärtsanalyse stattfindet. Der wp-Kalkül hilft gewisse Zusicherungen im Programm zu machen. Eine Zusicherung ist eine prädikatenlogische Aussage über den Inhalt derVariablen an der bestimmten Stelle. Eine Zusicherung vor einem Programmtext heißt Vorbedingung P, eine Zusicherung danach Nachbedingung Q. // x ist gerade// P: (x % 2) = 0x = x + 1;// x ist ungerade// Q: (x % 2) = 1 Der wp-Kalkül erlaubt es nun anhand bestimmter Regeln aus einer Nachbedingung die nötige Vorbedingung, und zwar die schwächste Vorbedingung, zu schließen, die erfüllt sein muss damit nach Ausführung des Programmcodes die Nachbedingung erfüllt ist. (de) La semántica de transformación de predicados es una extensión de Lógica de Floyd-Hoare ideada por Edsger Dijkstra y extendida y refinada por otros investigadores. Esta extensión fue presentada por Dijkstra en sus artículos titulados "Guarded commands, nondeterminacy and formal derivation of programs" ("Comandos guardados, no-determinismo y derivación formal de programas"). Consiste en un método para definir la semántica de un lenguaje de programación imperativa mediante la asignación a cada comando del correspondiente transformador de predicados. Un es una función total entre dos predicados del conjunto de estados de un programa. El transformador de predicados canónico de la programación imperativa secuencial es el conocido normalmente como "weakest precondition" (precondición más débil) . Aquí S denota una secuencia de comandos y R un predicada llamado "postcondición". El resultado de su aplicación es la "precondición más débil" para que S termine de modo que R sea cierto. Un ejemplo es la siguiente definición de la sentencia de asignación: De esta operación resulta un predicado que es una copia de R pero con el valor E asignado a la variable x. Un ejemplo de un cálculo válido de un wp para una asignación de variables enteras x e y es: Esto significa que para que la "postcondición" x > 10 sea cierta tras la asignación, la "precondición" y > 15 debe ser cierta antes de la asignación. Esto también es la "precondición más débil", en tanto en cuanto es la restricción "más débil" que hay aplicar al valor de y para que x > 10 sea cierto tras la asignación. Dijkstra también definió construcciones de este tipo para las estructuras alternativa (if) y repetitiva (do) así como un operador de composición utilizando wp. Las construcciones alternativa y repetitiva usan comandos guardados para influir en la ejecución. A causa de las reglas impuestas por él en la definición de wp, ambas construcciones permiten ejecuciones no-deterministas si los de los comandos no son disjuntos. A diferencia de otros formalismos semánticos, la semántica de transformación de predicados no fue fruto de la investigación realizada en centros de computación. Más bien fue creada con la intención de proveer a los programadores una metodología de desarrollo de programas "correctamente construidos" basada en un "estilo matemático". Aunque es el más común y más comentado por su relevancia en la programación secuencial, la "precondición más débil" no es el único transformador de predicados existente. Por ejemplo, Leslie Lamport ha propuesto win y sin como transformadores de predicados a utilizar en la programación concurrente. (es) Predicate transformer semantics were introduced by Edsger Dijkstra in his seminal paper "Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of an imperative programming paradigm by assigning to each statement in this language a corresponding predicate transformer: a total function between two predicates on the state space of the statement. In this sense, predicate transformer semantics are a kind of denotational semantics. Actually, in guarded commands, Dijkstra uses only one kind of predicate transformer: the well-known weakest preconditions (see below). Moreover, predicate transformer semantics are a reformulation of Floyd–Hoare logic. Whereas Hoare logic is presented as a deductive system, predicate transformer semantics (either by weakest-preconditions or by strongest-postconditions see below) are complete strategies to build valid deductions of Hoare logic. In other words, they provide an effective algorithm to reduce the problem of verifying a Hoare triple to the problem of proving a first-order formula. Technically, predicate transformer semantics perform a kind of symbolic execution of statements into predicates: execution runs backward in the case of weakest-preconditions, or runs forward in the case of strongest-postconditions. (en) 述語変換意味論（じゅつごへんかんいみろん、Predicate Transformer Semantics）は、エドガー・ダイクストラによるホーア論理の拡張であり、その後も他の研究者が改良を加えたものである。最初に登場したのはダイクストラの論文 "Guarded commands, nondeterminacy and formal derivation of programs" であった。 (ja) Преобразователи предикатов — расширение логики Флойда-Хоара, сделанное Э. Дейкстрой. Впервые появившись в [1], с помощью этого метода определяется семантика императивного программирования и соответствующего языка. В нём каждой команде языка программирования соответствует преобразователь предиката, т. е. полное функциональное соответствие между двумя предикатами в пространстве состояний программы. Основной преобразователь предикатов в последовательном императивном программировании называется слабейшее предусловие (от англ. weakest precondition), обозначаемый wp(S,R). Здесь S — список инструкций (команд), а R — предикат состояния, называемый также . Результат применения этой функции и даёт нам «слабейшее предусловие» для списка S, прерывающийся когда R будет истинным. Например, , получая предикат-копию R со значением x заменённым на E. Важным вариантом wp является так называемое слабейшее свободное предусловие (weakest liberal precondition — перевод даётся по [2]), обозначаемое wlp(S,R). Свободное предусловие является более слабым, т. е. получаемый результат (конечное состояние, удовлетворяющее R) не обязательно «правильный» — гарантируется лишь, что система не выдаст «неправильного» результата (не достигнет такого конечного состояния, которое не удовлетворяло бы R), однако не исключает возможность незавершения работы системы. Таким образом, выражение , где Т — терминальное (конечное) состояние системы, всегда обеспечит истинность R. С помощью wp Дейкстра определил альтернативный (if) и итерационный (do) операторы, а также оператор композиция . Назначением указанных преобразователей предикатов сам Дейкстра указывал создание методологии для программистов по разработке «правильно построенных» программ. Стиль программирования Дейкстры был развит в логике высшего порядка в статье . Можно отметить также другой предикат — сильнейшее постусловие, описывающий максимально сильные ограничения на состояние программы S, которые могут быть получены при данном предусловии. (ru) |
| dbo:wikiPageExternalLink | https://books.google.com/books%3Fid=cCbjBwAAQBAJ https://archive.org/details/disciplineofprog0000dijk https://archive.org/details/mathematicaltheo0000bakk https://archive.org/details/scienceofprogram0000grie |
| dbo:wikiPageID | 1453583 (xsd:integer) |
| dbo:wikiPageLength | 26651 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1124903239 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Deductive_reasoning dbr:Denotational_semantics dbr:Algorithm dbr:Dynamic_logic_(modal_logic) dbr:ESC/Java dbr:Loop_invariant dbr:Coq dbr:Cryptography dbr:Separation_logic dbr:Free_variables_and_bound_variables dbr:Monad_(functional_programming) dbr:Monotonic dbr:Concurrent_programming dbr:Precondition dbr:Leslie_Lamport dbr:Deductive_system dbr:Ralph-Johan_Back dbr:Symbolic_execution dbr:Postcondition dbr:Total_function dbr:Type_theory dbr:Well-founded_relation dbr:Gödel's_completeness_theorem dbr:Edsger_W._Dijkstra dbr:First-order_logic dbr:Formal_semantics_of_programming_languages dbr:Frama-C dbc:Edsger_W._Dijkstra dbr:Niklaus_Wirth dbc:Program_logic dbr:Formal_Aspects_of_Computing dbr:Predicate_(mathematical_logic) dbr:Haskell_(programming_language) dbc:Formal_methods dbr:Hoare_logic dbr:Automated_reasoning dbr:Axiomatic_semantics dbr:B-Method dbr:Guarded_Command_Language dbr:Randomized_algorithm dbr:Refinement_calculus dbr:Satisfiability_modulo_theories dbr:Imperative_programming dbr:Distributed_systems dbr:Evaluation_strategy dbr:Assertion_(computing) dbr:Floyd–Hoare_logic dbr:Guarded_commands dbr:Interactive_theorem_proving |
| dbp:wikiPageUsesTemplate | dbt:Anchor dbt:Citation_needed dbt:Cite_book dbt:Cite_journal dbt:Mvar dbt:Refbegin dbt:Refend dbt:Reflist dbt:Short_description dbt:Semantics dbt:Edsger_Dijkstra |
| dct:subject | dbc:Edsger_W._Dijkstra dbc:Program_logic dbc:Formal_methods |
| rdf:type | yago:Ability105616246 yago:Abstraction100002137 yago:Cognition100023271 yago:Creativity105624700 yago:Invention105633385 yago:Know-how105616786 yago:Method105660268 yago:PsychologicalFeature100023100 yago:WikicatDutchInventions yago:WikicatFormalMethods |
| rdfs:comment | 述語変換意味論（じゅつごへんかんいみろん、Predicate Transformer Semantics）は、エドガー・ダイクストラによるホーア論理の拡張であり、その後も他の研究者が改良を加えたものである。最初に登場したのはダイクストラの論文 "Guarded commands, nondeterminacy and formal derivation of programs" であった。 (ja) La semàntica de transformació de predicats és una extensió de la lògica de Floyd-Hoare ideada per Edsger Dijkstra i divulgada i perfeccionada per altres investigadors. Aquesta extensió va presentar-la Dijkstra en l'article "Comandaments guardats, no-determinisme i derivació formal de programes". Consisteix en un mètode per a definir la semàntica d'un llenguatge de programació imperativa amb l'assignació a cada comandament del corresponent transformador de predicats. Un transformador de predicats és una funció total entre dos predicats del conjunt d'estats d'un programa. (ca) Der wp-Kalkül ist ein Kalkül in der Informatik zur Verifikation eines imperativen Programmcodes. Die Abkürzung wp steht für weakest precondition, auf deutsch schwächste Vorbedingung. Bei der Verifikation geht es nicht darum, die Funktion mit einer bestimmten Menge an Eingabedaten auf korrekte Ergebnisse zu testen, sondern darum, eine allgemeingültige Aussage über das korrekte Ablaufen des Programms zu erhalten. Alternativ kann auch der Hoare-Kalkül benutzt werden, bei dem im Gegensatz zum wp-Kalkül eine Vorwärtsanalyse stattfindet. (de) La semántica de transformación de predicados es una extensión de Lógica de Floyd-Hoare ideada por Edsger Dijkstra y extendida y refinada por otros investigadores. Esta extensión fue presentada por Dijkstra en sus artículos titulados "Guarded commands, nondeterminacy and formal derivation of programs" ("Comandos guardados, no-determinismo y derivación formal de programas"). Consiste en un método para definir la semántica de un lenguaje de programación imperativa mediante la asignación a cada comando del correspondiente transformador de predicados. Un es una función total entre dos predicados del conjunto de estados de un programa. (es) Predicate transformer semantics were introduced by Edsger Dijkstra in his seminal paper "Guarded commands, nondeterminacy and formal derivation of programs". They define the semantics of an imperative programming paradigm by assigning to each statement in this language a corresponding predicate transformer: a total function between two predicates on the state space of the statement. In this sense, predicate transformer semantics are a kind of denotational semantics. Actually, in guarded commands, Dijkstra uses only one kind of predicate transformer: the well-known weakest preconditions (see below). (en) Преобразователи предикатов — расширение логики Флойда-Хоара, сделанное Э. Дейкстрой. Впервые появившись в [1], с помощью этого метода определяется семантика императивного программирования и соответствующего языка. В нём каждой команде языка программирования соответствует преобразователь предиката, т. е. полное функциональное соответствие между двумя предикатами в пространстве состояний программы. , получая предикат-копию R со значением x заменённым на E. Таким образом, выражение , где Т — терминальное (конечное) состояние системы, всегда обеспечит истинность R. (ru) |
| rdfs:label | Semàntica de transformació de predicats (ca) Wp-Kalkül (de) Semántica de transformación de predicados (es) 述語変換意味論 (ja) Predicate transformer semantics (en) Слабейшее предусловие (ru) |
| owl:sameAs | freebase:Predicate transformer semantics yago-res:Predicate transformer semantics wikidata:Predicate transformer semantics dbpedia-bg:Predicate transformer semantics dbpedia-ca:Predicate transformer semantics dbpedia-de:Predicate transformer semantics dbpedia-es:Predicate transformer semantics dbpedia-ja:Predicate transformer semantics dbpedia-ru:Predicate transformer semantics https://global.dbpedia.org/id/2iCn5 |
| prov:wasDerivedFrom | wikipedia-en:Predicate_transformer_semantics?oldid=1124903239&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Predicate_transformer_semantics |
| is dbo:wikiPageRedirects of | dbr:Weakest_liberal_precondition dbr:Weakest_precondition dbr:Weakest_precondition_calculus |
| is dbo:wikiPageWikiLink of | dbr:List_of_Dutch_inventions_and_innovations dbr:Dynamic_logic_(modal_logic) dbr:List_of_programming_language_researchers dbr:Loop_invariant dbr:Carel_S._Scholten dbr:Hoare_logic dbr:Axiomatic_semantics dbr:Guarded_Command_Language dbr:Loop_variant dbr:Semantics_(computer_science) dbr:Unifying_Theories_of_Programming dbr:Weakest_liberal_precondition dbr:Weakest_precondition dbr:Extended_static_checking dbr:List_of_tools_for_static_code_analysis dbr:Weakest_precondition_calculus |
| is foaf:primaryTopic of | wikipedia-en:Predicate_transformer_semantics |