Zpo-8-wyk-Slajd9
Rozszerzona definicja
Roberts zaobserwował, że proste przekształcenia zdefiniowane przez Opdyke'a nie są stosowane w praktyce, ponieważ wprowadzają zbyt drobne zmiany. Konieczne jest zatem stosowanie większych struktur: łańcuchów przekształceń. Jednak dowodzenie poprawności całych łańcuchów było zbyt trudne, ponieważ wymagało osobnego dowodu dla każdego przekształcenia z osobna, a co za tym idzie – obliczenia warunków wstępnych będących wynikiem wykonania wcześniejszych przekształceń w łańcuchu.
Dlatego Roberts zaproponował, aby rozszerzyć definicję każdego przekształcenia o warunki końcowe, które są prawdziwe po jej wykonaniu, np. po utworzeniu metody warunkiem końcowym jest jej istnienie. Ta drobna zmiana pozwoliła jednak znacznie łatwiej wykazywać poprawność łańcuchów przekształceń, wykorzystując znane już informacje pochodzące z analizy wcześniejszych przekształceń prostych.
