Semántica de transformación de predicados

Semántica de transformación de predicados

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 transformador de predicados 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) wp(S,R). 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:

wp(x := E, R)\ =\ R_E^x

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:

wp(x := y - 5, x > 10)\ =\ (y - 5 > 10)\ =\ (y > 15)

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 guardianes 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.

Referencias

  • Edsger Dijkstra, "Guarded commands, nondeterminacy and formal derivation of programs". Communications of the ACM, 18(8):453–457, August 1975. [1]
  • Leslie Lamport, "win and sin: Predicate Transformers for Concurrency". ACM Transactions on Programming Languages and Systems, 12(3), July 1990. [2]
  • Ralph-Johan Back and Joakim von Wright, Refinement Calculus: A Systematic Introduction, 1st edition, 1998. ISBN 0-387-98417-8.
  • Edsger W. Dijkstra. A Discipline of Programming (A systematic introduction with examples). ISBN 0-613-92411-8.

Wikimedia foundation. 2010.

Игры ⚽ Поможем написать реферат

Mira otros diccionarios:

  • Comandos Guardados — Saltar a navegación, búsqueda Comandos guardados (GCL) órdenes guardadas es un modelo de lenguaje definido por Edsger Dijkstra para semántica de transformación de predicados (una extensión lógica diseñada para proporcionar una metodología para… …   Wikipedia Español

  • Lenguaje de Comandos Guardados — El Lenguaje de Comandos Guardados (GCL, Guarded Command Language), o de Órdenes Guardadas, es un modelo de lenguaje definido por Edsger Dijkstra para semántica de transformación de predicados (una extensión lógica diseñada para proporcionar una… …   Wikipedia Español

  • Lógica de Hoare — Este artículo o sección necesita referencias que aparezcan en una publicación acreditada, como revistas especializadas, monografías, prensa diaria o páginas de Internet fidedignas. Puedes añadirlas así o avisar …   Wikipedia Español

  • Método formal — En ingeniería de software un método formal es un camino a la construcción y análisis de modelos matemáticos que permitan una automatización del desarrollo de sistemas informáticos. Los métodos formales se caracterizan por emplear técnicas y… …   Wikipedia Español

  • Lógica — La lógica es una ciencia formal y una rama de la filosofía que estudia los principios de la demostración e inferencia válida. La palabra deriva del griego antiguo λογική (logike), que significa «dotado de razón, intelectual, dialéctico,… …   Wikipedia Español

  • Gráficos existenciales — Se denomina Gráficos existenciales (en inglés: existential graphs) al sistema lógico y de notación creado por el lógico y filósofo norteamericano Charles Sanders Peirce. El sistema comprende tanto una notación gráfica original de proposiciones… …   Wikipedia Español

  • Silogismo — El silogismo es una forma de razonamiento deductivo que consta de dos proposiciones como premisas y otra como conclusión, siendo la última una inferencia necesariamente deductiva de las otras dos. Fue formulado por primera vez por Aristóteles, en …   Wikipedia Español

  • Traducción automática mediante transferencia — La traducción por transferencia es un tipo de traducción automática. Se fundamenta sobre las bases de interlingua, y es actualmente uno de los métodos de traducción automática más ampliamente utilizados. Contenido 1 Visión General 2… …   Wikipedia Español

  • Afirmación — El término Afirmación consiste en un acto por el cual manifestamos nuestro asentimiento intelectual y compromiso social respecto a una creencia expresando lingüísticamente un enunciado; considerando y declarando válida con plena conciencia su… …   Wikipedia Español

  • Parménides de Elea — Saltar a navegación, búsqueda Parménides (Παρμενίδης) Filosofía occidental Filosofía presocrática …   Wikipedia Español

Compartir el artículo y extractos

Link directo
… Do a right-click on the link above
and select “Copy Link”