Semàntica de transformació de predicats

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), $wp(S,R)$, 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ó:

$wp(x:=E,R)\ =\ R_{E}^{x}$

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:

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

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.

Referències

• 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 sense: 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 Disciplini of Programming (A systematic introduction with examples). ISBN 0-613-92411-8.