axiomatique Sémantique - Comment calculer une faible condition

Question

Voici par exemple:

x = y + 1; 
y = y - 2; 
{y < 3} 

Quelle est la plus faible condition de cet exemple?

Je pense que peut-être y < 3 est une réponse.

Sinon, pouvez-vous me dire pourquoi, en détail?

Answer 1

Voici ma première tentative erronée à une réponse fondée sur une lecture rapide de Predicate transformer semantics

WP(x := y + 1; y := y - 2, y < 3)  # Initial problem 
= WP(x := y + 1, WP(y := y - 2, y < 3)) # Sequence rule 
= WP(x := y + 1, y < 5)     # Assignment rule 
= WP(x - 1 = y, y < 5)      # solve for y <--- this is wrong! 
= WP(x - 1 < 5)       # Assignment rule 
= x < 6          # solve for x 

Cependant, comme l'a souligné Kris depuis x := y + 1 est une affectation à x qui ne porte pas atteinte y la condition la plus faible pour y devrait juste être y < 5 donc la réponse correcte doit être

WP(x := y + 1; y := y - 2, y < 3)   # Initial problem 
= WP(x := y + 1, WP(y := y - 2, y < 3)) # Sequence rule 
= WP(x := y + 1, y < 5)      # Assignment rule 
= y < 5          

Merci également à philipxy pour identifier les erreurs dans ma syntaxe en particulier := vs = car cela rendait plus facile de confondre les affectations pour les équations qui faisaient partie de ma confusion initiale.