Brontekst bekijken van Predicaat-transformer-semantiek

'''Predicaat-transformer-semantiek''' (Engels: ''predicate transformer semantics'') werd geïntroduceerd door [[Edsger Dijkstra]], die daarbij ook [[GCL]] (''Guarded Command Language'') ontwikkelde<ref>{{Citeer tijdschrift |achternaam=Dijkstra |voornaam=Edsger W |titel=Guarded commands, nondeterminacy and formal derivation of programs |url= |jaargang=1975 |tijdschrift=Association for Computing Machinery |datum=1975-08-01 |taal=en |serie=18 |nummer=8 |doi=10.1145/360933.360975 |pagina's=EWD472}}</ref>. De semantiek van imperatieve programma's wordt hierin gekenmerkt door bij elke mogelijke statement van een programma een predicaat-transformer toe te schrijven. Een predicaat-transformer is een totale functie, van predicaat naar predicaat, over de mogelijke toekenningen/staat van het statement. In GCL gebruikt Dijkstra een predicaat-transformer die werkt met [[Hoarelogica#Zwakste precondities|zwakste precondities]], gebaseerd op [[hoarelogica]].

== Toepassingen ==
Predicaat-transformer-semantiek vormt de basis voor een verificatietechniek genaamd ''[[Symbolische uitvoering|symbolic execution]]''. Bij deze techniek spreek men van "achterwaarts" wanneer de postconditie in een bijpassende preconditie wordt omgezet (zoals bij het gebruik van zwakste precondities), en van "voorwaarts" wanneer de preconditie in een bijpassende postconditie wordt omgezet. Wiskundig is dit correct en compleet wanneer het volgende waar is voor de hoaretriples:

<math>\begin{array}{lcl}
\{P\}\ S\ \{Q\} \equiv voorwaarts(S, P) \implies Q \\
\{P\}\ S\ \{Q\} \equiv P \implies achterwaarts(S, Q)
\end{array}</math>

Het dusdanig formaliseren van programma's stelt de computer in staat om [[Assertie|aannames]] in het programma automatisch te verifiëren, aangezien deze geplaatste aannames direct in de hoarelogica kunnen worden opgenomen. Verificatie kan op verschillende manieren gedaan worden; zo kan een programma per mogelijk programmapad gecontroleerd worden<ref>{{Citeer tijdschrift |achternaam=De Boer en Bonsangue |voornaam=Frank S. en Marcello |titel=Symbolic execution formally explained |jaargang=2021 |tijdschrift=Formal Aspects of Computing |datum=2021-08 |taal=en |doi=10.1007/s00165-020-00527-y}}</ref>. Als er dan [[Contradictie|tegenstrijdigheden]] worden gevonden, wordt het programma afgekeurd omdat de aannames geen stand houden.

Voor een computer is dit na te gaan door een [[SMT-solver]] te gebruiken. Bij een afkeuring kan dan ook het huidige model met variabeletoewijzingen teruggeven worden. Dit is een mogelijke invoer voor het programma die tot tegenstrijdigheden met de aannames in het programma leidt.

{{Appendix}}

[[Categorie:Wiskundige logica]]
[[Categorie:Software engineering]]