add if_minus_plus_reloaded exercise

kamalfarahani · Jun 20, 2021 · b3cd5da · b3cd5da
1 parent 106fe81
commit b3cd5da
Showing 1 changed file with 6 additions and 6 deletions.
diff --git a/plf/Hoare2.v b/plf/Hoare2.v
@@ -261,15 +261,15 @@ These decorations were constructed as follows:
 
        {{ True }}
       if X <= Y then
-          {{                         }} ->>
-          {{                         }}
+          {{ True /\ X <= Y }} ->>
+          {{ Y = X + (Y - X) }}
         Z := Y - X
-          {{                         }}
+          {{ Y = X + Z }}
       else
-          {{                         }} ->>
-          {{                         }}
+          {{ True /\ ~(X <= Y) }} ->>
+          {{ X + Z = X + Z }}
         Y := X + Z
-          {{                         }}
+          {{ Y = X + Z }}
       end
         {{ Y = X + Z }}