| 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)
|
| 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)
|
