Semantyka i weryfikacja programów

[verrso]

Drodzy forumowicze,

Nadchodzi czas sesji - i mam ogromny problem z zaliczeniem przedmiotu "Semantyka i i weryfikacja programów" na jutro mam rozwiązać zadania - a nie mam pojęcia jak to zrobić - bardzo was proszę o pomoc!

Zad.
Znaleźć najsłabszy warunek wstępny programu \(\displaystyle{ S}\) i predykatu \(\displaystyle{ Q}\) \(\displaystyle{ (NWW (S,Q)=}\)?)

Gdzie: \(\displaystyle{ Q(x,y) =x+1=y}\)

Program S:

Kod: Zaznacz cały

begin
x:=x+1
y:=y+2
end

Jeśli chodzi o "P" to mam zrobić dla dowolnego podanego przez siebie.

Bardzo Was proszę o pomoc - czasu mam nie wiele bo do jutra rana :/ - Liczę na Waszą pomoc.
Pozdrawiam,